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