search

sagemath / sage

Main repository of SageMath
https://www.sagemath.org
Other
1.33k stars 453 forks source link

symbolic relations metaticket #19162

Open rwst opened 9 years ago

rwst commented 9 years ago

We should provide a detailed interface for symbolic relations:

Tickets:

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 commented 8 years ago

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 commented 8 years ago

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 commented 6 years ago

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 commented 6 years ago

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: