Opened 3 years ago

Last modified 11 months ago

#19162 new enhancement

symbolic relations metaticket

Reported by: rws Owned by:
Priority: major Milestone: sage-8.2
Component: symbolics Keywords:
Cc: vdelecroix, slelievre Merged in:
Authors: Reviewers:
Report Upstream: N/A Work issues:
Branch: Commit:
Dependencies: Stopgaps:

Description (last modified by 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

Change History (5)

comment:1 Changed 3 years ago by slelievre

  • Cc vdelecroix slelievre added

comment:2 Changed 3 years ago by rws

  • Description modified (diff)

comment:3 Changed 3 years ago by rws

  • Description modified (diff)

comment:4 Changed 11 months ago by rws

  • Description modified (diff)
  • Milestone changed from sage-6.9 to sage-8.2

comment:5 Changed 11 months ago by rws

  • Description modified (diff)
Note: See TracTickets for help on using tickets.