symbolic relations metaticket

[rwst]

We should provide a detailed interface for symbolic relations:

• bool(rel) equivalent to (not)(LHS-RHS).is_trivial_zero() for ==,!= ; and for <, >, <=, >= the result follows alpha order of lhs and rhs
• satisfiable(rel) returning (Yes,example)/No/Undecidable/NotImplemented
• solve(rel) in case of satisfiable=Yes returning the full solution set
• is(rel) attempting simplification/proof, returning True/False, throwing NotImplementedError
• ex.is_zero(simplify=False) (default) calling the fast bool(ex==0) (Fix usage of symbolic comparison in several places #24992)
• ex.is_zero(simplify=True) attempting simplification/proof (Fix usage of symbolic comparison in several places #24992)
• prove(rel) showing more or less steps of simplification (which is out of reach for the moment)

Tickets:

• rewrite Expression.__nonzero__() #19040: to take satisfiability/truth functionality out of ex.__nonzero__ into resp. member functions
• Meta-ticket: SAT and SMT #19000: SMT-solver is needed for dedicated satisfiable()

See also https://trac.sagemath.org/wiki/symbolics/nonzero

CC: @videlec @slel

Component: symbolics

Issue created by migration from https://trac.sagemath.org/ticket/19162

[rwst]

Description changed:

--- 
+++ 
@@ -1,8 +1,10 @@
 We should provide a detailed interface for symbolic relations:
-* `bool(rel)` equivalent to `(not)(LHS-RHS).is_trivial_zero()` for ==,!= ; and an exception with maybe hint to the following for <,>,<=,>=
+* `bool(rel)` equivalent to `(not)(LHS-RHS).is_trivial_zero()` for ==,!= ; and for <, >, <=, >= the result follows alpha order of lhs and rhs
 * `satisfiable(rel)` returning `(Yes,example)/No/Undecidable/NotImplemented`
-* `truth(rel, (x,S1), (y,S2)...)` equivalent to `satisfiable(rel)` with quantifiers: for all `x,y...` in `S1,S2,...`
 * `solve(rel)` in case of `satisfiable=Yes` returning the full solution set
+* `is(rel)` attempting simplification/proof, returning `True`/`False`, throwing `NotImplementedError` 
+* `ex.is_zero(simplify=False)` (default) calling the fast `bool(ex==0)`
+* `ex.is_zero(simplify=True)` attempting simplification/proof
 * `prove(rel)` showing more or less steps of simplification (which is out of reach for the moment)
 
 Tickets:

[rwst]

Description changed:

--- 
+++ 
@@ -9,3 +9,4 @@
 
 Tickets:
 * #19040: to take satisfiability/truth functionality out of `ex.__nonzero__` into resp. member functions
+* #19000: SMT-solver is needed for dedicated `satisfiable()`

[rwst]

Description changed:

--- 
+++ 
@@ -10,3 +10,5 @@
 Tickets:
 * #19040: to take satisfiability/truth functionality out of `ex.__nonzero__` into resp. member functions
 * #19000: SMT-solver is needed for dedicated `satisfiable()`
+
+See also https://trac.sagemath.org/wiki/symbolics/nonzero

[rwst]

Description changed:

--- 
+++ 
@@ -3,8 +3,8 @@
 * `satisfiable(rel)` returning `(Yes,example)/No/Undecidable/NotImplemented`
 * `solve(rel)` in case of `satisfiable=Yes` returning the full solution set
 * `is(rel)` attempting simplification/proof, returning `True`/`False`, throwing `NotImplementedError` 
-* `ex.is_zero(simplify=False)` (default) calling the fast `bool(ex==0)`
-* `ex.is_zero(simplify=True)` attempting simplification/proof
+* `ex.is_zero(simplify=False)` (default) calling the fast `bool(ex==0)` (#24992)
+* `ex.is_zero(simplify=True)` attempting simplification/proof (#24992)
 * `prove(rel)` showing more or less steps of simplification (which is out of reach for the moment)
 
 Tickets: