Skip to content
This repository was archived by the owner on Jan 30, 2023. It is now read-only.

Commit 0d4e2a1

Browse files
committed
19040: prep satisfiable()
1 parent 7c6a8aa commit 0d4e2a1

File tree

1 file changed

+52
-60
lines changed

1 file changed

+52
-60
lines changed

src/sage/symbolic/expression.pyx

+52-60
Original file line numberDiff line numberDiff line change
@@ -2423,8 +2423,16 @@ cdef class Expression(CommutativeRingElement):
24232423
else:
24242424
return self.operator()(num, 0)
24252425

2426-
if self.operator() != operator.eq and self.operator() != operator.ne:
2426+
so = self.operator()
2427+
if so != operator.eq and so != operator.ne:
24272428
raise AttributeError("Please use satisfiable(), truth(), or solve() to decide symbolic inequalities.")
2429+
#poc = print_order_compare(self._gobj.lhs(), self._gobj.rhs())
2430+
#if poc == 0:
2431+
# return so == operator.ge or so == operator.le
2432+
#elif poc == 1:
2433+
# return so == operator.ge or so == operator.gt
2434+
#elif poc == -1:
2435+
# return so == operator.le or so == operator.lt
24282436
zero = (self.lhs()-self.rhs()).expand().is_trivial_zero()
24292437
if self.operator() == operator.eq:
24302438
return zero
@@ -2442,67 +2450,51 @@ cdef class Expression(CommutativeRingElement):
24422450

24432451

24442452
def satisfiable(self):
2445-
if self.is_relational():
2446-
# constants are wrappers around Sage objects, compare directly
2447-
if is_a_constant(self._gobj.lhs()) and is_a_constant(self._gobj.rhs()):
2448-
return self.operator()(self.lhs().pyobject(), self.rhs().pyobject())
2449-
2450-
pynac_result = relational_to_bool(self._gobj)
2451-
2452-
# pynac is guaranteed to give the correct answer for comparing infinities
2453-
if is_a_infinity(self._gobj.lhs()) or is_a_infinity(self._gobj.rhs()):
2454-
return pynac_result
2455-
2456-
if pynac_result:
2457-
if self.operator() == operator.ne: # this hack is necessary to catch the case where the operator is != but is False because of assumptions made
2458-
m = self._maxima_()
2459-
s = m.parent()._eval_line('is (notequal(%s,%s))'%(repr(m.lhs()),repr(m.rhs())))
2460-
if s == 'false':
2461-
return False
2462-
else:
2463-
return True
2464-
else:
2465-
return True
2453+
if len(self.variables())==0:
2454+
return self.__nonzero__()
2455+
2456+
res = relational_to_bool(self._gobj)
2457+
if res and self.operator() == operator.ne: # this hack is necessary to catch the case where the operator is != but is False because of assumptions made
2458+
m = self._maxima_()
2459+
s = m.parent()._eval_line('is (notequal(%s,%s))'%(repr(m.lhs()),repr(m.rhs())))
2460+
if s == 'false':
2461+
return False
2462+
else:
2463+
return True
24662464

2467-
# If assumptions are involved, falsification is more complicated...
2468-
need_assumptions = False
2469-
from sage.symbolic.assumptions import assumptions
2470-
assumption_list = assumptions()
2471-
if assumption_list:
2472-
vars = self.variables()
2473-
if vars:
2474-
assumption_var_list = []
2475-
for eqn in assumption_list:
2476-
try:
2477-
assumption_var_list.append(eqn.variables())
2478-
except AttributeError: # if we have a GenericDeclaration
2479-
assumption_var_list.append((eqn._var,))
2480-
assumption_vars = set(sum(assumption_var_list, ()))
2481-
if set(vars).intersection(assumption_vars):
2482-
need_assumptions = True
2483-
2484-
# Use interval fields to try and falsify the relation
2485-
if not need_assumptions:
2486-
res = self.test_relation()
2487-
if res is True:
2488-
return True
2489-
elif res is False:
2490-
return False
2465+
# If assumptions are involved, falsification is more complicated...
2466+
need_assumptions = False
2467+
from sage.symbolic.assumptions import assumptions
2468+
assumption_list = assumptions()
2469+
if assumption_list:
2470+
vars = self.variables()
2471+
if vars:
2472+
assumption_var_list = []
2473+
for eqn in assumption_list:
2474+
try:
2475+
assumption_var_list.append(eqn.variables())
2476+
except AttributeError: # if we have a GenericDeclaration
2477+
assumption_var_list.append((eqn._var,))
2478+
assumption_vars = set(sum(assumption_var_list, ()))
2479+
if set(vars).intersection(assumption_vars):
2480+
need_assumptions = True
2481+
2482+
# Use interval fields to try and falsify the relation
2483+
if not need_assumptions:
2484+
res = self.test_relation()
2485+
if res is True:
2486+
return True
2487+
elif res is False:
2488+
return False
24912489

2492-
# we really have to do some work here...
2493-
# I really don't like calling Maxima to test equality. It
2494-
# is SUPER SUPER SLOW, and it has all the problem
2495-
# associated with different semantics, different
2496-
# precision, etc., that can lead to subtle bugs. Also, a
2497-
# lot of basic Sage objects can't be put into maxima.
2498-
from sage.symbolic.relation import test_relation_maxima
2499-
return test_relation_maxima(self)
2500-
2501-
self_is_zero = self._gobj.is_zero()
2502-
if self_is_zero:
2503-
return False
2504-
else:
2505-
return not bool(self == self._parent.zero())
2490+
# we really have to do some work here...
2491+
# I really don't like calling Maxima to test equality. It
2492+
# is SUPER SUPER SLOW, and it has all the problem
2493+
# associated with different semantics, different
2494+
# precision, etc., that can lead to subtle bugs. Also, a
2495+
# lot of basic Sage objects can't be put into maxima.
2496+
from sage.symbolic.relation import test_relation_maxima
2497+
return test_relation_maxima(self)
25062498

25072499
def test_relation(self, int ntests=20, domain=None, proof=True):
25082500
"""

0 commit comments

Comments
 (0)