id summary reporter owner description type status priority milestone component resolution keywords cc merged author reviewer upstream work_issues branch commit dependencies stopgaps
19162 symbolic relations metaticket rws "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)` (#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:
* #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" enhancement new major sage-8.2 symbolics vdelecroix slelievre N/A