src: Rewritten and moved _Substitution to an extra module substitution.py. There is a working cython variant subtitution.pyx, which is not used.

Author: thomas-sturm

Makefile

@@ -4,14 +4,17 @@ ignores = --ignore=logic1/theories/RCF/test_simplify_motor_redlog.txt
 .PHONY: pytest pytest-full test-doc mypy test test-all doc pygount\
 		coverage coverage_html clean veryclean conda-build
 
+cython:
+	python setup.py build_ext --inplace
+
 pytest:
-	pytest -n 8 --exitfirst --doctest-modules $(ignores)
+	pytest -n 8 --doctest-cython --exitfirst --doctest-modules $(ignores)
 
 pytest-fast:
 	PYTHONOPTIMIZE=TRUE pytest -n 8 --disable-warnings --exitfirst --doctest-modules $(ignores)
 
 pytest-seq:
-	pytest --exitfirst --doctest-modules $(ignores)
+	pytest --doctest-cython --exitfirst --doctest-modules $(ignores)
 
 pytest-full:
 	pytest -n 8 --doctest-modules $(ignores)

cython.yaml

@@ -0,0 +1,19 @@
+# A conda environment for running and developing cython module within Logic1
+#
+# You might want to adapt the name to your preferences.
+#
+# Install and activate as follows:
+#   $ conda env create -f cython.yaml
+#   $ conda activate cython
+#
+# Further packages can be added interactively anytime later on.
+#
+# https://docs.conda.io/projects/conda/en/stable/user-guide/tasks/manage-environments.html
+#
+name: cython
+channels:
+  - conda-forge
+dependencies:
+  - python=3.11
+  - cython
+  - clang

logic1/abc/simplify.py

@@ -152,13 +152,12 @@ def is_valid(self, f: Formula[α, τ, χ, σ], assume: Iterable[α] = []) -> Opt
           simplifying `f` to :data:`.T` or :data:`.F`, respectively. Returns
           :data:`None` in the sense of "don't know" otherwise.
         """
-        match self.simplify(f, assume):
-            case _T():
-                return True
-            case _F():
-                return False
-            case _:
-                return None
+        f = self.simplify(f, assume)
+        if f is _T():
+            return True
+        if f is _F():
+            return False
+        return None
 
     def _post_process(self, f: Formula[α, τ, χ, σ]) -> Formula[α, τ, χ, σ]:
         """A hook for post-processing the final result in subclasses.
@@ -216,6 +215,16 @@ def _simpl_and_or(self, f: And[α, τ, χ, σ] | Or[α, τ, χ, σ], ir: ρ) ->
         """Simplify the negation normal form `f`, which starts with either
         :class:`.And` or :class:`.Or`, modulo `ir`.
         """
+
+        # def log(msg: str):
+        #     from IPython.lib import pretty
+        #     print('+' + (78 - len(msg)) * '-' + ' ' + msg)
+        #     pretty_f = pretty.pretty(f, newline='\n|   ')
+        #     pretty_nodes = pretty.pretty(ir._subst.nodes, newline='\n| ' + len('ir._subst.nodes=') * ' ')
+        #     pretty_ref_nodes = pretty.pretty(ref._subst.nodes, newline='\n| ' + len('ref._subst.nodes=') * ' ')
+        #     print(f'| f={pretty_f}\n| {ir._knowl=!s}\n| ir._subst.nodes={pretty_nodes}\n| {ref._knowl=!s}\n| ref._subst.nodes={pretty_ref_nodes}')
+        #     print('+' + 79 * '-')
+
         ref = ir
         ir = ir.next_()
         gand = f.op
@@ -295,13 +304,11 @@ def _simpl_atomic(self, atom: α, ir: ρ) -> Formula[α, τ, χ, σ]:
         except ir.Inconsistent:
             return _F()
         final_atoms = list(ir.extract(And, ref))
-        match len(final_atoms):
-            case 0:
-                return _T()
-            case 1:
-                return final_atoms[0]
-            case _:
-                assert False, final_atoms
+        if len(final_atoms) == 0:
+            return _T()
+        if len(final_atoms) == 1:
+            return final_atoms[0]
+        assert False, final_atoms
 
     def _simpl_quantified(self, f: QuantifiedFormula[α, τ, χ, σ], ir: ρ) -> Formula[α, τ, χ, σ]:
         """Simplify the negation normal form `f`, which starts with either

logic1/firstorder/formula.py

@@ -5,6 +5,8 @@
 from typing import Any, Callable, Final, Generic, Iterable, Iterator, Optional, Self, TypeVar
 from typing_extensions import TypeIs
 
+from IPython.lib import pretty
+
 from ..support.tracing import trace  # noqa
 
 
@@ -791,6 +793,16 @@ def _repr_latex_(self) -> str:
             as_latex += '{}\\dots'
         return f'$\\displaystyle {as_latex}$'
 
+    def _repr_pretty_(self, p: pretty.RepresentationPrinter, cycle: bool) -> None:
+        assert not cycle
+        op = self.__class__.__name__
+        with p.group(len(op) + 1, op + '(', ')'):
+            for idx, arg in enumerate(self.args):
+                if idx:
+                    p.text(',')
+                    p.breakable()
+                p.pretty(arg)
+
     def simplify(self) -> Formula[α, τ, χ, σ]:
         """Fast basic simplification. The result is equivalent to `self`. The
         following first-order simplifications are applied:

logic1/theories/RCF/simplify.py

@@ -15,7 +15,8 @@
 
 from ... import abc
 from ...firstorder import And, _F, Not, Or, _T
-from .atomic import AtomicFormula, DEFINITE, Eq, Ge, Le, Gt, Lt, Ne, SortKey, Term, Variable
+from .atomic import AtomicFormula, DEFINITE, Eq, Ge, Le, Gt, Lt, Ne, Term, Variable
+from .substitution import _SubstValue, _Substitution  # type: ignore
 from .typing import Formula
 
 from ...support.tracing import trace  # noqa
@@ -65,10 +66,17 @@ def __post_init__(self) -> None:
         assert self.ropen or self.end is not oo, self
         assert all(self.start < x < self.end for x in self.exc), self
 
-    def __str__(self):
+    def __str__(self) -> str:
         left = '(' if self.lopen else '['
+        start = '-oo' if self.start == -oo else str(self.start)
+        end = 'oo' if self.end == oo else str(self.end)
         right = ')' if self.ropen else ']'
-        return f'{left}{self.start}, {self.end}{right} \\ {self.exc}'
+        exc_entries = {str(q) for q in self.exc}
+        if exc_entries:
+            exc = f' \\ {{{", ".join(exc_entries)}}}'
+        else:
+            exc = ''
+        return f'{left}{start}, {end}{right}{exc}'
 
     def intersection(self, other: Self) -> Self:
         if self.start < other.start:
@@ -128,113 +136,6 @@ def transform(self, scale: mpq, shift: mpq) -> Self:
         return self.__class__(lopen, start, end, ropen, exc)
 
 
-@dataclass(frozen=True)
-class _SubstValue:
-    coefficient: mpq
-    variable: Optional[Variable]
-
-    def __eq__(self, other: Self) -> bool:  # type: ignore[override]
-        if self.coefficient != other.coefficient:
-            return False
-        if self.variable is None and other.variable is None:
-            return True
-        if self.variable is None or other.variable is None:
-            return False
-        return self.variable.sort_key() == other.variable.sort_key()
-
-    def __post_init__(self) -> None:
-        assert self.coefficient != 0 or self.variable is None
-
-    @lru_cache(maxsize=CACHE_SIZE)
-    def as_term(self) -> Term:
-        if self.variable is None:
-            return Term(self.coefficient)
-        else:
-            return self.coefficient * self.variable
-
-
-@dataclass(unsafe_hash=True)
-class _Substitution:
-    parents: dict[SortKey[Variable], _SubstValue] = field(default_factory=dict)
-
-    def __iter__(self) -> Iterator[tuple[Variable, _SubstValue]]:
-        for key in self.parents:
-            yield key.term, self.internal_find(key.term)
-
-    def as_gb(self, ignore: Optional[Variable] = None) -> list[Term]:
-        """Convert this :class:._Substitution` into a Gröbner basis that can be
-        used as an argument to reduction methods.
-        """
-        G = []
-        for var, val in self:
-            if ignore is None or var.sort_key() != ignore.sort_key():
-                G.append(var - val.as_term())
-        return G
-
-    def copy(self) -> Self:
-        return self.__class__(self.parents.copy())
-
-    def find(self, v: Variable) -> _SubstValue:
-        return self.internal_find(v)
-
-    def internal_find(self, v: Optional[Variable]) -> _SubstValue:
-        if v is None:
-            return _SubstValue(mpq(1), None)
-        sort_key = Variable.sort_key(v)
-        try:
-            parent = self.parents[sort_key]
-        except KeyError:
-            return _SubstValue(mpq(1), v)
-        root = self.internal_find(parent.variable)
-        root = _SubstValue(parent.coefficient * root.coefficient, root.variable)
-        self.parents[sort_key] = root
-        return root
-
-    def union(self, val1: _SubstValue, val2: _SubstValue) -> None:
-        root1 = self.internal_find(val1.variable)
-        root2 = self.internal_find(val2.variable)
-        c1 = val1.coefficient * root1.coefficient
-        c2 = val2.coefficient * root2.coefficient
-        if root1.variable is not None and root2.variable is not None:
-            sort_key1 = Variable.sort_key(root1.variable)
-            sort_key2 = Variable.sort_key(root2.variable)
-            if sort_key1 == sort_key2:
-                if c1 != c2:
-                    self.parents[sort_key1] = _SubstValue(mpq(0), None)
-            elif sort_key1 < sort_key2:  # type: ignore
-                self.parents[sort_key2] = _SubstValue(c1 / c2, root1.variable)
-            else:
-                self.parents[sort_key1] = _SubstValue(c2 / c1, root2.variable)
-        elif root1.variable is None and root2.variable is not None:
-            sort_key2 = Variable.sort_key(root2.variable)
-            self.parents[sort_key2] = _SubstValue(c1 / c2, None)
-        elif root1.variable is not None and root2.variable is None:
-            sort_key1 = Variable.sort_key(root1.variable)
-            self.parents[sort_key1] = _SubstValue(c2 / c1, None)
-        else:
-            if c1 != c2:
-                raise InternalRepresentation.Inconsistent()
-
-    def is_redundant(self, val1: _SubstValue, val2: _SubstValue) -> Optional[bool]:
-        """Check if the equation ``val1 == val2`` is redundant modulo self.
-        """
-        root1 = self.internal_find(val1.variable)
-        root2 = self.internal_find(val2.variable)
-        c1 = val1.coefficient * root1.coefficient
-        c2 = val2.coefficient * root2.coefficient
-        if root1.variable is None and root2.variable is None:
-            return c1 == c2
-        if root1.variable is None or root2.variable is None:
-            return None
-        if root1.variable == root2.variable and c1 == c2:
-            return True
-        else:
-            return None
-
-    def equations(self) -> Iterator[Eq]:
-        raise NotImplementedError()
-
-
 @dataclass
 class _BasicKnowledge:
 
@@ -429,6 +330,10 @@ def __iter__(self) -> Iterator[_BasicKnowledge]:
         for t, range_ in self.dict_.items():
             yield _BasicKnowledge(t, range_)
 
+    def __str__(self) -> str:
+        entries = [str(key) + ' in ' + str(range) for key, range in self.dict_.items()]
+        return f'{{{", ".join(entries)}}}'
+
     def add(self, bknowl: _BasicKnowledge) -> None:
         bknowl = self.prune(bknowl)
         self.dict_[bknowl.term] = bknowl.range
@@ -638,18 +543,18 @@ def create_initial_representation(self, assume: Iterable[AtomicFormula]) \
         ir = InternalRepresentation(_options=self._options)
         for atom in assume:
             simplified_atom = self._simpl_at(atom, And, explode_always=False)
-            match simplified_atom:
-                case AtomicFormula():
-                    ir.add(And, [simplified_atom])
-                case And(args=args):
-                    assert all(isinstance(arg, AtomicFormula) for arg in args)
-                    ir.add(And, args)
-                case _T():
-                    continue
-                case _F():
-                    raise InternalRepresentation.Inconsistent()
-                case _:
-                    assert False, simplified_atom
+            if Formula.is_atomic(simplified_atom):
+                ir.add(And, [simplified_atom])
+            elif Formula.is_and(simplified_atom):
+                args = simplified_atom.args
+                assert all(isinstance(arg, AtomicFormula) for arg in args)
+                ir.add(And, args)
+            elif Formula.is_true(simplified_atom):
+                continue
+            elif Formula.is_false(simplified_atom):
+                raise InternalRepresentation.Inconsistent()
+            else:
+                assert False, simplified_atom
         return ir
 
     def _post_process(self, f: Formula) -> Formula: