diff --git a/mathics/builtin/assumptions/assumptions.py b/mathics/builtin/assumptions/assumptions.py index b54281508..04cda037e 100644 --- a/mathics/builtin/assumptions/assumptions.py +++ b/mathics/builtin/assumptions/assumptions.py @@ -5,7 +5,7 @@ from mathics.builtin.scoping import dynamic_scoping from mathics.core.attributes import A_HOLD_REST, A_NO_ATTRIBUTES, A_PROTECTED from mathics.core.builtin import Builtin, Predefined -from mathics.core.convert.sympy import to_sympy_assumptions +from mathics.core.convert.sympy_predicates import to_sympy_predicates from mathics.core.evaluation import Evaluation from mathics.core.list import ListExpression from mathics.core.symbols import Symbol, SymbolFalse, SymbolTrue @@ -142,5 +142,5 @@ def eval(self, expr, assumptions, evaluation: Evaluation): if assumptions_eval is SymbolTrue or assumptions_eval is None: return expr.evaluate(evaluation) - sympy_assumptions = to_sympy_assumptions(assumptions_eval) + sympy_assumptions = to_sympy_predicates(assumptions_eval) return eval_Refine(expr, sympy_assumptions, evaluation) diff --git a/mathics/core/convert/sympy.py b/mathics/core/convert/sympy.py index d587104a5..3a2749715 100644 --- a/mathics/core/convert/sympy.py +++ b/mathics/core/convert/sympy.py @@ -1,49 +1,20 @@ -# -*- coding: utf-8 -*- - """ Converts expressions from SymPy to Mathics3 expressions. -Conversion to SymPy is handled directly in BaseElement descendants. +Provides conversion to SymPy for Mathics3 BaseElement descendants. """ -from typing import ( - TYPE_CHECKING, - Dict, - Final, - List, - Optional, - Sequence, - Tuple, - Union, - cast, -) +from typing import TYPE_CHECKING, Dict, List, Optional, Sequence, Tuple, Union, cast import sympy from sympy import ( - And, Dummy as Sympy_Dummy, - Ne, - Not, - Or, - Q, Symbol, Symbol as Sympy_Symbol, false as SympyFalse, true as SympyTrue, ) -from sympy.assumptions.assume import AppliedPredicate from sympy.calculus.accumulationbounds import AccumulationBounds -from sympy.core.relational import ( - Equality, - GreaterThan, - LessThan, - Ne, - Relational, - StrictGreaterThan, - StrictLessThan, -) from sympy.core.singleton import S -from sympy.sets.contains import Contains -from sympy.sets.fancysets import Complexes, Integers, Rationals, Reals from mathics.core.atoms import ( MATHICS3_COMPLEX_I, @@ -83,11 +54,9 @@ sympy_name, ) from mathics.core.systemsymbols import ( - SymbolAnd, SymbolC, SymbolCatalan, SymbolE, - SymbolElement, SymbolEqual, SymbolEulerGamma, SymbolFunction, @@ -98,9 +67,7 @@ SymbolLess, SymbolLessEqual, SymbolMatrixPower, - SymbolNot, SymbolO, - SymbolOr, SymbolPi, SymbolPiecewise, SymbolPrime, @@ -149,121 +116,11 @@ key: val for val, key in sympy_singleton_to_mathics.items() } -SYMPY_FALSE_PREDICATE: Final[AppliedPredicate] = Q.is_true(False) -SYMPY_TRUE_PREDICATE: Final[AppliedPredicate] = Q.is_true(True) - - -def sympy_expr_to_predicate(sympy_expr): - """ - Converts SymPy expressions (relational, boolean, or predicates) - into canonical SymPy Q AppliedPredicates for SymPy 1.14.0+. - Note: Newer SymPy can use sask() and to_predicate() - """ - # Already an AppliedPredicate (e.g., Q.positive(x)) or Boolean - if isinstance(sympy_expr, AppliedPredicate): - return sympy_expr - - # Boolean compound trees (And, Or, Not) - if ( - isinstance(sympy_expr, Not) - or hasattr(sympy_expr, "is_Not") - and sympy_expr.is_Not - ): - return Not(sympy_expr_to_predicate(sympy_expr.args[0])) - if ( - isinstance(sympy_expr, And) - or hasattr(sympy_expr, "is_And") - and sympy_expr.is_And - ): - return And(*[sympy_expr_to_predicate(arg) for arg in sympy_expr.args]) - if isinstance(sympy_expr, Or) or hasattr(sympy_expr, "is_Or") and sympy_expr.is_Or: - return Or(*[sympy_expr_to_predicate(arg) for arg in sympy_expr.args]) - - # Domain membership checks (Element(x, Reals), Contains(x, Integers), etc.) - # In SymPy, Element(x, S) constructs a Contains(x, S) object - if isinstance(sympy_expr, Contains) or type(sympy_expr).__name__ in ( - "Element", - "Contains", - ): - element, domain = sympy_expr.args[0], sympy_expr.args[1] - - # Map standard sets to corresponding Q domain predicates - if hasattr(domain, "name") and domain.name in ("Booleans", "Boolean"): - return Q.boolean(element) - if isinstance(domain, Complexes) or ( - hasattr(domain, "name") and domain.name == "Complexes" - ): - return Q.complex(element) - elif isinstance(domain, Integers) or ( - hasattr(domain, "name") and domain.name == "Integers" - ): - return Q.integer(element) - elif isinstance(domain, Rationals) or ( - hasattr(domain, "name") and domain.name == "Rationals" - ): - return Q.rational(element) - elif isinstance(domain, Reals) or ( - hasattr(domain, "name") and domain.name == "Reals" - ): - return Q.real(element) - else: - raise RuntimeError(f"Domain {domain} is not valid") - - # Relational expressions with directional alignment. - if isinstance(sympy_expr, Relational): - # Handle zero-rhs explicit cases directly to preserve original symbol orientation - if sympy_expr.rhs == 0: - if isinstance(sympy_expr, StrictGreaterThan): - return Q.positive(sympy_expr.lhs) - elif isinstance(sympy_expr, StrictLessThan): - return Q.negative(sympy_expr.lhs) - elif isinstance(sympy_expr, GreaterThan): - return Q.nonnegative(sympy_expr.lhs) - elif isinstance(sympy_expr, LessThan): - return Q.nonpositive(sympy_expr.lhs) - elif isinstance(sympy_expr, Equality): - return Q.zero(sympy_expr.lhs) - elif isinstance(sympy_expr, Ne): - return Q.nonzero(sympy_expr.lhs) - - # Handle zero-lhs explicit cases (0 < x -> x > 0 -> Q.positive(x)) - if sympy_expr.lhs == 0: - if isinstance(sympy_expr, StrictGreaterThan): # 0 > x -> x < 0 - return Q.negative(sympy_expr.rhs) - elif isinstance(sympy_expr, StrictLessThan): # 0 < x -> x > 0 - return Q.positive(sympy_expr.rhs) - elif isinstance(sympy_expr, GreaterThan): # 0 >= x -> x <= 0 - return Q.nonpositive(sympy_expr.rhs) - elif isinstance(sympy_expr, LessThan): # 0 <= x -> x >= 0 - return Q.nonnegative(sympy_expr.rhs) - elif isinstance(sympy_expr, Equality): - return Q.zero(sympy_expr.rhs) - elif isinstance(sympy_expr, Ne): - return Q.nonzero(sympy_expr.rhs) - - # Non-zero general cases (algebraic reduction). - if isinstance(sympy_expr, StrictGreaterThan): # lhs > rhs -> lhs - rhs > 0 - return Q.positive(sympy_expr.lhs - sympy_expr.rhs) - elif isinstance(sympy_expr, StrictLessThan): # lhs < rhs -> rhs - lhs > 0 - return Q.positive(sympy_expr.rhs - sympy_expr.lhs) - elif isinstance(sympy_expr, GreaterThan): # lhs >= rhs -> lhs - rhs >= 0 - return Q.nonnegative(sympy_expr.lhs - sympy_expr.rhs) - elif isinstance(sympy_expr, LessThan): # lhs <= rhs -> rhs - lhs >= 0 - return Q.nonnegative(sympy_expr.rhs - sympy_expr.lhs) - elif isinstance(sympy_expr, Equality): - return Q.zero(sympy_expr.lhs - sympy_expr.rhs) - elif isinstance(sympy_expr, Ne): - return Q.nonzero(sympy_expr.lhs - sympy_expr.rhs) - - # None of the above conditions. - # Fallback to a general boolean sympy_expression. - return Q.is_true(sympy_expr) - def sympy_decode_mathics_symbol_name(name: str) -> str: """ - Remove the Prefix for Mathics3 symbols - and restore the context separator character. + Remove the Mathics3-supplied prefix in symbol names, + and restore the context-separator character. """ if name.startswith(SYMPY_SYMBOL_PREFIX): return name[len(SYMPY_SYMBOL_PREFIX) :].replace("_", "`") @@ -280,54 +137,9 @@ def is_Cn_expr(name: str) -> bool: return number != "" and number.isdigit() -def to_sympy_assumptions(assumptions) -> AppliedPredicate: - """Convert a Mathics3 assumptions expression to an - AppliedPredicate (or True) that can be used by SymPy. None is - returned if we can't convert to a Sympy matrix. - - """ - match assumptions: - case val if val is SymbolTrue: - return SYMPY_TRUE_PREDICATE - case val if val is SymbolFalse: - return SYMPY_FALSE_PREDICATE - case val if isinstance(val, ListExpression): - combined_predicate = SYMPY_TRUE_PREDICATE - for elem in val.elements: - sympy_assume = to_sympy_assumptions(elem) - if sympy_assume is not SYMPY_TRUE_PREDICATE: - if combined_predicate is SYMPY_TRUE_PREDICATE: - combined_predicate = sympy_assume - elif isinstance(sympy_assume, AppliedPredicate): - combined_predicate = AppliedPredicate("And", *sympy_assume.args) - else: - raise RuntimeError( - "to_sympy_assumptions returned whacky result {sympy_assume}" - ) - return combined_predicate - - case expr if isinstance(val, Expression): - head = expr.head - if head in ( - SymbolAnd, - SymbolOr, - SymbolNot, - SymbolElement, - SymbolEqual, - SymbolGreater, - SymbolGreaterEqual, - SymbolLess, - SymbolLessEqual, - ): - if (sympy_expr := expr.to_sympy()) is not None: - return sympy_expr_to_predicate(sympy_expr) - - return SYMPY_TRUE_PREDICATE - - def to_sympy_matrix(data, **__) -> Optional[sympy.MutableDenseMatrix]: - """Convert a Mathics3 matrix to one that can be used by Sympy. - None is returned if we can't convert to a Sympy matrix. + """Convert a Mathics3 matrix to one that can be used by SymPy. + None is returned if we can't convert to a SymPy matrix. """ if not isinstance(data, list): data = matrix_data(data) @@ -392,7 +204,7 @@ def has_any_symbols(self, *syms) -> bool: return result def _eval_subs(self, old, new): - """Replace occurencies of old by new in self.""" + """Replace occurrences of old by new in self.""" if self == old: return new old, new = from_sympy(old), from_sympy(new) @@ -406,7 +218,7 @@ def _eval_rewrite(self, rule, args, **hints): return self # @property does not match SymPy's definition. However, - # @is_commutative.setter is needed, by linear algebra stuff. And + # @is_commutative.setter is needed in linear algebra stuff. And # for that, we need @property here. @property # pyrefly: ignore [bad-override] @@ -555,7 +367,7 @@ def from_sympy_matrix( def from_sympy(sympy_expr) -> BaseElement | Symbol: """ - converts a SymPy object to a Mathics3 element. + Converts a SymPy object to a Mathics3 element. """ if isinstance(sympy_expr, (tuple, list)): return to_mathics_list(*sympy_expr, elements_conversion_fn=from_sympy) diff --git a/mathics/core/convert/sympy_predicates.py b/mathics/core/convert/sympy_predicates.py new file mode 100644 index 000000000..d02a5e197 --- /dev/null +++ b/mathics/core/convert/sympy_predicates.py @@ -0,0 +1,196 @@ +""" +Converts expressions from Mathics3 expressions to SymPy Predicates. +These are used in the built-in functions Refine and Assumptions. +""" + +from typing import Final + +from sympy import And, Ne, Not, Or, Q +from sympy.assumptions.assume import AppliedPredicate +from sympy.core.add import Add +from sympy.core.mul import Mul +from sympy.core.relational import ( + Equality, + GreaterThan, + LessThan, + Ne, + Relational, + StrictGreaterThan, + StrictLessThan, +) +from sympy.sets.contains import Contains +from sympy.sets.fancysets import Complexes, Integers, Rationals, Reals + +from mathics.core.expression import Expression +from mathics.core.list import ListExpression +from mathics.core.symbols import SymbolFalse, SymbolTrue +from mathics.core.systemsymbols import ( + SymbolAnd, + SymbolElement, + SymbolEqual, + SymbolGreater, + SymbolGreaterEqual, + SymbolLess, + SymbolLessEqual, + SymbolNot, + SymbolOr, +) + +SYMPY_FALSE_PREDICATE: Final[AppliedPredicate] = Q.is_true(False) +SYMPY_TRUE_PREDICATE: Final[AppliedPredicate] = Q.is_true(True) + + +def sympy_expr_to_predicate(sympy_expr): + """ + Converts SymPy expressions (relational, boolean, or predicates) + into canonical SymPy Q AppliedPredicates for SymPy 1.14.0+. + Note: Newer SymPy can use sask() and to_predicate() + """ + # Already an AppliedPredicate (e.g., Q.positive(x)) or Boolean + if isinstance(sympy_expr, AppliedPredicate): + return sympy_expr + + # Boolean compound trees (And, Or, Not) + if ( + isinstance(sympy_expr, Not) + or hasattr(sympy_expr, "is_Not") + and sympy_expr.is_Not + ): + return Not(sympy_expr_to_predicate(sympy_expr.args[0])) + if ( + isinstance(sympy_expr, And) + or hasattr(sympy_expr, "is_And") + and sympy_expr.is_And + ): + return And(*[sympy_expr_to_predicate(arg) for arg in sympy_expr.args]) + if isinstance(sympy_expr, Or) or hasattr(sympy_expr, "is_Or") and sympy_expr.is_Or: + return Or(*[sympy_expr_to_predicate(arg) for arg in sympy_expr.args]) + + # Domain membership checks (Element(x, Reals), Contains(x, Integers), etc.) + # In SymPy, Element(x, S) constructs a Contains(x, S) object + if isinstance(sympy_expr, Contains) or type(sympy_expr).__name__ in ( + "Element", + "Contains", + ): + element, domain = sympy_expr.args[0], sympy_expr.args[1] + + # Map standard sets to their corresponding SymPy Q domain predicates. + if hasattr(domain, "name") and domain.name in ("Booleans", "Boolean"): + return Q.boolean(element) + if isinstance(domain, Complexes) or ( + hasattr(domain, "name") and domain.name == "Complexes" + ): + return Q.complex(element) + elif isinstance(domain, Integers) or ( + hasattr(domain, "name") and domain.name == "Integers" + ): + return Q.integer(element) + elif isinstance(domain, Rationals) or ( + hasattr(domain, "name") and domain.name == "Rationals" + ): + return Q.rational(element) + elif isinstance(domain, Reals) or ( + hasattr(domain, "name") and domain.name == "Reals" + ): + return Q.real(element) + else: + raise RuntimeError(f"Domain {domain} is not valid") + + # Relational expressions, canonicalizing the relation direction. + if isinstance(sympy_expr, Relational): + # Handle where the rhs is zero. For example: x > 0 -> Q.positive(x) + # Handle zero-rhs explicit cases directly to preserve original symbol orientation + if sympy_expr.rhs == 0: + if isinstance(sympy_expr, StrictGreaterThan): + return Q.positive(sympy_expr.lhs) + elif isinstance(sympy_expr, StrictLessThan): + return Q.negative(sympy_expr.lhs) + elif isinstance(sympy_expr, GreaterThan): + return Q.nonnegative(sympy_expr.lhs) + elif isinstance(sympy_expr, LessThan): + return Q.nonpositive(sympy_expr.lhs) + elif isinstance(sympy_expr, Equality): + return Q.zero(sympy_expr.lhs) + elif isinstance(sympy_expr, Ne): + return Q.nonzero(sympy_expr.lhs) + + # Handle where the lhs is zero. For example: 0 < x is the same as x > 0 -> Q.positive(x) + if sympy_expr.lhs == 0: + if isinstance(sympy_expr, StrictGreaterThan): # 0 > x -> x < 0 + return Q.negative(sympy_expr.rhs) + elif isinstance(sympy_expr, StrictLessThan): # 0 < x -> x > 0 + return Q.positive(sympy_expr.rhs) + elif isinstance(sympy_expr, GreaterThan): # 0 >= x -> x <= 0 + return Q.nonpositive(sympy_expr.rhs) + elif isinstance(sympy_expr, LessThan): # 0 <= x -> x >= 0 + return Q.nonnegative(sympy_expr.rhs) + elif isinstance(sympy_expr, Equality): + return Q.zero(sympy_expr.rhs) + elif isinstance(sympy_expr, Ne): + return Q.nonzero(sympy_expr.rhs) + + lhs, rhs = sympy_expr.lhs, sympy_expr.rhs + # Construct negated terms explicitly using Mul(-1, ...) to make type checking happy. + neg_rhs = Mul(-1, rhs) + neg_lhs = Mul(-1, lhs) + + # Non-zero general cases (algebraic reduction). + if isinstance(sympy_expr, StrictGreaterThan): # lhs > rhs -> lhs - rhs > 0 + return Q.positive(Add(lhs, neg_rhs)) + elif isinstance(sympy_expr, StrictLessThan): # lhs < rhs -> rhs - lhs > 0 + return Q.positive(Add(rhs, neg_lhs)) + elif isinstance(sympy_expr, GreaterThan): # lhs >= rhs -> lhs - rhs >= 0 + return Q.nonnegative(Add(lhs, neg_rhs)) + elif isinstance(sympy_expr, LessThan): # lhs <= rhs -> rhs - lhs >= 0 + return Q.nonnegative(Add(rhs, neg_lhs)) + elif isinstance(sympy_expr, Equality): + return Q.zero(Add(lhs, neg_rhs)) + elif isinstance(sympy_expr, Ne): + return Q.nonzero(Add(lhs, neg_rhs)) + + # None of the above conditions. + # Fallback to a general boolean sympy_expression. + return Q.is_true(sympy_expr) + + +def to_sympy_predicates(assumptions) -> AppliedPredicate: + """Convert a Mathics3 assumptions expression to an + AppliedPredicate used in SymPy's refine() or with_assumptions(). + """ + match assumptions: + case val if val is SymbolTrue: + return SYMPY_TRUE_PREDICATE + case val if val is SymbolFalse: + return SYMPY_FALSE_PREDICATE + case val if isinstance(val, ListExpression): + combined_predicate = SYMPY_TRUE_PREDICATE + for elem in val.elements: + sympy_assume = to_sympy_predicates(elem) + if sympy_assume is not SYMPY_TRUE_PREDICATE: + if combined_predicate is SYMPY_TRUE_PREDICATE: + combined_predicate = sympy_assume + elif isinstance(sympy_assume, AppliedPredicate): + combined_predicate = AppliedPredicate("And", *sympy_assume.args) + else: + raise RuntimeError( + f"to_sympy_predicates returned whacky result {sympy_assume}" + ) + return combined_predicate + + case expr if isinstance(val, Expression): + head = expr.head + if head in ( + SymbolAnd, + SymbolOr, + SymbolNot, + SymbolElement, + SymbolEqual, + SymbolGreater, + SymbolGreaterEqual, + SymbolLess, + SymbolLessEqual, + ): + if (sympy_expr := expr.to_sympy()) is not None: + return sympy_expr_to_predicate(sympy_expr) + + return SYMPY_TRUE_PREDICATE diff --git a/test/core/convert/test_sympy_predicate.py b/test/core/convert/test_sympy_predicate.py index eb63e95f5..8c9ab6cae 100644 --- a/test/core/convert/test_sympy_predicate.py +++ b/test/core/convert/test_sympy_predicate.py @@ -18,7 +18,7 @@ ) from sympy.assumptions.assume import AppliedPredicate -from mathics.core.convert.sympy import sympy_expr_to_predicate +from mathics.core.convert.sympy_predicates import sympy_expr_to_predicate from mathics.core.symbols import Symbol Symbol_a = Symbol("Global`a") @@ -130,3 +130,24 @@ def test_refine_compatibility(x): assert ( refine(Abs(x), combined) == x ), "Abs(x) should simpify to x when real and positive" + + +def test_explicit_relational_classes(x, y): + """Test "Gt", "Lt", "Ge", "Le" functions/classes""" + assert sympy_expr_to_predicate(Gt(x, 0)) == Q.positive(x) + assert sympy_expr_to_predicate(Lt(x, 0)) == Q.negative(x) + assert sympy_expr_to_predicate(Ge(x, 0)) == Q.nonnegative(x) + assert sympy_expr_to_predicate(Le(x, 0)) == Q.nonpositive(x) + + # General relational expressions with two symbols + assert sympy_expr_to_predicate(Gt(x, y)) == Q.positive(x - y) + assert sympy_expr_to_predicate(Lt(x, y)) == Q.positive(y - x) + assert sympy_expr_to_predicate(Ge(x, y)) == Q.nonnegative(x - y) + assert sympy_expr_to_predicate(Le(x, y)) == Q.nonnegative(y - x) + + +def test_explicit_not_class(x): + """Test "Not" instantiated explicitly as a class wrapper""" + assert sympy_expr_to_predicate(Not(Gt(x, 0))) == Q.nonpositive(x) + assert sympy_expr_to_predicate(Not(Le(x, 0))) == Q.positive(x) + assert sympy_expr_to_predicate(Not(Contains(x, S.Integers))) == ~Q.integer(x)