Add files using upload-large-folder tool

.gitattributes

@@ -33,3 +33,7 @@ phivenv/Lib/site-packages/numpy/ma/tests/__pycache__/test_core.cpython-39.pyc fi
 phivenv/Lib/site-packages/numpy/ma/__pycache__/core.cpython-39.pyc filter=lfs diff=lfs merge=lfs -text
 phivenv/Lib/site-packages/numpy/random/bit_generator.cp39-win_amd64.pyd filter=lfs diff=lfs merge=lfs -text
 phivenv/Lib/site-packages/numpy/random/mtrand.cp39-win_amd64.pyd filter=lfs diff=lfs merge=lfs -text
+phivenv/Lib/site-packages/numpy/random/_common.cp39-win_amd64.pyd filter=lfs diff=lfs merge=lfs -text
+phivenv/Lib/site-packages/numpy/random/_bounded_integers.cp39-win_amd64.pyd filter=lfs diff=lfs merge=lfs -text
+phivenv/Lib/site-packages/numpy/random/lib/npyrandom.lib filter=lfs diff=lfs merge=lfs -text
+phivenv/Lib/site-packages/numpy/random/_generator.cp39-win_amd64.pyd filter=lfs diff=lfs merge=lfs -text

phivenv/Lib/site-packages/numpy/random/_bounded_integers.cp39-win_amd64.pyd

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:5e38cea16c127bbfb7291b60468e9500f45bbdc6b63f83d3240109d02fd00e44
+size 252928

phivenv/Lib/site-packages/numpy/random/_common.cp39-win_amd64.pyd

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:a4eceb8cd34b3ecf695c4252df85452c31f3e4e0a2cb43cfc62f70f21e35d46c
+size 176640

phivenv/Lib/site-packages/numpy/random/_generator.cp39-win_amd64.pyd

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:0831522b7e15b6b0888586a5bb296d093c4f771b314ec812caa261f96189d464
+size 754688

phivenv/Lib/site-packages/numpy/random/lib/npyrandom.lib

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:6046451e469e3f9257f302b8a7b90e1fe9c20b4635113e0ab4497da3e36dc71f
+size 147796

phivenv/Lib/site-packages/sympy/logic/algorithms/dpll2.py

@@ -0,0 +1,688 @@
+"""Implementation of DPLL algorithm
+
+Features:
+  - Clause learning
+  - Watch literal scheme
+  - VSIDS heuristic
+
+References:
+  - https://en.wikipedia.org/wiki/DPLL_algorithm
+"""
+
+from collections import defaultdict
+from heapq import heappush, heappop
+
+from sympy.core.sorting import ordered
+from sympy.assumptions.cnf import EncodedCNF
+
+from sympy.logic.algorithms.lra_theory import LRASolver
+
+
+def dpll_satisfiable(expr, all_models=False, use_lra_theory=False):
+    """
+    Check satisfiability of a propositional sentence.
+    It returns a model rather than True when it succeeds.
+    Returns a generator of all models if all_models is True.
+
+    Examples
+    ========
+
+    >>> from sympy.abc import A, B
+    >>> from sympy.logic.algorithms.dpll2 import dpll_satisfiable
+    >>> dpll_satisfiable(A & ~B)
+    {A: True, B: False}
+    >>> dpll_satisfiable(A & ~A)
+    False
+
+    """
+    if not isinstance(expr, EncodedCNF):
+        exprs = EncodedCNF()
+        exprs.add_prop(expr)
+        expr = exprs
+
+    # Return UNSAT when False (encoded as 0) is present in the CNF
+    if {0} in expr.data:
+        if all_models:
+            return (f for f in [False])
+        return False
+
+    if use_lra_theory:
+        lra, immediate_conflicts = LRASolver.from_encoded_cnf(expr)
+    else:
+        lra = None
+        immediate_conflicts = []
+    solver = SATSolver(expr.data + immediate_conflicts, expr.variables, set(), expr.symbols, lra_theory=lra)
+    models = solver._find_model()
+
+    if all_models:
+        return _all_models(models)
+
+    try:
+        return next(models)
+    except StopIteration:
+        return False
+
+    # Uncomment to confirm the solution is valid (hitting set for the clauses)
+    #else:
+        #for cls in clauses_int_repr:
+            #assert solver.var_settings.intersection(cls)
+
+
+def _all_models(models):
+    satisfiable = False
+    try:
+        while True:
+            yield next(models)
+            satisfiable = True
+    except StopIteration:
+        if not satisfiable:
+            yield False
+
+
+class SATSolver:
+    """
+    Class for representing a SAT solver capable of
+     finding a model to a boolean theory in conjunctive
+     normal form.
+    """
+
+    def __init__(self, clauses, variables, var_settings, symbols=None,
+                heuristic='vsids', clause_learning='none', INTERVAL=500,
+                 lra_theory = None):
+
+        self.var_settings = var_settings
+        self.heuristic = heuristic
+        self.is_unsatisfied = False
+        self._unit_prop_queue = []
+        self.update_functions = []
+        self.INTERVAL = INTERVAL
+
+        if symbols is None:
+            self.symbols = list(ordered(variables))
+        else:
+            self.symbols = symbols
+
+        self._initialize_variables(variables)
+        self._initialize_clauses(clauses)
+
+        if 'vsids' == heuristic:
+            self._vsids_init()
+            self.heur_calculate = self._vsids_calculate
+            self.heur_lit_assigned = self._vsids_lit_assigned
+            self.heur_lit_unset = self._vsids_lit_unset
+            self.heur_clause_added = self._vsids_clause_added
+
+            # Note: Uncomment this if/when clause learning is enabled
+            #self.update_functions.append(self._vsids_decay)
+
+        else:
+            raise NotImplementedError
+
+        if 'simple' == clause_learning:
+            self.add_learned_clause = self._simple_add_learned_clause
+            self.compute_conflict = self._simple_compute_conflict
+            self.update_functions.append(self._simple_clean_clauses)
+        elif 'none' == clause_learning:
+            self.add_learned_clause = lambda x: None
+            self.compute_conflict = lambda: None
+        else:
+            raise NotImplementedError
+
+        # Create the base level
+        self.levels = [Level(0)]
+        self._current_level.varsettings = var_settings
+
+        # Keep stats
+        self.num_decisions = 0
+        self.num_learned_clauses = 0
+        self.original_num_clauses = len(self.clauses)
+
+        self.lra = lra_theory
+
+    def _initialize_variables(self, variables):
+        """Set up the variable data structures needed."""
+        self.sentinels = defaultdict(set)
+        self.occurrence_count = defaultdict(int)
+        self.variable_set = [False] * (len(variables) + 1)
+
+    def _initialize_clauses(self, clauses):
+        """Set up the clause data structures needed.
+
+        For each clause, the following changes are made:
+        - Unit clauses are queued for propagation right away.
+        - Non-unit clauses have their first and last literals set as sentinels.
+        - The number of clauses a literal appears in is computed.
+        """
+        self.clauses = [list(clause) for clause in clauses]
+
+        for i, clause in enumerate(self.clauses):
+
+            # Handle the unit clauses
+            if 1 == len(clause):
+                self._unit_prop_queue.append(clause[0])
+                continue
+
+            self.sentinels[clause[0]].add(i)
+            self.sentinels[clause[-1]].add(i)
+
+            for lit in clause:
+                self.occurrence_count[lit] += 1
+
+    def _find_model(self):
+        """
+        Main DPLL loop. Returns a generator of models.
+
+        Variables are chosen successively, and assigned to be either
+        True or False. If a solution is not found with this setting,
+        the opposite is chosen and the search continues. The solver
+        halts when every variable has a setting.
+
+        Examples
+        ========
+
+        >>> from sympy.logic.algorithms.dpll2 import SATSolver
+        >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
+        ... {3, -2}], {1, 2, 3}, set())
+        >>> list(l._find_model())
+        [{1: True, 2: False, 3: False}, {1: True, 2: True, 3: True}]
+
+        >>> from sympy.abc import A, B, C
+        >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
+        ... {3, -2}], {1, 2, 3}, set(), [A, B, C])
+        >>> list(l._find_model())
+        [{A: True, B: False, C: False}, {A: True, B: True, C: True}]
+
+        """
+
+        # We use this variable to keep track of if we should flip a
+        #  variable setting in successive rounds
+        flip_var = False
+
+        # Check if unit prop says the theory is unsat right off the bat
+        self._simplify()
+        if self.is_unsatisfied:
+            return
+
+        # While the theory still has clauses remaining
+        while True:
+            # Perform cleanup / fixup at regular intervals
+            if self.num_decisions % self.INTERVAL == 0:
+                for func in self.update_functions:
+                    func()
+
+            if flip_var:
+                # We have just backtracked and we are trying to opposite literal
+                flip_var = False
+                lit = self._current_level.decision
+
+            else:
+                # Pick a literal to set
+                lit = self.heur_calculate()
+                self.num_decisions += 1
+
+                # Stopping condition for a satisfying theory
+                if 0 == lit:
+
+                    # check if assignment satisfies lra theory
+                    if self.lra:
+                        for enc_var in self.var_settings:
+                            res = self.lra.assert_lit(enc_var)
+                            if res is not None:
+                                break
+                        res = self.lra.check()
+                        self.lra.reset_bounds()
+                    else:
+                        res = None
+                    if res is None or res[0]:
+                        yield {self.symbols[abs(lit) - 1]:
+                                    lit > 0 for lit in self.var_settings}
+                    else:
+                        self._simple_add_learned_clause(res[1])
+
+                        # backtrack until we unassign one of the literals causing the conflict
+                        while not any(-lit in res[1] for lit in self._current_level.var_settings):
+                            self._undo()
+
+                    while self._current_level.flipped:
+                        self._undo()
+                    if len(self.levels) == 1:
+                        return
+                    flip_lit = -self._current_level.decision
+                    self._undo()
+                    self.levels.append(Level(flip_lit, flipped=True))
+                    flip_var = True
+                    continue
+
+                # Start the new decision level
+                self.levels.append(Level(lit))
+
+            # Assign the literal, updating the clauses it satisfies
+            self._assign_literal(lit)
+
+            # _simplify the theory
+            self._simplify()
+
+            # Check if we've made the theory unsat
+            if self.is_unsatisfied:
+
+                self.is_unsatisfied = False
+
+                # We unroll all of the decisions until we can flip a literal
+                while self._current_level.flipped:
+                    self._undo()
+
+                    # If we've unrolled all the way, the theory is unsat
+                    if 1 == len(self.levels):
+                        return
+
+                # Detect and add a learned clause
+                self.add_learned_clause(self.compute_conflict())
+
+                # Try the opposite setting of the most recent decision
+                flip_lit = -self._current_level.decision
+                self._undo()
+                self.levels.append(Level(flip_lit, flipped=True))
+                flip_var = True
+
+    ########################
+    #    Helper Methods    #
+    ########################
+    @property
+    def _current_level(self):
+        """The current decision level data structure
+
+        Examples
+        ========
+
+        >>> from sympy.logic.algorithms.dpll2 import SATSolver
+        >>> l = SATSolver([{1}, {2}], {1, 2}, set())
+        >>> next(l._find_model())
+        {1: True, 2: True}
+        >>> l._current_level.decision
+        0
+        >>> l._current_level.flipped
+        False
+        >>> l._current_level.var_settings
+        {1, 2}
+
+        """
+        return self.levels[-1]
+
+    def _clause_sat(self, cls):
+        """Check if a clause is satisfied by the current variable setting.
+
+        Examples
+        ========
+
+        >>> from sympy.logic.algorithms.dpll2 import SATSolver
+        >>> l = SATSolver([{1}, {-1}], {1}, set())
+        >>> try:
+        ...     next(l._find_model())
+        ... except StopIteration:
+        ...     pass
+        >>> l._clause_sat(0)
+        False
+        >>> l._clause_sat(1)
+        True
+
+        """
+        for lit in self.clauses[cls]:
+            if lit in self.var_settings:
+                return True
+        return False
+
+    def _is_sentinel(self, lit, cls):
+        """Check if a literal is a sentinel of a given clause.
+
+        Examples
+        ========
+
+        >>> from sympy.logic.algorithms.dpll2 import SATSolver
+        >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
+        ... {3, -2}], {1, 2, 3}, set())
+        >>> next(l._find_model())
+        {1: True, 2: False, 3: False}
+        >>> l._is_sentinel(2, 3)
+        True
+        >>> l._is_sentinel(-3, 1)
+        False
+
+        """
+        return cls in self.sentinels[lit]
+
+    def _assign_literal(self, lit):
+        """Make a literal assignment.
+
+        The literal assignment must be recorded as part of the current
+        decision level. Additionally, if the literal is marked as a
+        sentinel of any clause, then a new sentinel must be chosen. If
+        this is not possible, then unit propagation is triggered and
+        another literal is added to the queue to be set in the future.
+
+        Examples
+        ========
+
+        >>> from sympy.logic.algorithms.dpll2 import SATSolver
+        >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
+        ... {3, -2}], {1, 2, 3}, set())
+        >>> next(l._find_model())
+        {1: True, 2: False, 3: False}
+        >>> l.var_settings
+        {-3, -2, 1}
+
+        >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
+        ... {3, -2}], {1, 2, 3}, set())
+        >>> l._assign_literal(-1)
+        >>> try:
+        ...     next(l._find_model())
+        ... except StopIteration:
+        ...     pass
+        >>> l.var_settings
+        {-1}
+
+        """
+        self.var_settings.add(lit)
+        self._current_level.var_settings.add(lit)
+        self.variable_set[abs(lit)] = True
+        self.heur_lit_assigned(lit)
+
+        sentinel_list = list(self.sentinels[-lit])
+
+        for cls in sentinel_list:
+            if not self._clause_sat(cls):
+                other_sentinel = None
+                for newlit in self.clauses[cls]:
+                    if newlit != -lit:
+                        if self._is_sentinel(newlit, cls):
+                            other_sentinel = newlit
+                        elif not self.variable_set[abs(newlit)]:
+                            self.sentinels[-lit].remove(cls)
+                            self.sentinels[newlit].add(cls)
+                            other_sentinel = None
+                            break
+
+                # Check if no sentinel update exists
+                if other_sentinel:
+                    self._unit_prop_queue.append(other_sentinel)
+
+    def _undo(self):
+        """
+        _undo the changes of the most recent decision level.
+
+        Examples
+        ========
+
+        >>> from sympy.logic.algorithms.dpll2 import SATSolver
+        >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
+        ... {3, -2}], {1, 2, 3}, set())
+        >>> next(l._find_model())
+        {1: True, 2: False, 3: False}
+        >>> level = l._current_level
+        >>> level.decision, level.var_settings, level.flipped
+        (-3, {-3, -2}, False)
+        >>> l._undo()
+        >>> level = l._current_level
+        >>> level.decision, level.var_settings, level.flipped
+        (0, {1}, False)
+
+        """
+        # Undo the variable settings
+        for lit in self._current_level.var_settings:
+            self.var_settings.remove(lit)
+            self.heur_lit_unset(lit)
+            self.variable_set[abs(lit)] = False
+
+        # Pop the level off the stack
+        self.levels.pop()
+
+    #########################
+    #      Propagation      #
+    #########################
+    """
+    Propagation methods should attempt to soundly simplify the boolean
+      theory, and return True if any simplification occurred and False
+      otherwise.
+    """
+    def _simplify(self):
+        """Iterate over the various forms of propagation to simplify the theory.
+
+        Examples
+        ========
+
+        >>> from sympy.logic.algorithms.dpll2 import SATSolver
+        >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
+        ... {3, -2}], {1, 2, 3}, set())
+        >>> l.variable_set
+        [False, False, False, False]
+        >>> l.sentinels
+        {-3: {0, 2}, -2: {3, 4}, 2: {0, 3}, 3: {2, 4}}
+
+        >>> l._simplify()
+
+        >>> l.variable_set
+        [False, True, False, False]
+        >>> l.sentinels
+        {-3: {0, 2}, -2: {3, 4}, -1: set(), 2: {0, 3},
+        ...3: {2, 4}}
+
+        """
+        changed = True
+        while changed:
+            changed = False
+            changed |= self._unit_prop()
+            changed |= self._pure_literal()
+
+    def _unit_prop(self):
+        """Perform unit propagation on the current theory."""
+        result = len(self._unit_prop_queue) > 0
+        while self._unit_prop_queue:
+            next_lit = self._unit_prop_queue.pop()
+            if -next_lit in self.var_settings:
+                self.is_unsatisfied = True
+                self._unit_prop_queue = []
+                return False
+            else:
+                self._assign_literal(next_lit)
+
+        return result
+
+    def _pure_literal(self):
+        """Look for pure literals and assign them when found."""
+        return False
+
+    #########################
+    #      Heuristics       #
+    #########################
+    def _vsids_init(self):
+        """Initialize the data structures needed for the VSIDS heuristic."""
+        self.lit_heap = []
+        self.lit_scores = {}
+
+        for var in range(1, len(self.variable_set)):
+            self.lit_scores[var] = float(-self.occurrence_count[var])
+            self.lit_scores[-var] = float(-self.occurrence_count[-var])
+            heappush(self.lit_heap, (self.lit_scores[var], var))
+            heappush(self.lit_heap, (self.lit_scores[-var], -var))
+
+    def _vsids_decay(self):
+        """Decay the VSIDS scores for every literal.
+
+        Examples
+        ========
+
+        >>> from sympy.logic.algorithms.dpll2 import SATSolver
+        >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
+        ... {3, -2}], {1, 2, 3}, set())
+
+        >>> l.lit_scores
+        {-3: -2.0, -2: -2.0, -1: 0.0, 1: 0.0, 2: -2.0, 3: -2.0}
+
+        >>> l._vsids_decay()
+
+        >>> l.lit_scores
+        {-3: -1.0, -2: -1.0, -1: 0.0, 1: 0.0, 2: -1.0, 3: -1.0}
+
+        """
+        # We divide every literal score by 2 for a decay factor
+        #  Note: This doesn't change the heap property
+        for lit in self.lit_scores.keys():
+            self.lit_scores[lit] /= 2.0
+
+    def _vsids_calculate(self):
+        """
+            VSIDS Heuristic Calculation
+
+        Examples
+        ========
+
+        >>> from sympy.logic.algorithms.dpll2 import SATSolver
+        >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
+        ... {3, -2}], {1, 2, 3}, set())
+
+        >>> l.lit_heap
+        [(-2.0, -3), (-2.0, 2), (-2.0, -2), (0.0, 1), (-2.0, 3), (0.0, -1)]
+
+        >>> l._vsids_calculate()
+        -3
+
+        >>> l.lit_heap
+        [(-2.0, -2), (-2.0, 2), (0.0, -1), (0.0, 1), (-2.0, 3)]
+
+        """
+        if len(self.lit_heap) == 0:
+            return 0
+
+        # Clean out the front of the heap as long the variables are set
+        while self.variable_set[abs(self.lit_heap[0][1])]:
+            heappop(self.lit_heap)
+            if len(self.lit_heap) == 0:
+                return 0
+
+        return heappop(self.lit_heap)[1]
+
+    def _vsids_lit_assigned(self, lit):
+        """Handle the assignment of a literal for the VSIDS heuristic."""
+        pass
+
+    def _vsids_lit_unset(self, lit):
+        """Handle the unsetting of a literal for the VSIDS heuristic.
+
+        Examples
+        ========
+
+        >>> from sympy.logic.algorithms.dpll2 import SATSolver
+        >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
+        ... {3, -2}], {1, 2, 3}, set())
+        >>> l.lit_heap
+        [(-2.0, -3), (-2.0, 2), (-2.0, -2), (0.0, 1), (-2.0, 3), (0.0, -1)]
+
+        >>> l._vsids_lit_unset(2)
+
+        >>> l.lit_heap
+        [(-2.0, -3), (-2.0, -2), (-2.0, -2), (-2.0, 2), (-2.0, 3), (0.0, -1),
+        ...(-2.0, 2), (0.0, 1)]
+
+        """
+        var = abs(lit)
+        heappush(self.lit_heap, (self.lit_scores[var], var))
+        heappush(self.lit_heap, (self.lit_scores[-var], -var))
+
+    def _vsids_clause_added(self, cls):
+        """Handle the addition of a new clause for the VSIDS heuristic.
+
+        Examples
+        ========
+
+        >>> from sympy.logic.algorithms.dpll2 import SATSolver
+        >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
+        ... {3, -2}], {1, 2, 3}, set())
+
+        >>> l.num_learned_clauses
+        0
+        >>> l.lit_scores
+        {-3: -2.0, -2: -2.0, -1: 0.0, 1: 0.0, 2: -2.0, 3: -2.0}
+
+        >>> l._vsids_clause_added({2, -3})
+
+        >>> l.num_learned_clauses
+        1
+        >>> l.lit_scores
+        {-3: -1.0, -2: -2.0, -1: 0.0, 1: 0.0, 2: -1.0, 3: -2.0}
+
+        """
+        self.num_learned_clauses += 1
+        for lit in cls:
+            self.lit_scores[lit] += 1
+
+    ########################
+    #   Clause Learning    #
+    ########################
+    def _simple_add_learned_clause(self, cls):
+        """Add a new clause to the theory.
+
+        Examples
+        ========
+
+        >>> from sympy.logic.algorithms.dpll2 import SATSolver
+        >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
+        ... {3, -2}], {1, 2, 3}, set())
+
+        >>> l.num_learned_clauses
+        0
+        >>> l.clauses
+        [[2, -3], [1], [3, -3], [2, -2], [3, -2]]
+        >>> l.sentinels
+        {-3: {0, 2}, -2: {3, 4}, 2: {0, 3}, 3: {2, 4}}
+
+        >>> l._simple_add_learned_clause([3])
+
+        >>> l.clauses
+        [[2, -3], [1], [3, -3], [2, -2], [3, -2], [3]]
+        >>> l.sentinels
+        {-3: {0, 2}, -2: {3, 4}, 2: {0, 3}, 3: {2, 4, 5}}
+
+        """
+        cls_num = len(self.clauses)
+        self.clauses.append(cls)
+
+        for lit in cls:
+            self.occurrence_count[lit] += 1
+
+        self.sentinels[cls[0]].add(cls_num)
+        self.sentinels[cls[-1]].add(cls_num)
+
+        self.heur_clause_added(cls)
+
+    def _simple_compute_conflict(self):
+        """ Build a clause representing the fact that at least one decision made
+        so far is wrong.
+
+        Examples
+        ========
+
+        >>> from sympy.logic.algorithms.dpll2 import SATSolver
+        >>> l = SATSolver([{2, -3}, {1}, {3, -3}, {2, -2},
+        ... {3, -2}], {1, 2, 3}, set())
+        >>> next(l._find_model())
+        {1: True, 2: False, 3: False}
+        >>> l._simple_compute_conflict()
+        [3]
+
+        """
+        return [-(level.decision) for level in self.levels[1:]]
+
+    def _simple_clean_clauses(self):
+        """Clean up learned clauses."""
+        pass
+
+
+class Level:
+    """
+    Represents a single level in the DPLL algorithm, and contains
+    enough information for a sound backtracking procedure.
+    """
+
+    def __init__(self, decision, flipped=False):
+        self.decision = decision
+        self.var_settings = set()
+        self.flipped = flipped

phivenv/Lib/site-packages/sympy/logic/algorithms/lra_theory.py

@@ -0,0 +1,912 @@
+"""Implements "A Fast Linear-Arithmetic Solver for DPLL(T)"
+
+The LRASolver class defined in this file can be used
+in conjunction with a SAT solver to check the
+satisfiability of formulas involving inequalities.
+
+Here's an example of how that would work:
+
+    Suppose you want to check the satisfiability of
+    the following formula:
+
+    >>> from sympy.core.relational import Eq
+    >>> from sympy.abc import x, y
+    >>> f = ((x > 0) | (x < 0)) & (Eq(x, 0) | Eq(y, 1)) & (~Eq(y, 1) | Eq(1, 2))
+
+    First a preprocessing step should be done on f. During preprocessing,
+    f should be checked for any predicates such as `Q.prime` that can't be
+    handled. Also unequality like `~Eq(y, 1)` should be split.
+
+    I should mention that the paper says to split both equalities and
+    unequality, but this implementation only requires that unequality
+    be split.
+
+    >>> f = ((x > 0) | (x < 0)) & (Eq(x, 0) | Eq(y, 1)) & ((y < 1) | (y > 1) | Eq(1, 2))
+
+    Then an LRASolver instance needs to be initialized with this formula.
+
+    >>> from sympy.assumptions.cnf import CNF, EncodedCNF
+    >>> from sympy.assumptions.ask import Q
+    >>> from sympy.logic.algorithms.lra_theory import LRASolver
+    >>> cnf = CNF.from_prop(f)
+    >>> enc = EncodedCNF()
+    >>> enc.add_from_cnf(cnf)
+    >>> lra, conflicts = LRASolver.from_encoded_cnf(enc)
+
+    Any immediate one-lital conflicts clauses will be detected here.
+    In this example, `~Eq(1, 2)` is one such conflict clause. We'll
+    want to add it to `f` so that the SAT solver is forced to
+    assign Eq(1, 2) to False.
+
+    >>> f = f & ~Eq(1, 2)
+
+    Now that the one-literal conflict clauses have been added
+    and an lra object has been initialized, we can pass `f`
+    to a SAT solver. The SAT solver will give us a satisfying
+    assignment such as:
+
+    (1 = 2): False
+    (y = 1): True
+    (y < 1): True
+    (y > 1): True
+    (x = 0): True
+    (x < 0): True
+    (x > 0): True
+
+    Next you would pass this assignment to the LRASolver
+    which will be able to determine that this particular
+    assignment is satisfiable or not.
+
+    Note that since EncodedCNF is inherently non-deterministic,
+    the int each predicate is encoded as is not consistent. As a
+    result, the code below likely does not reflect the assignment
+    given above.
+
+    >>> lra.assert_lit(-1) #doctest: +SKIP
+    >>> lra.assert_lit(2) #doctest: +SKIP
+    >>> lra.assert_lit(3) #doctest: +SKIP
+    >>> lra.assert_lit(4) #doctest: +SKIP
+    >>> lra.assert_lit(5) #doctest: +SKIP
+    >>> lra.assert_lit(6) #doctest: +SKIP
+    >>> lra.assert_lit(7) #doctest: +SKIP
+    >>> is_sat, conflict_or_assignment = lra.check()
+
+    As the particular assignment suggested is not satisfiable,
+    the LRASolver will return unsat and a conflict clause when
+    given that assignment. The conflict clause will always be
+    minimal, but there can be multiple minimal conflict clauses.
+    One possible conflict clause could be `~(x < 0) | ~(x > 0)`.
+
+    We would then add whatever conflict clause is given to
+    `f` to prevent the SAT solver from coming up with an
+    assignment with the same conflicting literals. In this case,
+    the conflict clause `~(x < 0) | ~(x > 0)` would prevent
+    any assignment where both (x < 0) and (x > 0) were both
+    true.
+
+    The SAT solver would then find another assignment
+    and we would check that assignment with the LRASolver
+    and so on. Eventually either a satisfying assignment
+    that the SAT solver and LRASolver agreed on would be found
+    or enough conflict clauses would be added so that the
+    boolean formula was unsatisfiable.
+
+
+This implementation is based on [1]_, which includes a
+detailed explanation of the algorithm and pseudocode
+for the most important functions.
+
+[1]_ also explains how backtracking and theory propagation
+could be implemented to speed up the current implementation,
+but these are not currently implemented.
+
+TODO:
+ - Handle non-rational real numbers
+ - Handle positive and negative infinity
+ - Implement backtracking and theory proposition
+ - Simplify matrix by removing unused variables using Gaussian elimination
+
+References
+==========
+
+.. [1] Dutertre, B., de Moura, L.:
+       A Fast Linear-Arithmetic Solver for DPLL(T)
+       https://link.springer.com/chapter/10.1007/11817963_11
+"""
+from sympy.solvers.solveset import linear_eq_to_matrix
+from sympy.matrices.dense import eye
+from sympy.assumptions import Predicate
+from sympy.assumptions.assume import AppliedPredicate
+from sympy.assumptions.ask import Q
+from sympy.core import Dummy
+from sympy.core.mul import Mul
+from sympy.core.add import Add
+from sympy.core.relational import Eq, Ne
+from sympy.core.sympify import sympify
+from sympy.core.singleton import S
+from sympy.core.numbers import Rational, oo
+from sympy.matrices.dense import Matrix
+
+class UnhandledInput(Exception):
+    """
+    Raised while creating an LRASolver if non-linearity
+    or non-rational numbers are present.
+    """
+
+# predicates that LRASolver understands and makes use of
+ALLOWED_PRED = {Q.eq, Q.gt, Q.lt, Q.le, Q.ge}
+
+# if true ~Q.gt(x, y) implies Q.le(x, y)
+HANDLE_NEGATION = True
+
+class LRASolver():
+    """
+    Linear Arithmetic Solver for DPLL(T) implemented with an algorithm based on
+    the Dual Simplex method. Uses Bland's pivoting rule to avoid cycling.
+
+    References
+    ==========
+
+    .. [1] Dutertre, B., de Moura, L.:
+           A Fast Linear-Arithmetic Solver for DPLL(T)
+           https://link.springer.com/chapter/10.1007/11817963_11
+    """
+
+    def __init__(self, A, slack_variables, nonslack_variables, enc_to_boundary, s_subs, testing_mode):
+        """
+        Use the "from_encoded_cnf" method to create a new LRASolver.
+        """
+        self.run_checks = testing_mode
+        self.s_subs = s_subs  # used only for test_lra_theory.test_random_problems
+
+        if any(not isinstance(a, Rational) for a in A):
+            raise UnhandledInput("Non-rational numbers are not handled")
+        if any(not isinstance(b.bound, Rational) for b in enc_to_boundary.values()):
+            raise UnhandledInput("Non-rational numbers are not handled")
+        m, n = len(slack_variables), len(slack_variables)+len(nonslack_variables)
+        if m != 0:
+            assert A.shape == (m, n)
+        if self.run_checks:
+            assert A[:, n-m:] == -eye(m)
+
+        self.enc_to_boundary = enc_to_boundary  # mapping of int to Boundary objects
+        self.boundary_to_enc = {value: key for key, value in enc_to_boundary.items()}
+        self.A = A
+        self.slack = slack_variables
+        self.nonslack = nonslack_variables
+        self.all_var = nonslack_variables + slack_variables
+
+        self.slack_set = set(slack_variables)
+
+        self.is_sat = True  # While True, all constraints asserted so far are satisfiable
+        self.result = None  # always one of: (True, assignment), (False, conflict clause), None
+
+    @staticmethod
+    def from_encoded_cnf(encoded_cnf, testing_mode=False):
+        """
+        Creates an LRASolver from an EncodedCNF object
+        and a list of conflict clauses for propositions
+        that can be simplified to True or False.
+
+        Parameters
+        ==========
+
+        encoded_cnf : EncodedCNF
+
+        testing_mode : bool
+            Setting testing_mode to True enables some slow assert statements
+            and sorting to reduce nonterministic behavior.
+
+        Returns
+        =======
+
+        (lra, conflicts)
+
+        lra : LRASolver
+
+        conflicts : list
+            Contains a one-literal conflict clause for each proposition
+            that can be simplified to True or False.
+
+        Example
+        =======
+
+        >>> from sympy.core.relational import Eq
+        >>> from sympy.assumptions.cnf import CNF, EncodedCNF
+        >>> from sympy.assumptions.ask import Q
+        >>> from sympy.logic.algorithms.lra_theory import LRASolver
+        >>> from sympy.abc import x, y, z
+        >>> phi = (x >= 0) & ((x + y <= 2) | (x + 2 * y - z >= 6))
+        >>> phi = phi & (Eq(x + y, 2) | (x + 2 * y - z > 4))
+        >>> phi = phi & Q.gt(2, 1)
+        >>> cnf = CNF.from_prop(phi)
+        >>> enc = EncodedCNF()
+        >>> enc.from_cnf(cnf)
+        >>> lra, conflicts = LRASolver.from_encoded_cnf(enc, testing_mode=True)
+        >>> lra #doctest: +SKIP
+        <sympy.logic.algorithms.lra_theory.LRASolver object at 0x7fdcb0e15b70>
+        >>> conflicts #doctest: +SKIP
+        [[4]]
+        """
+        # This function has three main jobs:
+        # - raise errors if the input formula is not handled
+        # - preprocesses the formula into a matrix and single variable constraints
+        # - create one-literal conflict clauses from predicates that are always True
+        #   or always False such as Q.gt(3, 2)
+        #
+        # See the preprocessing section of "A Fast Linear-Arithmetic Solver for DPLL(T)"
+        # for an explanation of how the formula is converted into a matrix
+        # and a set of single variable constraints.
+
+        encoding = {}  # maps int to boundary
+        A = []
+
+        basic = []
+        s_count = 0
+        s_subs = {}
+        nonbasic = []
+
+        if testing_mode:
+            # sort to reduce nondeterminism
+            encoded_cnf_items = sorted(encoded_cnf.encoding.items(), key=lambda x: str(x))
+        else:
+            encoded_cnf_items = encoded_cnf.encoding.items()
+
+        empty_var = Dummy()
+        var_to_lra_var = {}
+        conflicts = []
+
+        for prop, enc in encoded_cnf_items:
+            if isinstance(prop, Predicate):
+                prop = prop(empty_var)
+            if not isinstance(prop, AppliedPredicate):
+                if prop == True:
+                    conflicts.append([enc])
+                    continue
+                if prop == False:
+                    conflicts.append([-enc])
+                    continue
+
+                raise ValueError(f"Unhandled Predicate: {prop}")
+
+            assert prop.function in ALLOWED_PRED
+            if prop.lhs == S.NaN or prop.rhs == S.NaN:
+                raise ValueError(f"{prop} contains nan")
+            if prop.lhs.is_imaginary or prop.rhs.is_imaginary:
+                raise UnhandledInput(f"{prop} contains an imaginary component")
+            if prop.lhs == oo or prop.rhs == oo:
+                raise UnhandledInput(f"{prop} contains infinity")
+
+            prop = _eval_binrel(prop)  # simplify variable-less quantities to True / False if possible
+            if prop == True:
+                conflicts.append([enc])
+                continue
+            elif prop == False:
+                conflicts.append([-enc])
+                continue
+            elif prop is None:
+                raise UnhandledInput(f"{prop} could not be simplified")
+
+            expr = prop.lhs - prop.rhs
+            if prop.function in [Q.ge, Q.gt]:
+                expr = -expr
+
+            # expr should be less than (or equal to) 0
+            # otherwise prop is False
+            if prop.function in [Q.le, Q.ge]:
+                bool = (expr <= 0)
+            elif prop.function in [Q.lt, Q.gt]:
+                bool = (expr < 0)
+            else:
+                assert prop.function == Q.eq
+                bool = Eq(expr, 0)
+
+            if bool == True:
+                conflicts.append([enc])
+                continue
+            elif bool == False:
+                conflicts.append([-enc])
+                continue
+
+
+            vars, const = _sep_const_terms(expr)  # example: (2x + 3y + 2) --> (2x + 3y), (2)
+            vars, var_coeff = _sep_const_coeff(vars)  # examples: (2x) --> (x, 2); (2x + 3y) --> (2x + 3y), (1)
+            const = const / var_coeff
+
+            terms = _list_terms(vars)  # example: (2x + 3y) --> [2x, 3y]
+            for term in terms:
+                term, _ = _sep_const_coeff(term)
+                assert len(term.free_symbols) > 0
+                if term not in var_to_lra_var:
+                    var_to_lra_var[term] = LRAVariable(term)
+                    nonbasic.append(term)
+
+            if len(terms) > 1:
+                if vars not in s_subs:
+                    s_count += 1
+                    d = Dummy(f"s{s_count}")
+                    var_to_lra_var[d] = LRAVariable(d)
+                    basic.append(d)
+                    s_subs[vars] = d
+                    A.append(vars - d)
+                var = s_subs[vars]
+            else:
+                var = terms[0]
+
+            assert var_coeff != 0
+
+            equality = prop.function == Q.eq
+            upper = var_coeff > 0 if not equality else None
+            strict = prop.function in [Q.gt, Q.lt]
+            b = Boundary(var_to_lra_var[var], -const, upper, equality, strict)
+            encoding[enc] = b
+
+        fs = [v.free_symbols for v in nonbasic + basic]
+        assert all(len(syms) > 0 for syms in fs)
+        fs_count = sum(len(syms) for syms in fs)
+        if len(fs) > 0 and  len(set.union(*fs)) < fs_count:
+            raise UnhandledInput("Nonlinearity is not handled")
+
+        A, _ = linear_eq_to_matrix(A, nonbasic + basic)
+        nonbasic = [var_to_lra_var[nb] for nb in nonbasic]
+        basic = [var_to_lra_var[b] for b in basic]
+        for idx, var in enumerate(nonbasic + basic):
+            var.col_idx = idx
+
+        return LRASolver(A, basic, nonbasic, encoding, s_subs, testing_mode), conflicts
+
+    def reset_bounds(self):
+        """
+        Resets the state of the LRASolver to before
+        anything was asserted.
+        """
+        self.result = None
+        for var in self.all_var:
+            var.lower = LRARational(-float("inf"), 0)
+            var.lower_from_eq = False
+            var.lower_from_neg = False
+            var.upper = LRARational(float("inf"), 0)
+            var.upper_from_eq= False
+            var.lower_from_neg = False
+            var.assign = LRARational(0, 0)
+
+    def assert_lit(self, enc_constraint):
+        """
+        Assert a literal representing a constraint
+        and update the internal state accordingly.
+
+        Note that due to peculiarities of this implementation
+        asserting ~(x > 0) will assert (x <= 0) but asserting
+        ~Eq(x, 0) will not do anything.
+
+        Parameters
+        ==========
+
+        enc_constraint : int
+            A mapping of encodings to constraints
+            can be found in `self.enc_to_boundary`.
+
+        Returns
+        =======
+
+        None or (False, explanation)
+
+        explanation : set of ints
+            A conflict clause that "explains" why
+            the literals asserted so far are unsatisfiable.
+        """
+        if abs(enc_constraint) not in self.enc_to_boundary:
+            return None
+
+        if not HANDLE_NEGATION and enc_constraint < 0:
+            return None
+
+        boundary = self.enc_to_boundary[abs(enc_constraint)]
+        sym, c, negated = boundary.var, boundary.bound, enc_constraint < 0
+
+        if boundary.equality and negated:
+            return None # negated equality is not handled and should only appear in conflict clauses
+
+        upper = boundary.upper != negated
+        if boundary.strict != negated:
+            delta = -1 if upper else 1
+            c = LRARational(c, delta)
+        else:
+            c = LRARational(c, 0)
+
+        if boundary.equality:
+            res1 = self._assert_lower(sym, c, from_equality=True, from_neg=negated)
+            if res1 and res1[0] == False:
+                res = res1
+            else:
+                res2 = self._assert_upper(sym, c, from_equality=True, from_neg=negated)
+                res =  res2
+        elif upper:
+            res = self._assert_upper(sym, c, from_neg=negated)
+        else:
+            res = self._assert_lower(sym, c, from_neg=negated)
+
+        if self.is_sat and sym not in self.slack_set:
+            self.is_sat = res is None
+        else:
+            self.is_sat = False
+
+        return res
+
+    def _assert_upper(self, xi, ci, from_equality=False, from_neg=False):
+        """
+        Adjusts the upper bound on variable xi if the new upper bound is
+        more limiting. The assignment of variable xi is adjusted to be
+        within the new bound if needed.
+
+        Also calls `self._update` to update the assignment for slack variables
+        to keep all equalities satisfied.
+        """
+        if self.result:
+            assert self.result[0] != False
+        self.result = None
+        if ci >= xi.upper:
+            return None
+        if ci < xi.lower:
+            assert (xi.lower[1] >= 0) is True
+            assert (ci[1] <= 0) is True
+
+            lit1, neg1 = Boundary.from_lower(xi)
+
+            lit2 = Boundary(var=xi, const=ci[0], strict=ci[1] != 0, upper=True, equality=from_equality)
+            if from_neg:
+                lit2 = lit2.get_negated()
+            neg2 = -1 if from_neg else 1
+
+            conflict = [-neg1*self.boundary_to_enc[lit1], -neg2*self.boundary_to_enc[lit2]]
+            self.result = False, conflict
+            return self.result
+        xi.upper = ci
+        xi.upper_from_eq = from_equality
+        xi.upper_from_neg = from_neg
+        if xi in self.nonslack and xi.assign > ci:
+            self._update(xi, ci)
+
+        if self.run_checks and all(v.assign[0] != float("inf") and v.assign[0] != -float("inf")
+                                   for v in self.all_var):
+            M = self.A
+            X = Matrix([v.assign[0] for v in self.all_var])
+            assert all(abs(val) < 10 ** (-10) for val in M * X)
+
+        return None
+
+    def _assert_lower(self, xi, ci, from_equality=False, from_neg=False):
+        """
+        Adjusts the lower bound on variable xi if the new lower bound is
+        more limiting. The assignment of variable xi is adjusted to be
+        within the new bound if needed.
+
+        Also calls `self._update` to update the assignment for slack variables
+        to keep all equalities satisfied.
+        """
+        if self.result:
+            assert self.result[0] != False
+        self.result = None
+        if ci <= xi.lower:
+            return None
+        if ci > xi.upper:
+            assert (xi.upper[1] <= 0) is True
+            assert (ci[1] >= 0) is True
+
+            lit1, neg1 = Boundary.from_upper(xi)
+
+            lit2 = Boundary(var=xi, const=ci[0], strict=ci[1] != 0, upper=False, equality=from_equality)
+            if from_neg:
+                lit2 = lit2.get_negated()
+            neg2 = -1 if from_neg else 1
+
+            conflict = [-neg1*self.boundary_to_enc[lit1],-neg2*self.boundary_to_enc[lit2]]
+            self.result = False, conflict
+            return self.result
+        xi.lower = ci
+        xi.lower_from_eq = from_equality
+        xi.lower_from_neg = from_neg
+        if xi in self.nonslack and xi.assign < ci:
+            self._update(xi, ci)
+
+        if self.run_checks and all(v.assign[0] != float("inf") and v.assign[0] != -float("inf")
+                                   for v in self.all_var):
+            M = self.A
+            X = Matrix([v.assign[0] for v in self.all_var])
+            assert all(abs(val) < 10 ** (-10) for val in M * X)
+
+        return None
+
+    def _update(self, xi, v):
+        """
+        Updates all slack variables that have equations that contain
+        variable xi so that they stay satisfied given xi is equal to v.
+        """
+        i = xi.col_idx
+        for j, b in enumerate(self.slack):
+            aji = self.A[j, i]
+            b.assign = b.assign + (v - xi.assign)*aji
+        xi.assign = v
+
+    def check(self):
+        """
+        Searches for an assignment that satisfies all constraints
+        or determines that no such assignment exists and gives
+        a minimal conflict clause that "explains" why the
+        constraints are unsatisfiable.
+
+        Returns
+        =======
+
+        (True, assignment) or (False, explanation)
+
+        assignment : dict of LRAVariables to values
+            Assigned values are tuples that represent a rational number
+            plus some infinatesimal delta.
+
+        explanation : set of ints
+        """
+        if self.is_sat:
+            return True, {var: var.assign for var in self.all_var}
+        if self.result:
+            return self.result
+
+        from sympy.matrices.dense import Matrix
+        M = self.A.copy()
+        basic = {s: i for i, s in enumerate(self.slack)}  # contains the row index associated with each basic variable
+        nonbasic = set(self.nonslack)
+        while True:
+            if self.run_checks:
+                # nonbasic variables must always be within bounds
+                assert all(((nb.assign >= nb.lower) == True) and ((nb.assign <= nb.upper) == True) for nb in nonbasic)
+
+                # assignments for x must always satisfy Ax = 0
+                # probably have to turn this off when dealing with strict ineq
+                if all(v.assign[0] != float("inf") and v.assign[0] != -float("inf")
+                                   for v in self.all_var):
+                    X = Matrix([v.assign[0] for v in self.all_var])
+                    assert all(abs(val) < 10**(-10) for val in M*X)
+
+                # check upper and lower match this format:
+                # x <= rat + delta iff x < rat
+                # x >= rat - delta iff x > rat
+                # this wouldn't make sense:
+                # x <= rat - delta
+                # x >= rat + delta
+                assert all(x.upper[1] <= 0 for x in self.all_var)
+                assert all(x.lower[1] >= 0 for x in self.all_var)
+
+            cand = [b for b in basic if b.assign < b.lower or b.assign > b.upper]
+
+            if len(cand) == 0:
+                return True, {var: var.assign for var in self.all_var}
+
+            xi = min(cand, key=lambda v: v.col_idx) # Bland's rule
+            i = basic[xi]
+
+            if xi.assign < xi.lower:
+                cand = [nb for nb in nonbasic
+                        if (M[i, nb.col_idx] > 0 and nb.assign < nb.upper)
+                        or (M[i, nb.col_idx] < 0 and nb.assign > nb.lower)]
+                if len(cand) == 0:
+                    N_plus = [nb for nb in nonbasic if M[i, nb.col_idx] > 0]
+                    N_minus = [nb for nb in nonbasic if M[i, nb.col_idx] < 0]
+
+                    conflict = []
+                    conflict += [Boundary.from_upper(nb) for nb in N_plus]
+                    conflict += [Boundary.from_lower(nb) for nb in N_minus]
+                    conflict.append(Boundary.from_lower(xi))
+                    conflict = [-neg*self.boundary_to_enc[c] for c, neg in conflict]
+                    return False, conflict
+                xj = min(cand, key=str)
+                M = self._pivot_and_update(M, basic, nonbasic, xi, xj, xi.lower)
+
+            if xi.assign > xi.upper:
+                cand = [nb for nb in nonbasic
+                        if (M[i, nb.col_idx] < 0 and nb.assign < nb.upper)
+                        or (M[i, nb.col_idx] > 0 and nb.assign > nb.lower)]
+
+                if len(cand) == 0:
+                    N_plus = [nb for nb in nonbasic if M[i, nb.col_idx] > 0]
+                    N_minus = [nb for nb in nonbasic if M[i, nb.col_idx] < 0]
+
+                    conflict = []
+                    conflict += [Boundary.from_upper(nb) for nb in N_minus]
+                    conflict += [Boundary.from_lower(nb) for nb in N_plus]
+                    conflict.append(Boundary.from_upper(xi))
+
+                    conflict = [-neg*self.boundary_to_enc[c] for c, neg in conflict]
+                    return False, conflict
+                xj = min(cand, key=lambda v: v.col_idx)
+                M = self._pivot_and_update(M, basic, nonbasic, xi, xj, xi.upper)
+
+    def _pivot_and_update(self, M, basic, nonbasic, xi, xj, v):
+        """
+        Pivots basic variable xi with nonbasic variable xj,
+        and sets value of xi to v and adjusts the values of all basic variables
+        to keep equations satisfied.
+        """
+        i, j = basic[xi], xj.col_idx
+        assert M[i, j] != 0
+        theta = (v - xi.assign)*(1/M[i, j])
+        xi.assign = v
+        xj.assign = xj.assign + theta
+        for xk in basic:
+            if xk != xi:
+                k = basic[xk]
+                akj = M[k, j]
+                xk.assign = xk.assign + theta*akj
+        # pivot
+        basic[xj] = basic[xi]
+        del basic[xi]
+        nonbasic.add(xi)
+        nonbasic.remove(xj)
+        return self._pivot(M, i, j)
+
+    @staticmethod
+    def _pivot(M, i, j):
+        """
+        Performs a pivot operation about entry i, j of M by performing
+        a series of row operations on a copy of M and returning the result.
+        The original M is left unmodified.
+
+        Conceptually, M represents a system of equations and pivoting
+        can be thought of as rearranging equation i to be in terms of
+        variable j and then substituting in the rest of the equations
+        to get rid of other occurances of variable j.
+
+        Example
+        =======
+
+        >>> from sympy.matrices.dense import Matrix
+        >>> from sympy.logic.algorithms.lra_theory import LRASolver
+        >>> from sympy import var
+        >>> Matrix(3, 3, var('a:i'))
+        Matrix([
+        [a, b, c],
+        [d, e, f],
+        [g, h, i]])
+
+        This matrix is equivalent to:
+        0 = a*x + b*y + c*z
+        0 = d*x + e*y + f*z
+        0 = g*x + h*y + i*z
+
+        >>> LRASolver._pivot(_, 1, 0)
+        Matrix([
+        [ 0, -a*e/d + b, -a*f/d + c],
+        [-1,       -e/d,       -f/d],
+        [ 0,  h - e*g/d,  i - f*g/d]])
+
+        We rearrange equation 1 in terms of variable 0 (x)
+        and substitute to remove x from the other equations.
+
+        0 = 0 + (-a*e/d + b)*y + (-a*f/d + c)*z
+        0 = -x + (-e/d)*y + (-f/d)*z
+        0 = 0 + (h - e*g/d)*y + (i - f*g/d)*z
+        """
+        _, _, Mij = M[i, :], M[:, j], M[i, j]
+        if Mij == 0:
+            raise ZeroDivisionError("Tried to pivot about zero-valued entry.")
+        A = M.copy()
+        A[i, :] = -A[i, :]/Mij
+        for row in range(M.shape[0]):
+            if row != i:
+                A[row, :] = A[row, :] + A[row, j] * A[i, :]
+
+        return A
+
+
+def _sep_const_coeff(expr):
+    """
+    Example
+    =======
+
+    >>> from sympy.logic.algorithms.lra_theory import _sep_const_coeff
+    >>> from sympy.abc import x, y
+    >>> _sep_const_coeff(2*x)
+    (x, 2)
+    >>> _sep_const_coeff(2*x + 3*y)
+    (2*x + 3*y, 1)
+    """
+    if isinstance(expr, Add):
+        return expr, sympify(1)
+
+    if isinstance(expr, Mul):
+        coeffs = expr.args
+    else:
+        coeffs = [expr]
+
+    var, const = [], []
+    for c in coeffs:
+        c = sympify(c)
+        if len(c.free_symbols)==0:
+            const.append(c)
+        else:
+            var.append(c)
+    return Mul(*var), Mul(*const)
+
+
+def _list_terms(expr):
+    if not isinstance(expr, Add):
+        return [expr]
+
+    return expr.args
+
+
+def _sep_const_terms(expr):
+    """
+    Example
+    =======
+
+    >>> from sympy.logic.algorithms.lra_theory import _sep_const_terms
+    >>> from sympy.abc import x, y
+    >>> _sep_const_terms(2*x + 3*y + 2)
+    (2*x + 3*y, 2)
+    """
+    if isinstance(expr, Add):
+        terms = expr.args
+    else:
+        terms = [expr]
+
+    var, const = [], []
+    for t in terms:
+        if len(t.free_symbols) == 0:
+            const.append(t)
+        else:
+            var.append(t)
+    return sum(var), sum(const)
+
+
+def _eval_binrel(binrel):
+    """
+    Simplify binary relation to True / False if possible.
+    """
+    if not (len(binrel.lhs.free_symbols) == 0 and len(binrel.rhs.free_symbols) == 0):
+        return binrel
+    if binrel.function == Q.lt:
+        res = binrel.lhs < binrel.rhs
+    elif binrel.function == Q.gt:
+        res = binrel.lhs > binrel.rhs
+    elif binrel.function == Q.le:
+        res = binrel.lhs <= binrel.rhs
+    elif binrel.function == Q.ge:
+        res = binrel.lhs >= binrel.rhs
+    elif binrel.function == Q.eq:
+        res = Eq(binrel.lhs, binrel.rhs)
+    elif binrel.function == Q.ne:
+        res = Ne(binrel.lhs, binrel.rhs)
+
+    if res == True or res == False:
+        return res
+    else:
+        return None
+
+
+class Boundary:
+    """
+    Represents an upper or lower bound or an equality between a symbol
+    and some constant.
+    """
+    def __init__(self, var, const, upper, equality, strict=None):
+        if not equality in [True, False]:
+            assert equality in [True, False]
+
+
+        self.var = var
+        if isinstance(const, tuple):
+            s = const[1] != 0
+            if strict:
+                assert s == strict
+            self.bound = const[0]
+            self.strict = s
+        else:
+            self.bound = const
+            self.strict = strict
+        self.upper = upper if not equality else None
+        self.equality = equality
+        self.strict = strict
+        assert self.strict is not None
+
+    @staticmethod
+    def from_upper(var):
+        neg = -1 if var.upper_from_neg else 1
+        b = Boundary(var, var.upper[0], True, var.upper_from_eq, var.upper[1] != 0)
+        if neg < 0:
+            b = b.get_negated()
+        return b, neg
+
+    @staticmethod
+    def from_lower(var):
+        neg = -1 if var.lower_from_neg else 1
+        b = Boundary(var, var.lower[0], False, var.lower_from_eq, var.lower[1] != 0)
+        if neg < 0:
+            b = b.get_negated()
+        return b, neg
+
+    def get_negated(self):
+        return Boundary(self.var, self.bound, not self.upper, self.equality, not self.strict)
+
+    def get_inequality(self):
+        if self.equality:
+            return Eq(self.var.var, self.bound)
+        elif self.upper and self.strict:
+            return self.var.var < self.bound
+        elif not self.upper and self.strict:
+            return self.var.var > self.bound
+        elif self.upper:
+            return self.var.var <= self.bound
+        else:
+            return self.var.var >= self.bound
+
+    def __repr__(self):
+        return repr("Boundary(" + repr(self.get_inequality()) + ")")
+
+    def __eq__(self, other):
+        other = (other.var, other.bound, other.strict, other.upper, other.equality)
+        return (self.var, self.bound, self.strict, self.upper, self.equality) == other
+
+    def __hash__(self):
+        return hash((self.var, self.bound, self.strict, self.upper, self.equality))
+
+
+class LRARational():
+    """
+    Represents a rational plus or minus some amount
+    of arbitrary small deltas.
+    """
+    def __init__(self, rational, delta):
+        self.value = (rational, delta)
+
+    def __lt__(self, other):
+        return self.value < other.value
+
+    def __le__(self, other):
+        return self.value <= other.value
+
+    def __eq__(self, other):
+        return self.value == other.value
+
+    def __add__(self, other):
+        return LRARational(self.value[0] + other.value[0], self.value[1] + other.value[1])
+
+    def __sub__(self, other):
+        return LRARational(self.value[0] - other.value[0], self.value[1] - other.value[1])
+
+    def __mul__(self, other):
+        assert not isinstance(other, LRARational)
+        return LRARational(self.value[0] * other, self.value[1] * other)
+
+    def __getitem__(self, index):
+        return self.value[index]
+
+    def __repr__(self):
+        return repr(self.value)
+
+
+class LRAVariable():
+    """
+    Object to keep track of upper and lower bounds
+    on `self.var`.
+    """
+    def __init__(self, var):
+        self.upper = LRARational(float("inf"), 0)
+        self.upper_from_eq = False
+        self.upper_from_neg = False
+        self.lower = LRARational(-float("inf"), 0)
+        self.lower_from_eq = False
+        self.lower_from_neg = False
+        self.assign = LRARational(0,0)
+        self.var = var
+        self.col_idx = None
+
+    def __repr__(self):
+        return repr(self.var)
+
+    def __eq__(self, other):
+        if not isinstance(other, LRAVariable):
+            return False
+        return other.var == self.var
+
+    def __hash__(self):
+        return hash(self.var)

phivenv/Lib/site-packages/sympy/logic/algorithms/minisat22_wrapper.py

@@ -0,0 +1,46 @@
+from sympy.assumptions.cnf import EncodedCNF
+
+def minisat22_satisfiable(expr, all_models=False, minimal=False):
+
+    if not isinstance(expr, EncodedCNF):
+        exprs = EncodedCNF()
+        exprs.add_prop(expr)
+        expr = exprs
+
+    from pysat.solvers import Minisat22
+
+    # Return UNSAT when False (encoded as 0) is present in the CNF
+    if {0} in expr.data:
+        if all_models:
+            return (f for f in [False])
+        return False
+
+    r = Minisat22(expr.data)
+
+    if minimal:
+        r.set_phases([-(i+1) for i in range(r.nof_vars())])
+
+    if not r.solve():
+        return False
+
+    if not all_models:
+        return {expr.symbols[abs(lit) - 1]: lit > 0 for lit in r.get_model()}
+
+    else:
+        # Make solutions SymPy compatible by creating a generator
+        def _gen(results):
+            satisfiable = False
+            while results.solve():
+                sol = results.get_model()
+                yield {expr.symbols[abs(lit) - 1]: lit > 0 for lit in sol}
+                if minimal:
+                    results.add_clause([-i for i in sol if i>0])
+                else:
+                    results.add_clause([-i for i in sol])
+                satisfiable = True
+            if not satisfiable:
+                yield False
+            raise StopIteration
+
+
+        return _gen(r)

phivenv/Lib/site-packages/sympy/logic/algorithms/pycosat_wrapper.py

@@ -0,0 +1,41 @@
+from sympy.assumptions.cnf import EncodedCNF
+
+
+def pycosat_satisfiable(expr, all_models=False):
+    import pycosat
+    if not isinstance(expr, EncodedCNF):
+        exprs = EncodedCNF()
+        exprs.add_prop(expr)
+        expr = exprs
+
+    # Return UNSAT when False (encoded as 0) is present in the CNF
+    if {0} in expr.data:
+        if all_models:
+            return (f for f in [False])
+        return False
+
+    if not all_models:
+        r = pycosat.solve(expr.data)
+        result = (r != "UNSAT")
+        if not result:
+            return result
+        return {expr.symbols[abs(lit) - 1]: lit > 0 for lit in r}
+    else:
+        r = pycosat.itersolve(expr.data)
+        result = (r != "UNSAT")
+        if not result:
+            return result
+
+        # Make solutions SymPy compatible by creating a generator
+        def _gen(results):
+            satisfiable = False
+            try:
+                while True:
+                    sol = next(results)
+                    yield {expr.symbols[abs(lit) - 1]: lit > 0 for lit in sol}
+                    satisfiable = True
+            except StopIteration:
+                if not satisfiable:
+                    yield False
+
+        return _gen(r)

phivenv/Lib/site-packages/sympy/logic/algorithms/z3_wrapper.py

@@ -0,0 +1,115 @@
+from sympy.printing.smtlib import smtlib_code
+from sympy.assumptions.assume import AppliedPredicate
+from sympy.assumptions.cnf import EncodedCNF
+from sympy.assumptions.ask import Q
+
+from sympy.core import Add, Mul
+from sympy.core.relational import Equality, LessThan, GreaterThan, StrictLessThan, StrictGreaterThan
+from sympy.functions.elementary.complexes import Abs
+from sympy.functions.elementary.exponential import Pow
+from sympy.functions.elementary.miscellaneous import Min, Max
+from sympy.logic.boolalg import And, Or, Xor, Implies
+from sympy.logic.boolalg import Not, ITE
+from sympy.assumptions.relation.equality import StrictGreaterThanPredicate, StrictLessThanPredicate, GreaterThanPredicate, LessThanPredicate, EqualityPredicate
+from sympy.external import import_module
+
+def z3_satisfiable(expr, all_models=False):
+    if not isinstance(expr, EncodedCNF):
+        exprs = EncodedCNF()
+        exprs.add_prop(expr)
+        expr = exprs
+
+    z3 = import_module("z3")
+    if z3 is None:
+        raise ImportError("z3 is not installed")
+
+    s = encoded_cnf_to_z3_solver(expr, z3)
+
+    res = str(s.check())
+    if res == "unsat":
+        return False
+    elif res == "sat":
+        return z3_model_to_sympy_model(s.model(), expr)
+    else:
+        return None
+
+
+def z3_model_to_sympy_model(z3_model, enc_cnf):
+    rev_enc = {value : key for key, value in enc_cnf.encoding.items()}
+    return {rev_enc[int(var.name()[1:])] : bool(z3_model[var]) for var in z3_model}
+
+
+def clause_to_assertion(clause):
+    clause_strings = [f"d{abs(lit)}" if lit > 0 else f"(not d{abs(lit)})" for lit in clause]
+    return "(assert (or " + " ".join(clause_strings) + "))"
+
+
+def encoded_cnf_to_z3_solver(enc_cnf, z3):
+    def dummify_bool(pred):
+        return False
+        assert isinstance(pred, AppliedPredicate)
+
+        if pred.function in [Q.positive, Q.negative, Q.zero]:
+            return pred
+        else:
+            return False
+
+    s = z3.Solver()
+
+    declarations = [f"(declare-const d{var} Bool)" for var in enc_cnf.variables]
+    assertions = [clause_to_assertion(clause) for clause in enc_cnf.data]
+
+    symbols = set()
+    for pred, enc in enc_cnf.encoding.items():
+        if not isinstance(pred, AppliedPredicate):
+            continue
+        if pred.function not in (Q.gt, Q.lt, Q.ge, Q.le, Q.ne, Q.eq, Q.positive, Q.negative, Q.extended_negative, Q.extended_positive, Q.zero, Q.nonzero, Q.nonnegative, Q.nonpositive, Q.extended_nonzero, Q.extended_nonnegative, Q.extended_nonpositive):
+            continue
+
+        pred_str = smtlib_code(pred, auto_declare=False, auto_assert=False, known_functions=known_functions)
+
+        symbols |= pred.free_symbols
+        pred = pred_str
+        clause = f"(implies d{enc} {pred})"
+        assertion = "(assert " + clause + ")"
+        assertions.append(assertion)
+
+    for sym in symbols:
+        declarations.append(f"(declare-const {sym} Real)")
+
+    declarations = "\n".join(declarations)
+    assertions = "\n".join(assertions)
+    s.from_string(declarations)
+    s.from_string(assertions)
+
+    return s
+
+
+known_functions = {
+            Add: '+',
+            Mul: '*',
+
+            Equality: '=',
+            LessThan: '<=',
+            GreaterThan: '>=',
+            StrictLessThan: '<',
+            StrictGreaterThan: '>',
+
+            EqualityPredicate(): '=',
+            LessThanPredicate(): '<=',
+            GreaterThanPredicate(): '>=',
+            StrictLessThanPredicate(): '<',
+            StrictGreaterThanPredicate(): '>',
+
+            Abs: 'abs',
+            Min: 'min',
+            Max: 'max',
+            Pow: '^',
+
+            And: 'and',
+            Or: 'or',
+            Xor: 'xor',
+            Not: 'not',
+            ITE: 'ite',
+            Implies: '=>',
+        }

phivenv/Lib/site-packages/sympy/logic/tests/test_boolalg.py

@@ -0,0 +1,1367 @@
+from sympy.assumptions.ask import Q
+from sympy.assumptions.refine import refine
+from sympy.core.numbers import oo
+from sympy.core.relational import Equality, Eq, Ne
+from sympy.core.singleton import S
+from sympy.core.symbol import (Dummy, symbols)
+from sympy.functions import Piecewise
+from sympy.functions.elementary.trigonometric import cos, sin
+from sympy.sets.sets import Interval, Union
+from sympy.sets.contains import Contains
+from sympy.simplify.simplify import simplify
+from sympy.logic.boolalg import (
+    And, Boolean, Equivalent, ITE, Implies, Nand, Nor, Not, Or,
+    POSform, SOPform, Xor, Xnor, conjuncts, disjuncts,
+    distribute_or_over_and, distribute_and_over_or,
+    eliminate_implications, is_nnf, is_cnf, is_dnf, simplify_logic,
+    to_nnf, to_cnf, to_dnf, to_int_repr, bool_map, true, false,
+    BooleanAtom, is_literal, term_to_integer,
+    truth_table, as_Boolean, to_anf, is_anf, distribute_xor_over_and,
+    anf_coeffs, ANFform, bool_minterm, bool_maxterm, bool_monomial,
+    _check_pair, _convert_to_varsSOP, _convert_to_varsPOS, Exclusive,
+    gateinputcount)
+from sympy.assumptions.cnf import CNF
+
+from sympy.testing.pytest import raises, XFAIL, slow
+
+from itertools import combinations, permutations, product
+
+A, B, C, D = symbols('A:D')
+a, b, c, d, e, w, x, y, z = symbols('a:e w:z')
+
+
+def test_overloading():
+    """Test that |, & are overloaded as expected"""
+
+    assert A & B == And(A, B)
+    assert A | B == Or(A, B)
+    assert (A & B) | C == Or(And(A, B), C)
+    assert A >> B == Implies(A, B)
+    assert A << B == Implies(B, A)
+    assert ~A == Not(A)
+    assert A ^ B == Xor(A, B)
+
+
+def test_And():
+    assert And() is true
+    assert And(A) == A
+    assert And(True) is true
+    assert And(False) is false
+    assert And(True, True) is true
+    assert And(True, False) is false
+    assert And(False, False) is false
+    assert And(True, A) == A
+    assert And(False, A) is false
+    assert And(True, True, True) is true
+    assert And(True, True, A) == A
+    assert And(True, False, A) is false
+    assert And(1, A) == A
+    raises(TypeError, lambda: And(2, A))
+    assert And(A < 1, A >= 1) is false
+    e = A > 1
+    assert And(e, e.canonical) == e.canonical
+    g, l, ge, le = A > B, B < A, A >= B, B <= A
+    assert And(g, l, ge, le) == And(ge, g)
+    assert {And(*i) for i in permutations((l, g, le, ge))} == {And(ge, g)}
+    assert And(And(Eq(a, 0), Eq(b, 0)), And(Ne(a, 0), Eq(c, 0))) is false
+
+
+def test_Or():
+    assert Or() is false
+    assert Or(A) == A
+    assert Or(True) is true
+    assert Or(False) is false
+    assert Or(True, True) is true
+    assert Or(True, False) is true
+    assert Or(False, False) is false
+    assert Or(True, A) is true
+    assert Or(False, A) == A
+    assert Or(True, False, False) is true
+    assert Or(True, False, A) is true
+    assert Or(False, False, A) == A
+    assert Or(1, A) is true
+    raises(TypeError, lambda: Or(2, A))
+    assert Or(A < 1, A >= 1) is true
+    e = A > 1
+    assert Or(e, e.canonical) == e
+    g, l, ge, le = A > B, B < A, A >= B, B <= A
+    assert Or(g, l, ge, le) == Or(g, ge)
+
+
+def test_Xor():
+    assert Xor() is false
+    assert Xor(A) == A
+    assert Xor(A, A) is false
+    assert Xor(True, A, A) is true
+    assert Xor(A, A, A, A, A) == A
+    assert Xor(True, False, False, A, B) == ~Xor(A, B)
+    assert Xor(True) is true
+    assert Xor(False) is false
+    assert Xor(True, True) is false
+    assert Xor(True, False) is true
+    assert Xor(False, False) is false
+    assert Xor(True, A) == ~A
+    assert Xor(False, A) == A
+    assert Xor(True, False, False) is true
+    assert Xor(True, False, A) == ~A
+    assert Xor(False, False, A) == A
+    assert isinstance(Xor(A, B), Xor)
+    assert Xor(A, B, Xor(C, D)) == Xor(A, B, C, D)
+    assert Xor(A, B, Xor(B, C)) == Xor(A, C)
+    assert Xor(A < 1, A >= 1, B) == Xor(0, 1, B) == Xor(1, 0, B)
+    e = A > 1
+    assert Xor(e, e.canonical) == Xor(0, 0) == Xor(1, 1)
+
+
+def test_rewrite_as_And():
+    expr = x ^ y
+    assert expr.rewrite(And) == (x | y) & (~x | ~y)
+
+
+def test_rewrite_as_Or():
+    expr = x ^ y
+    assert expr.rewrite(Or) == (x & ~y) | (y & ~x)
+
+
+def test_rewrite_as_Nand():
+    expr = (y & z) | (z & ~w)
+    assert expr.rewrite(Nand) == ~(~(y & z) & ~(z & ~w))
+
+
+def test_rewrite_as_Nor():
+    expr = z & (y | ~w)
+    assert expr.rewrite(Nor) == ~(~z | ~(y | ~w))
+
+
+def test_Not():
+    raises(TypeError, lambda: Not(True, False))
+    assert Not(True) is false
+    assert Not(False) is true
+    assert Not(0) is true
+    assert Not(1) is false
+    assert Not(2) is false
+
+
+def test_Nand():
+    assert Nand() is false
+    assert Nand(A) == ~A
+    assert Nand(True) is false
+    assert Nand(False) is true
+    assert Nand(True, True) is false
+    assert Nand(True, False) is true
+    assert Nand(False, False) is true
+    assert Nand(True, A) == ~A
+    assert Nand(False, A) is true
+    assert Nand(True, True, True) is false
+    assert Nand(True, True, A) == ~A
+    assert Nand(True, False, A) is true
+
+
+def test_Nor():
+    assert Nor() is true
+    assert Nor(A) == ~A
+    assert Nor(True) is false
+    assert Nor(False) is true
+    assert Nor(True, True) is false
+    assert Nor(True, False) is false
+    assert Nor(False, False) is true
+    assert Nor(True, A) is false
+    assert Nor(False, A) == ~A
+    assert Nor(True, True, True) is false
+    assert Nor(True, True, A) is false
+    assert Nor(True, False, A) is false
+
+
+def test_Xnor():
+    assert Xnor() is true
+    assert Xnor(A) == ~A
+    assert Xnor(A, A) is true
+    assert Xnor(True, A, A) is false
+    assert Xnor(A, A, A, A, A) == ~A
+    assert Xnor(True) is false
+    assert Xnor(False) is true
+    assert Xnor(True, True) is true
+    assert Xnor(True, False) is false
+    assert Xnor(False, False) is true
+    assert Xnor(True, A) == A
+    assert Xnor(False, A) == ~A
+    assert Xnor(True, False, False) is false
+    assert Xnor(True, False, A) == A
+    assert Xnor(False, False, A) == ~A
+
+
+def test_Implies():
+    raises(ValueError, lambda: Implies(A, B, C))
+    assert Implies(True, True) is true
+    assert Implies(True, False) is false
+    assert Implies(False, True) is true
+    assert Implies(False, False) is true
+    assert Implies(0, A) is true
+    assert Implies(1, 1) is true
+    assert Implies(1, 0) is false
+    assert A >> B == B << A
+    assert (A < 1) >> (A >= 1) == (A >= 1)
+    assert (A < 1) >> (S.One > A) is true
+    assert A >> A is true
+
+
+def test_Equivalent():
+    assert Equivalent(A, B) == Equivalent(B, A) == Equivalent(A, B, A)
+    assert Equivalent() is true
+    assert Equivalent(A, A) == Equivalent(A) is true
+    assert Equivalent(True, True) == Equivalent(False, False) is true
+    assert Equivalent(True, False) == Equivalent(False, True) is false
+    assert Equivalent(A, True) == A
+    assert Equivalent(A, False) == Not(A)
+    assert Equivalent(A, B, True) == A & B
+    assert Equivalent(A, B, False) == ~A & ~B
+    assert Equivalent(1, A) == A
+    assert Equivalent(0, A) == Not(A)
+    assert Equivalent(A, Equivalent(B, C)) != Equivalent(Equivalent(A, B), C)
+    assert Equivalent(A < 1, A >= 1) is false
+    assert Equivalent(A < 1, A >= 1, 0) is false
+    assert Equivalent(A < 1, A >= 1, 1) is false
+    assert Equivalent(A < 1, S.One > A) == Equivalent(1, 1) == Equivalent(0, 0)
+    assert Equivalent(Equality(A, B), Equality(B, A)) is true
+
+
+def test_Exclusive():
+    assert Exclusive(False, False, False) is true
+    assert Exclusive(True, False, False) is true
+    assert Exclusive(True, True, False) is false
+    assert Exclusive(True, True, True) is false
+
+
+def test_equals():
+    assert Not(Or(A, B)).equals(And(Not(A), Not(B))) is True
+    assert Equivalent(A, B).equals((A >> B) & (B >> A)) is True
+    assert ((A | ~B) & (~A | B)).equals((~A & ~B) | (A & B)) is True
+    assert (A >> B).equals(~A >> ~B) is False
+    assert (A >> (B >> A)).equals(A >> (C >> A)) is False
+    raises(NotImplementedError, lambda: (A & B).equals(A > B))
+
+
+def test_simplification_boolalg():
+    """
+    Test working of simplification methods.
+    """
+    set1 = [[0, 0, 1], [0, 1, 1], [1, 0, 0], [1, 1, 0]]
+    set2 = [[0, 0, 0], [0, 1, 0], [1, 0, 1], [1, 1, 1]]
+    assert SOPform([x, y, z], set1) == Or(And(Not(x), z), And(Not(z), x))
+    assert Not(SOPform([x, y, z], set2)) == \
+           Not(Or(And(Not(x), Not(z)), And(x, z)))
+    assert POSform([x, y, z], set1 + set2) is true
+    assert SOPform([x, y, z], set1 + set2) is true
+    assert SOPform([Dummy(), Dummy(), Dummy()], set1 + set2) is true
+
+    minterms = [[0, 0, 0, 1], [0, 0, 1, 1], [0, 1, 1, 1], [1, 0, 1, 1],
+                [1, 1, 1, 1]]
+    dontcares = [[0, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 1]]
+    assert (
+        SOPform([w, x, y, z], minterms, dontcares) ==
+        Or(And(y, z), And(Not(w), Not(x))))
+    assert POSform([w, x, y, z], minterms, dontcares) == And(Or(Not(w), y), z)
+
+    minterms = [1, 3, 7, 11, 15]
+    dontcares = [0, 2, 5]
+    assert (
+        SOPform([w, x, y, z], minterms, dontcares) ==
+        Or(And(y, z), And(Not(w), Not(x))))
+    assert POSform([w, x, y, z], minterms, dontcares) == And(Or(Not(w), y), z)
+
+    minterms = [1, [0, 0, 1, 1], 7, [1, 0, 1, 1],
+                [1, 1, 1, 1]]
+    dontcares = [0, [0, 0, 1, 0], 5]
+    assert (
+        SOPform([w, x, y, z], minterms, dontcares) ==
+        Or(And(y, z), And(Not(w), Not(x))))
+    assert POSform([w, x, y, z], minterms, dontcares) == And(Or(Not(w), y), z)
+
+    minterms = [1, {y: 1, z: 1}]
+    dontcares = [0, [0, 0, 1, 0], 5]
+    assert (
+        SOPform([w, x, y, z], minterms, dontcares) ==
+        Or(And(y, z), And(Not(w), Not(x))))
+    assert POSform([w, x, y, z], minterms, dontcares) == And(Or(Not(w), y), z)
+
+    minterms = [{y: 1, z: 1}, 1]
+    dontcares = [[0, 0, 0, 0]]
+
+    minterms = [[0, 0, 0]]
+    raises(ValueError, lambda: SOPform([w, x, y, z], minterms))
+    raises(ValueError, lambda: POSform([w, x, y, z], minterms))
+
+    raises(TypeError, lambda: POSform([w, x, y, z], ["abcdefg"]))
+
+    # test simplification
+    ans = And(A, Or(B, C))
+    assert simplify_logic(A & (B | C)) == ans
+    assert simplify_logic((A & B) | (A & C)) == ans
+    assert simplify_logic(Implies(A, B)) == Or(Not(A), B)
+    assert simplify_logic(Equivalent(A, B)) == \
+           Or(And(A, B), And(Not(A), Not(B)))
+    assert simplify_logic(And(Equality(A, 2), C)) == And(Equality(A, 2), C)
+    assert simplify_logic(And(Equality(A, 2), A)) == And(Equality(A, 2), A)
+    assert simplify_logic(And(Equality(A, B), C)) == And(Equality(A, B), C)
+    assert simplify_logic(Or(And(Equality(A, 3), B), And(Equality(A, 3), C))) \
+           == And(Equality(A, 3), Or(B, C))
+    b = (~x & ~y & ~z) | (~x & ~y & z)
+    e = And(A, b)
+    assert simplify_logic(e) == A & ~x & ~y
+    raises(ValueError, lambda: simplify_logic(A & (B | C), form='blabla'))
+    assert simplify(Or(x <= y, And(x < y, z))) == (x <= y)
+    assert simplify(Or(x <= y, And(y > x, z))) == (x <= y)
+    assert simplify(Or(x >= y, And(y < x, z))) == (x >= y)
+
+    # Check that expressions with nine variables or more are not simplified
+    # (without the force-flag)
+    a, b, c, d, e, f, g, h, j = symbols('a b c d e f g h j')
+    expr = a & b & c & d & e & f & g & h & j | \
+           a & b & c & d & e & f & g & h & ~j
+    # This expression can be simplified to get rid of the j variables
+    assert simplify_logic(expr) == expr
+
+    # Test dontcare
+    assert simplify_logic((a & b) | c | d, dontcare=(a & b)) == c | d
+
+    # check input
+    ans = SOPform([x, y], [[1, 0]])
+    assert SOPform([x, y], [[1, 0]]) == ans
+    assert POSform([x, y], [[1, 0]]) == ans
+
+    raises(ValueError, lambda: SOPform([x], [[1]], [[1]]))
+    assert SOPform([x], [[1]], [[0]]) is true
+    assert SOPform([x], [[0]], [[1]]) is true
+    assert SOPform([x], [], []) is false
+
+    raises(ValueError, lambda: POSform([x], [[1]], [[1]]))
+    assert POSform([x], [[1]], [[0]]) is true
+    assert POSform([x], [[0]], [[1]]) is true
+    assert POSform([x], [], []) is false
+
+    # check working of simplify
+    assert simplify((A & B) | (A & C)) == And(A, Or(B, C))
+    assert simplify(And(x, Not(x))) == False
+    assert simplify(Or(x, Not(x))) == True
+    assert simplify(And(Eq(x, 0), Eq(x, y))) == And(Eq(x, 0), Eq(y, 0))
+    assert And(Eq(x - 1, 0), Eq(x, y)).simplify() == And(Eq(x, 1), Eq(y, 1))
+    assert And(Ne(x - 1, 0), Ne(x, y)).simplify() == And(Ne(x, 1), Ne(x, y))
+    assert And(Eq(x - 1, 0), Ne(x, y)).simplify() == And(Eq(x, 1), Ne(y, 1))
+    assert And(Eq(x - 1, 0), Eq(x, z + y), Eq(y + x, 0)).simplify(
+    ) == And(Eq(x, 1), Eq(y, -1), Eq(z, 2))
+    assert And(Eq(x - 1, 0), Eq(x + 2, 3)).simplify() == Eq(x, 1)
+    assert And(Ne(x - 1, 0), Ne(x + 2, 3)).simplify() == Ne(x, 1)
+    assert And(Eq(x - 1, 0), Eq(x + 2, 2)).simplify() == False
+    assert And(Ne(x - 1, 0), Ne(x + 2, 2)).simplify(
+    ) == And(Ne(x, 1), Ne(x, 0))
+    assert simplify(Xor(x, ~x)) == True
+
+
+def test_bool_map():
+    """
+    Test working of bool_map function.
+    """
+
+    minterms = [[0, 0, 0, 1], [0, 0, 1, 1], [0, 1, 1, 1], [1, 0, 1, 1],
+                [1, 1, 1, 1]]
+    assert bool_map(Not(Not(a)), a) == (a, {a: a})
+    assert bool_map(SOPform([w, x, y, z], minterms),
+                    POSform([w, x, y, z], minterms)) == \
+           (And(Or(Not(w), y), Or(Not(x), y), z), {x: x, w: w, z: z, y: y})
+    assert bool_map(SOPform([x, z, y], [[1, 0, 1]]),
+                    SOPform([a, b, c], [[1, 0, 1]])) != False
+    function1 = SOPform([x, z, y], [[1, 0, 1], [0, 0, 1]])
+    function2 = SOPform([a, b, c], [[1, 0, 1], [1, 0, 0]])
+    assert bool_map(function1, function2) == \
+           (function1, {y: a, z: b})
+    assert bool_map(Xor(x, y), ~Xor(x, y)) == False
+    assert bool_map(And(x, y), Or(x, y)) is None
+    assert bool_map(And(x, y), And(x, y, z)) is None
+    # issue 16179
+    assert bool_map(Xor(x, y, z), ~Xor(x, y, z)) == False
+    assert bool_map(Xor(a, x, y, z), ~Xor(a, x, y, z)) == False
+
+
+def test_bool_symbol():
+    """Test that mixing symbols with boolean values
+    works as expected"""
+
+    assert And(A, True) == A
+    assert And(A, True, True) == A
+    assert And(A, False) is false
+    assert And(A, True, False) is false
+    assert Or(A, True) is true
+    assert Or(A, False) == A
+
+
+def test_is_boolean():
+    assert isinstance(True, Boolean) is False
+    assert isinstance(true, Boolean) is True
+    assert 1 == True
+    assert 1 != true
+    assert (1 == true) is False
+    assert 0 == False
+    assert 0 != false
+    assert (0 == false) is False
+    assert true.is_Boolean is True
+    assert (A & B).is_Boolean
+    assert (A | B).is_Boolean
+    assert (~A).is_Boolean
+    assert (A ^ B).is_Boolean
+    assert A.is_Boolean != isinstance(A, Boolean)
+    assert isinstance(A, Boolean)
+
+
+def test_subs():
+    assert (A & B).subs(A, True) == B
+    assert (A & B).subs(A, False) is false
+    assert (A & B).subs(B, True) == A
+    assert (A & B).subs(B, False) is false
+    assert (A & B).subs({A: True, B: True}) is true
+    assert (A | B).subs(A, True) is true
+    assert (A | B).subs(A, False) == B
+    assert (A | B).subs(B, True) is true
+    assert (A | B).subs(B, False) == A
+    assert (A | B).subs({A: True, B: True}) is true
+
+
+"""
+we test for axioms of boolean algebra
+see https://en.wikipedia.org/wiki/Boolean_algebra_(structure)
+"""
+
+
+def test_commutative():
+    """Test for commutativity of And and Or"""
+    A, B = map(Boolean, symbols('A,B'))
+
+    assert A & B == B & A
+    assert A | B == B | A
+
+
+def test_and_associativity():
+    """Test for associativity of And"""
+
+    assert (A & B) & C == A & (B & C)
+
+
+def test_or_assicativity():
+    assert ((A | B) | C) == (A | (B | C))
+
+
+def test_double_negation():
+    a = Boolean()
+    assert ~(~a) == a
+
+
+# test methods
+
+def test_eliminate_implications():
+    assert eliminate_implications(Implies(A, B, evaluate=False)) == (~A) | B
+    assert eliminate_implications(
+        A >> (C >> Not(B))) == Or(Or(Not(B), Not(C)), Not(A))
+    assert eliminate_implications(Equivalent(A, B, C, D)) == \
+           (~A | B) & (~B | C) & (~C | D) & (~D | A)
+
+
+def test_conjuncts():
+    assert conjuncts(A & B & C) == {A, B, C}
+    assert conjuncts((A | B) & C) == {A | B, C}
+    assert conjuncts(A) == {A}
+    assert conjuncts(True) == {True}
+    assert conjuncts(False) == {False}
+
+
+def test_disjuncts():
+    assert disjuncts(A | B | C) == {A, B, C}
+    assert disjuncts((A | B) & C) == {(A | B) & C}
+    assert disjuncts(A) == {A}
+    assert disjuncts(True) == {True}
+    assert disjuncts(False) == {False}
+
+
+def test_distribute():
+    assert distribute_and_over_or(Or(And(A, B), C)) == And(Or(A, C), Or(B, C))
+    assert distribute_or_over_and(And(A, Or(B, C))) == Or(And(A, B), And(A, C))
+    assert distribute_xor_over_and(And(A, Xor(B, C))) == Xor(And(A, B), And(A, C))
+
+
+def test_to_anf():
+    x, y, z = symbols('x,y,z')
+    assert to_anf(And(x, y)) == And(x, y)
+    assert to_anf(Or(x, y)) == Xor(x, y, And(x, y))
+    assert to_anf(Or(Implies(x, y), And(x, y), y)) == \
+           Xor(x, True, x & y, remove_true=False)
+    assert to_anf(Or(Nand(x, y), Nor(x, y), Xnor(x, y), Implies(x, y))) == True
+    assert to_anf(Or(x, Not(y), Nor(x, z), And(x, y), Nand(y, z))) == \
+           Xor(True, And(y, z), And(x, y, z), remove_true=False)
+    assert to_anf(Xor(x, y)) == Xor(x, y)
+    assert to_anf(Not(x)) == Xor(x, True, remove_true=False)
+    assert to_anf(Nand(x, y)) == Xor(True, And(x, y), remove_true=False)
+    assert to_anf(Nor(x, y)) == Xor(x, y, True, And(x, y), remove_true=False)
+    assert to_anf(Implies(x, y)) == Xor(x, True, And(x, y), remove_true=False)
+    assert to_anf(Equivalent(x, y)) == Xor(x, y, True, remove_true=False)
+    assert to_anf(Nand(x | y, x >> y), deep=False) == \
+           Xor(True, And(Or(x, y), Implies(x, y)), remove_true=False)
+    assert to_anf(Nor(x ^ y, x & y), deep=False) == \
+           Xor(True, Or(Xor(x, y), And(x, y)), remove_true=False)
+    # issue 25218
+    assert to_anf(x ^ ~(x ^ y ^ ~y)) == False
+
+
+def test_to_nnf():
+    assert to_nnf(true) is true
+    assert to_nnf(false) is false
+    assert to_nnf(A) == A
+    assert to_nnf(A | ~A | B) is true
+    assert to_nnf(A & ~A & B) is false
+    assert to_nnf(A >> B) == ~A | B
+    assert to_nnf(Equivalent(A, B, C)) == (~A | B) & (~B | C) & (~C | A)
+    assert to_nnf(A ^ B ^ C) == \
+           (A | B | C) & (~A | ~B | C) & (A | ~B | ~C) & (~A | B | ~C)
+    assert to_nnf(ITE(A, B, C)) == (~A | B) & (A | C)
+    assert to_nnf(Not(A | B | C)) == ~A & ~B & ~C
+    assert to_nnf(Not(A & B & C)) == ~A | ~B | ~C
+    assert to_nnf(Not(A >> B)) == A & ~B
+    assert to_nnf(Not(Equivalent(A, B, C))) == And(Or(A, B, C), Or(~A, ~B, ~C))
+    assert to_nnf(Not(A ^ B ^ C)) == \
+           (~A | B | C) & (A | ~B | C) & (A | B | ~C) & (~A | ~B | ~C)
+    assert to_nnf(Not(ITE(A, B, C))) == (~A | ~B) & (A | ~C)
+    assert to_nnf((A >> B) ^ (B >> A)) == (A & ~B) | (~A & B)
+    assert to_nnf((A >> B) ^ (B >> A), False) == \
+           (~A | ~B | A | B) & ((A & ~B) | (~A & B))
+    assert ITE(A, 1, 0).to_nnf() == A
+    assert ITE(A, 0, 1).to_nnf() == ~A
+    # although ITE can hold non-Boolean, it will complain if
+    # an attempt is made to convert the ITE to Boolean nnf
+    raises(TypeError, lambda: ITE(A < 1, [1], B).to_nnf())
+
+
+def test_to_cnf():
+    assert to_cnf(~(B | C)) == And(Not(B), Not(C))
+    assert to_cnf((A & B) | C) == And(Or(A, C), Or(B, C))
+    assert to_cnf(A >> B) == (~A) | B
+    assert to_cnf(A >> (B & C)) == (~A | B) & (~A | C)
+    assert to_cnf(A & (B | C) | ~A & (B | C), True) == B | C
+    assert to_cnf(A & B) == And(A, B)
+
+    assert to_cnf(Equivalent(A, B)) == And(Or(A, Not(B)), Or(B, Not(A)))
+    assert to_cnf(Equivalent(A, B & C)) == \
+           (~A | B) & (~A | C) & (~B | ~C | A)
+    assert to_cnf(Equivalent(A, B | C), True) == \
+           And(Or(Not(B), A), Or(Not(C), A), Or(B, C, Not(A)))
+    assert to_cnf(A + 1) == A + 1
+
+
+def test_issue_18904():
+    x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15 = symbols('x1:16')
+    eq = ((x1 & x2 & x3 & x4 & x5 & x6 & x7 & x8 & x9) |
+          (x1 & x2 & x3 & x4 & x5 & x6 & x7 & x10 & x9) |
+          (x1 & x11 & x3 & x12 & x5 & x13 & x14 & x15 & x9))
+    assert is_cnf(to_cnf(eq))
+    raises(ValueError, lambda: to_cnf(eq, simplify=True))
+    for f, t in zip((And, Or), (to_cnf, to_dnf)):
+        eq = f(x1, x2, x3, x4, x5, x6, x7, x8, x9)
+        raises(ValueError, lambda: to_cnf(eq, simplify=True))
+        assert t(eq, simplify=True, force=True) == eq
+
+
+def test_issue_9949():
+    assert is_cnf(to_cnf((b > -5) | (a > 2) & (a < 4)))
+
+
+def test_to_CNF():
+    assert CNF.CNF_to_cnf(CNF.to_CNF(~(B | C))) == to_cnf(~(B | C))
+    assert CNF.CNF_to_cnf(CNF.to_CNF((A & B) | C)) == to_cnf((A & B) | C)
+    assert CNF.CNF_to_cnf(CNF.to_CNF(A >> B)) == to_cnf(A >> B)
+    assert CNF.CNF_to_cnf(CNF.to_CNF(A >> (B & C))) == to_cnf(A >> (B & C))
+    assert CNF.CNF_to_cnf(CNF.to_CNF(A & (B | C) | ~A & (B | C))) == to_cnf(A & (B | C) | ~A & (B | C))
+    assert CNF.CNF_to_cnf(CNF.to_CNF(A & B)) == to_cnf(A & B)
+
+
+def test_to_dnf():
+    assert to_dnf(~(B | C)) == And(Not(B), Not(C))
+    assert to_dnf(A & (B | C)) == Or(And(A, B), And(A, C))
+    assert to_dnf(A >> B) == (~A) | B
+    assert to_dnf(A >> (B & C)) == (~A) | (B & C)
+    assert to_dnf(A | B) == A | B
+
+    assert to_dnf(Equivalent(A, B), True) == \
+           Or(And(A, B), And(Not(A), Not(B)))
+    assert to_dnf(Equivalent(A, B & C), True) == \
+           Or(And(A, B, C), And(Not(A), Not(B)), And(Not(A), Not(C)))
+    assert to_dnf(A + 1) == A + 1
+
+
+def test_to_int_repr():
+    x, y, z = map(Boolean, symbols('x,y,z'))
+
+    def sorted_recursive(arg):
+        try:
+            return sorted(sorted_recursive(x) for x in arg)
+        except TypeError:  # arg is not a sequence
+            return arg
+
+    assert sorted_recursive(to_int_repr([x | y, z | x], [x, y, z])) == \
+           sorted_recursive([[1, 2], [1, 3]])
+    assert sorted_recursive(to_int_repr([x | y, z | ~x], [x, y, z])) == \
+           sorted_recursive([[1, 2], [3, -1]])
+
+
+def test_is_anf():
+    x, y = symbols('x,y')
+    assert is_anf(true) is True
+    assert is_anf(false) is True
+    assert is_anf(x) is True
+    assert is_anf(And(x, y)) is True
+    assert is_anf(Xor(x, y, And(x, y))) is True
+    assert is_anf(Xor(x, y, Or(x, y))) is False
+    assert is_anf(Xor(Not(x), y)) is False
+
+
+def test_is_nnf():
+    assert is_nnf(true) is True
+    assert is_nnf(A) is True
+    assert is_nnf(~A) is True
+    assert is_nnf(A & B) is True
+    assert is_nnf((A & B) | (~A & A) | (~B & B) | (~A & ~B), False) is True
+    assert is_nnf((A | B) & (~A | ~B)) is True
+    assert is_nnf(Not(Or(A, B))) is False
+    assert is_nnf(A ^ B) is False
+    assert is_nnf((A & B) | (~A & A) | (~B & B) | (~A & ~B), True) is False
+
+
+def test_is_cnf():
+    assert is_cnf(x) is True
+    assert is_cnf(x | y | z) is True
+    assert is_cnf(x & y & z) is True
+    assert is_cnf((x | y) & z) is True
+    assert is_cnf((x & y) | z) is False
+    assert is_cnf(~(x & y) | z) is False
+
+
+def test_is_dnf():
+    assert is_dnf(x) is True
+    assert is_dnf(x | y | z) is True
+    assert is_dnf(x & y & z) is True
+    assert is_dnf((x & y) | z) is True
+    assert is_dnf((x | y) & z) is False
+    assert is_dnf(~(x | y) & z) is False
+
+
+def test_ITE():
+    A, B, C = symbols('A:C')
+    assert ITE(True, False, True) is false
+    assert ITE(True, True, False) is true
+    assert ITE(False, True, False) is false
+    assert ITE(False, False, True) is true
+    assert isinstance(ITE(A, B, C), ITE)
+
+    A = True
+    assert ITE(A, B, C) == B
+    A = False
+    assert ITE(A, B, C) == C
+    B = True
+    assert ITE(And(A, B), B, C) == C
+    assert ITE(Or(A, False), And(B, True), False) is false
+    assert ITE(x, A, B) == Not(x)
+    assert ITE(x, B, A) == x
+    assert ITE(1, x, y) == x
+    assert ITE(0, x, y) == y
+    raises(TypeError, lambda: ITE(2, x, y))
+    raises(TypeError, lambda: ITE(1, [], y))
+    raises(TypeError, lambda: ITE(1, (), y))
+    raises(TypeError, lambda: ITE(1, y, []))
+    assert ITE(1, 1, 1) is S.true
+    assert isinstance(ITE(1, 1, 1, evaluate=False), ITE)
+
+    assert ITE(Eq(x, True), y, x) == ITE(x, y, x)
+    assert ITE(Eq(x, False), y, x) == ITE(~x, y, x)
+    assert ITE(Ne(x, True), y, x) == ITE(~x, y, x)
+    assert ITE(Ne(x, False), y, x) == ITE(x, y, x)
+    assert ITE(Eq(S.true, x), y, x) == ITE(x, y, x)
+    assert ITE(Eq(S.false, x), y, x) == ITE(~x, y, x)
+    assert ITE(Ne(S.true, x), y, x) == ITE(~x, y, x)
+    assert ITE(Ne(S.false, x), y, x) == ITE(x, y, x)
+    # 0 and 1 in the context are not treated as True/False
+    # so the equality must always be False since dissimilar
+    # objects cannot be equal
+    assert ITE(Eq(x, 0), y, x) == x
+    assert ITE(Eq(x, 1), y, x) == x
+    assert ITE(Ne(x, 0), y, x) == y
+    assert ITE(Ne(x, 1), y, x) == y
+    assert ITE(Eq(x, 0), y, z).subs(x, 0) == y
+    assert ITE(Eq(x, 0), y, z).subs(x, 1) == z
+    raises(ValueError, lambda: ITE(x > 1, y, x, z))
+
+
+def test_is_literal():
+    assert is_literal(True) is True
+    assert is_literal(False) is True
+    assert is_literal(A) is True
+    assert is_literal(~A) is True
+    assert is_literal(Or(A, B)) is False
+    assert is_literal(Q.zero(A)) is True
+    assert is_literal(Not(Q.zero(A))) is True
+    assert is_literal(Or(A, B)) is False
+    assert is_literal(And(Q.zero(A), Q.zero(B))) is False
+    assert is_literal(x < 3)
+    assert not is_literal(x + y < 3)
+
+
+def test_operators():
+    # Mostly test __and__, __rand__, and so on
+    assert True & A == A & True == A
+    assert False & A == A & False == False
+    assert A & B == And(A, B)
+    assert True | A == A | True == True
+    assert False | A == A | False == A
+    assert A | B == Or(A, B)
+    assert ~A == Not(A)
+    assert True >> A == A << True == A
+    assert False >> A == A << False == True
+    assert A >> True == True << A == True
+    assert A >> False == False << A == ~A
+    assert A >> B == B << A == Implies(A, B)
+    assert True ^ A == A ^ True == ~A
+    assert False ^ A == A ^ False == A
+    assert A ^ B == Xor(A, B)
+
+
+def test_true_false():
+    assert true is S.true
+    assert false is S.false
+    assert true is not True
+    assert false is not False
+    assert true
+    assert not false
+    assert true == True
+    assert false == False
+    assert not (true == False)
+    assert not (false == True)
+    assert not (true == false)
+
+    assert hash(true) == hash(True)
+    assert hash(false) == hash(False)
+    assert len({true, True}) == len({false, False}) == 1
+
+    assert isinstance(true, BooleanAtom)
+    assert isinstance(false, BooleanAtom)
+    # We don't want to subclass from bool, because bool subclasses from
+    # int. But operators like &, |, ^, <<, >>, and ~ act differently on 0 and
+    # 1 then we want them to on true and false.  See the docstrings of the
+    # various And, Or, etc. functions for examples.
+    assert not isinstance(true, bool)
+    assert not isinstance(false, bool)
+
+    # Note: using 'is' comparison is important here. We want these to return
+    # true and false, not True and False
+
+    assert Not(true) is false
+    assert Not(True) is false
+    assert Not(false) is true
+    assert Not(False) is true
+    assert ~true is false
+    assert ~false is true
+
+    for T, F in product((True, true), (False, false)):
+        assert And(T, F) is false
+        assert And(F, T) is false
+        assert And(F, F) is false
+        assert And(T, T) is true
+        assert And(T, x) == x
+        assert And(F, x) is false
+        if not (T is True and F is False):
+            assert T & F is false
+            assert F & T is false
+        if F is not False:
+            assert F & F is false
+        if T is not True:
+            assert T & T is true
+
+        assert Or(T, F) is true
+        assert Or(F, T) is true
+        assert Or(F, F) is false
+        assert Or(T, T) is true
+        assert Or(T, x) is true
+        assert Or(F, x) == x
+        if not (T is True and F is False):
+            assert T | F is true
+            assert F | T is true
+        if F is not False:
+            assert F | F is false
+        if T is not True:
+            assert T | T is true
+
+        assert Xor(T, F) is true
+        assert Xor(F, T) is true
+        assert Xor(F, F) is false
+        assert Xor(T, T) is false
+        assert Xor(T, x) == ~x
+        assert Xor(F, x) == x
+        if not (T is True and F is False):
+            assert T ^ F is true
+            assert F ^ T is true
+        if F is not False:
+            assert F ^ F is false
+        if T is not True:
+            assert T ^ T is false
+
+        assert Nand(T, F) is true
+        assert Nand(F, T) is true
+        assert Nand(F, F) is true
+        assert Nand(T, T) is false
+        assert Nand(T, x) == ~x
+        assert Nand(F, x) is true
+
+        assert Nor(T, F) is false
+        assert Nor(F, T) is false
+        assert Nor(F, F) is true
+        assert Nor(T, T) is false
+        assert Nor(T, x) is false
+        assert Nor(F, x) == ~x
+
+        assert Implies(T, F) is false
+        assert Implies(F, T) is true
+        assert Implies(F, F) is true
+        assert Implies(T, T) is true
+        assert Implies(T, x) == x
+        assert Implies(F, x) is true
+        assert Implies(x, T) is true
+        assert Implies(x, F) == ~x
+        if not (T is True and F is False):
+            assert T >> F is false
+            assert F << T is false
+            assert F >> T is true
+            assert T << F is true
+        if F is not False:
+            assert F >> F is true
+            assert F << F is true
+        if T is not True:
+            assert T >> T is true
+            assert T << T is true
+
+        assert Equivalent(T, F) is false
+        assert Equivalent(F, T) is false
+        assert Equivalent(F, F) is true
+        assert Equivalent(T, T) is true
+        assert Equivalent(T, x) == x
+        assert Equivalent(F, x) == ~x
+        assert Equivalent(x, T) == x
+        assert Equivalent(x, F) == ~x
+
+        assert ITE(T, T, T) is true
+        assert ITE(T, T, F) is true
+        assert ITE(T, F, T) is false
+        assert ITE(T, F, F) is false
+        assert ITE(F, T, T) is true
+        assert ITE(F, T, F) is false
+        assert ITE(F, F, T) is true
+        assert ITE(F, F, F) is false
+
+    assert all(i.simplify(1, 2) is i for i in (S.true, S.false))
+
+
+def test_bool_as_set():
+    assert ITE(y <= 0, False, y >= 1).as_set() == Interval(1, oo)
+    assert And(x <= 2, x >= -2).as_set() == Interval(-2, 2)
+    assert Or(x >= 2, x <= -2).as_set() == Interval(-oo, -2) + Interval(2, oo)
+    assert Not(x > 2).as_set() == Interval(-oo, 2)
+    # issue 10240
+    assert Not(And(x > 2, x < 3)).as_set() == \
+           Union(Interval(-oo, 2), Interval(3, oo))
+    assert true.as_set() == S.UniversalSet
+    assert false.as_set() is S.EmptySet
+    assert x.as_set() == S.UniversalSet
+    assert And(Or(x < 1, x > 3), x < 2).as_set() == Interval.open(-oo, 1)
+    assert And(x < 1, sin(x) < 3).as_set() == (x < 1).as_set()
+    raises(NotImplementedError, lambda: (sin(x) < 1).as_set())
+    # watch for object morph in as_set
+    assert Eq(-1, cos(2 * x) ** 2 / sin(2 * x) ** 2).as_set() is S.EmptySet
+
+
+@XFAIL
+def test_multivariate_bool_as_set():
+    x, y = symbols('x,y')
+
+    assert And(x >= 0, y >= 0).as_set() == Interval(0, oo) * Interval(0, oo)
+    assert Or(x >= 0, y >= 0).as_set() == S.Reals * S.Reals - \
+           Interval(-oo, 0, True, True) * Interval(-oo, 0, True, True)
+
+
+def test_all_or_nothing():
+    x = symbols('x', extended_real=True)
+    args = x >= -oo, x <= oo
+    v = And(*args)
+    if v.func is And:
+        assert len(v.args) == len(args) - args.count(S.true)
+    else:
+        assert v == True
+    v = Or(*args)
+    if v.func is Or:
+        assert len(v.args) == 2
+    else:
+        assert v == True
+
+
+def test_canonical_atoms():
+    assert true.canonical == true
+    assert false.canonical == false
+
+
+def test_negated_atoms():
+    assert true.negated == false
+    assert false.negated == true
+
+
+def test_issue_8777():
+    assert And(x > 2, x < oo).as_set() == Interval(2, oo, left_open=True)
+    assert And(x >= 1, x < oo).as_set() == Interval(1, oo)
+    assert (x < oo).as_set() == Interval(-oo, oo)
+    assert (x > -oo).as_set() == Interval(-oo, oo)
+
+
+def test_issue_8975():
+    assert Or(And(-oo < x, x <= -2), And(2 <= x, x < oo)).as_set() == \
+           Interval(-oo, -2) + Interval(2, oo)
+
+
+def test_term_to_integer():
+    assert term_to_integer([1, 0, 1, 0, 0, 1, 0]) == 82
+    assert term_to_integer('0010101000111001') == 10809
+
+
+def test_issue_21971():
+    a, b, c, d = symbols('a b c d')
+    f = a & b & c | a & c
+    assert f.subs(a & c, d) == b & d | d
+    assert f.subs(a & b & c, d) == a & c | d
+
+    f = (a | b | c) & (a | c)
+    assert f.subs(a | c, d) == (b | d) & d
+    assert f.subs(a | b | c, d) == (a | c) & d
+
+    f = (a ^ b ^ c) & (a ^ c)
+    assert f.subs(a ^ c, d) == (b ^ d) & d
+    assert f.subs(a ^ b ^ c, d) == (a ^ c) & d
+
+
+def test_truth_table():
+    assert list(truth_table(And(x, y), [x, y], input=False)) == \
+           [False, False, False, True]
+    assert list(truth_table(x | y, [x, y], input=False)) == \
+           [False, True, True, True]
+    assert list(truth_table(x >> y, [x, y], input=False)) == \
+           [True, True, False, True]
+    assert list(truth_table(And(x, y), [x, y])) == \
+           [([0, 0], False), ([0, 1], False), ([1, 0], False), ([1, 1], True)]
+
+
+def test_issue_8571():
+    for t in (S.true, S.false):
+        raises(TypeError, lambda: +t)
+        raises(TypeError, lambda: -t)
+        raises(TypeError, lambda: abs(t))
+        # use int(bool(t)) to get 0 or 1
+        raises(TypeError, lambda: int(t))
+
+        for o in [S.Zero, S.One, x]:
+            for _ in range(2):
+                raises(TypeError, lambda: o + t)
+                raises(TypeError, lambda: o - t)
+                raises(TypeError, lambda: o % t)
+                raises(TypeError, lambda: o * t)
+                raises(TypeError, lambda: o / t)
+                raises(TypeError, lambda: o ** t)
+                o, t = t, o  # do again in reversed order
+
+
+def test_expand_relational():
+    n = symbols('n', negative=True)
+    p, q = symbols('p q', positive=True)
+    r = ((n + q * (-n / q + 1)) / (q * (-n / q + 1)) < 0)
+    assert r is not S.false
+    assert r.expand() is S.false
+    assert (q > 0).expand() is S.true
+
+
+def test_issue_12717():
+    assert S.true.is_Atom == True
+    assert S.false.is_Atom == True
+
+
+def test_as_Boolean():
+    nz = symbols('nz', nonzero=True)
+    assert all(as_Boolean(i) is S.true for i in (True, S.true, 1, nz))
+    z = symbols('z', zero=True)
+    assert all(as_Boolean(i) is S.false for i in (False, S.false, 0, z))
+    assert all(as_Boolean(i) == i for i in (x, x < 0))
+    for i in (2, S(2), x + 1, []):
+        raises(TypeError, lambda: as_Boolean(i))
+
+
+def test_binary_symbols():
+    assert ITE(x < 1, y, z).binary_symbols == {y, z}
+    for f in (Eq, Ne):
+        assert f(x, 1).binary_symbols == set()
+        assert f(x, True).binary_symbols == {x}
+        assert f(x, False).binary_symbols == {x}
+    assert S.true.binary_symbols == set()
+    assert S.false.binary_symbols == set()
+    assert x.binary_symbols == {x}
+    assert And(x, Eq(y, False), Eq(z, 1)).binary_symbols == {x, y}
+    assert Q.prime(x).binary_symbols == set()
+    assert Q.lt(x, 1).binary_symbols == set()
+    assert Q.is_true(x).binary_symbols == {x}
+    assert Q.eq(x, True).binary_symbols == {x}
+    assert Q.prime(x).binary_symbols == set()
+
+
+def test_BooleanFunction_diff():
+    assert And(x, y).diff(x) == Piecewise((0, Eq(y, False)), (1, True))
+
+
+def test_issue_14700():
+    A, B, C, D, E, F, G, H = symbols('A B C D E F G H')
+    q = ((B & D & H & ~F) | (B & H & ~C & ~D) | (B & H & ~C & ~F) |
+         (B & H & ~D & ~G) | (B & H & ~F & ~G) | (C & G & ~B & ~D) |
+         (C & G & ~D & ~H) | (C & G & ~F & ~H) | (D & F & H & ~B) |
+         (D & F & ~G & ~H) | (B & D & F & ~C & ~H) | (D & E & F & ~B & ~C) |
+         (D & F & ~A & ~B & ~C) | (D & F & ~A & ~C & ~H) |
+         (A & B & D & F & ~E & ~H))
+    soldnf = ((B & D & H & ~F) | (D & F & H & ~B) | (B & H & ~C & ~D) |
+              (B & H & ~D & ~G) | (C & G & ~B & ~D) | (C & G & ~D & ~H) |
+              (C & G & ~F & ~H) | (D & F & ~G & ~H) | (D & E & F & ~C & ~H) |
+              (D & F & ~A & ~C & ~H) | (A & B & D & F & ~E & ~H))
+    solcnf = ((B | C | D) & (B | D | G) & (C | D | H) & (C | F | H) &
+              (D | G | H) & (F | G | H) & (B | F | ~D | ~H) &
+              (~B | ~D | ~F | ~H) & (D | ~B | ~C | ~G | ~H) &
+              (A | H | ~C | ~D | ~F | ~G) & (H | ~C | ~D | ~E | ~F | ~G) &
+              (B | E | H | ~A | ~D | ~F | ~G))
+    assert simplify_logic(q, "dnf") == soldnf
+    assert simplify_logic(q, "cnf") == solcnf
+
+    minterms = [[0, 1, 0, 0], [0, 1, 0, 1], [0, 1, 1, 0], [0, 1, 1, 1],
+                [0, 0, 1, 1], [1, 0, 1, 1]]
+    dontcares = [[1, 0, 0, 0], [1, 0, 0, 1], [1, 1, 0, 0], [1, 1, 0, 1]]
+    assert SOPform([w, x, y, z], minterms) == (x & ~w) | (y & z & ~x)
+    # Should not be more complicated with don't cares
+    assert SOPform([w, x, y, z], minterms, dontcares) == \
+           (x & ~w) | (y & z & ~x)
+
+
+def test_issue_25115():
+    cond = Contains(x, S.Integers)
+    # Previously this raised an exception:
+    assert simplify_logic(cond) == cond
+
+
+def test_relational_simplification():
+    w, x, y, z = symbols('w x y z', real=True)
+    d, e = symbols('d e', real=False)
+    # Test all combinations or sign and order
+    assert Or(x >= y, x < y).simplify() == S.true
+    assert Or(x >= y, y > x).simplify() == S.true
+    assert Or(x >= y, -x > -y).simplify() == S.true
+    assert Or(x >= y, -y < -x).simplify() == S.true
+    assert Or(-x <= -y, x < y).simplify() == S.true
+    assert Or(-x <= -y, -x > -y).simplify() == S.true
+    assert Or(-x <= -y, y > x).simplify() == S.true
+    assert Or(-x <= -y, -y < -x).simplify() == S.true
+    assert Or(y <= x, x < y).simplify() == S.true
+    assert Or(y <= x, y > x).simplify() == S.true
+    assert Or(y <= x, -x > -y).simplify() == S.true
+    assert Or(y <= x, -y < -x).simplify() == S.true
+    assert Or(-y >= -x, x < y).simplify() == S.true
+    assert Or(-y >= -x, y > x).simplify() == S.true
+    assert Or(-y >= -x, -x > -y).simplify() == S.true
+    assert Or(-y >= -x, -y < -x).simplify() == S.true
+
+    assert Or(x < y, x >= y).simplify() == S.true
+    assert Or(y > x, x >= y).simplify() == S.true
+    assert Or(-x > -y, x >= y).simplify() == S.true
+    assert Or(-y < -x, x >= y).simplify() == S.true
+    assert Or(x < y, -x <= -y).simplify() == S.true
+    assert Or(-x > -y, -x <= -y).simplify() == S.true
+    assert Or(y > x, -x <= -y).simplify() == S.true
+    assert Or(-y < -x, -x <= -y).simplify() == S.true
+    assert Or(x < y, y <= x).simplify() == S.true
+    assert Or(y > x, y <= x).simplify() == S.true
+    assert Or(-x > -y, y <= x).simplify() == S.true
+    assert Or(-y < -x, y <= x).simplify() == S.true
+    assert Or(x < y, -y >= -x).simplify() == S.true
+    assert Or(y > x, -y >= -x).simplify() == S.true
+    assert Or(-x > -y, -y >= -x).simplify() == S.true
+    assert Or(-y < -x, -y >= -x).simplify() == S.true
+
+    # Some other tests
+    assert Or(x >= y, w < z, x <= y).simplify() == S.true
+    assert And(x >= y, x < y).simplify() == S.false
+    assert Or(x >= y, Eq(y, x)).simplify() == (x >= y)
+    assert And(x >= y, Eq(y, x)).simplify() == Eq(x, y)
+    assert And(Eq(x, y), x >= 1, 2 < y, y >= 5, z < y).simplify() == \
+           (Eq(x, y) & (x >= 1) & (y >= 5) & (y > z))
+    assert Or(Eq(x, y), x >= y, w < y, z < y).simplify() == \
+           (x >= y) | (y > z) | (w < y)
+    assert And(Eq(x, y), x >= y, w < y, y >= z, z < y).simplify() == \
+           Eq(x, y) & (y > z) & (w < y)
+    # assert And(Eq(x, y), x >= y, w < y, y >= z, z < y).simplify(relational_minmax=True) == \
+    #    And(Eq(x, y), y > Max(w, z))
+    # assert Or(Eq(x, y), x >= 1, 2 < y, y >= 5, z < y).simplify(relational_minmax=True) == \
+    #    (Eq(x, y) | (x >= 1) | (y > Min(2, z)))
+    assert And(Eq(x, y), x >= 1, 2 < y, y >= 5, z < y).simplify() == \
+           (Eq(x, y) & (x >= 1) & (y >= 5) & (y > z))
+    assert (Eq(x, y) & Eq(d, e) & (x >= y) & (d >= e)).simplify() == \
+           (Eq(x, y) & Eq(d, e) & (d >= e))
+    assert And(Eq(x, y), Eq(x, -y)).simplify() == And(Eq(x, 0), Eq(y, 0))
+    assert Xor(x >= y, x <= y).simplify() == Ne(x, y)
+    assert And(x > 1, x < -1, Eq(x, y)).simplify() == S.false
+    # From #16690
+    assert And(x >= y, Eq(y, 0)).simplify() == And(x >= 0, Eq(y, 0))
+    assert Or(Ne(x, 1), Ne(x, 2)).simplify() == S.true
+    assert And(Eq(x, 1), Ne(2, x)).simplify() == Eq(x, 1)
+    assert Or(Eq(x, 1), Ne(2, x)).simplify() == Ne(x, 2)
+
+
+def test_issue_8373():
+    x = symbols('x', real=True)
+    assert Or(x < 1, x > -1).simplify() == S.true
+    assert Or(x < 1, x >= 1).simplify() == S.true
+    assert And(x < 1, x >= 1).simplify() == S.false
+    assert Or(x <= 1, x >= 1).simplify() == S.true
+
+
+def test_issue_7950():
+    x = symbols('x', real=True)
+    assert And(Eq(x, 1), Eq(x, 2)).simplify() == S.false
+
+
+@slow
+def test_relational_simplification_numerically():
+    def test_simplification_numerically_function(original, simplified):
+        symb = original.free_symbols
+        n = len(symb)
+        valuelist = list(set(combinations(list(range(-(n - 1), n)) * n, n)))
+        for values in valuelist:
+            sublist = dict(zip(symb, values))
+            originalvalue = original.subs(sublist)
+            simplifiedvalue = simplified.subs(sublist)
+            assert originalvalue == simplifiedvalue, "Original: {}\nand" \
+                                                     " simplified: {}\ndo not evaluate to the same value for {}" \
+                                                     "".format(original, simplified, sublist)
+
+    w, x, y, z = symbols('w x y z', real=True)
+    d, e = symbols('d e', real=False)
+
+    expressions = (And(Eq(x, y), x >= y, w < y, y >= z, z < y),
+                   And(Eq(x, y), x >= 1, 2 < y, y >= 5, z < y),
+                   Or(Eq(x, y), x >= 1, 2 < y, y >= 5, z < y),
+                   And(x >= y, Eq(y, x)),
+                   Or(And(Eq(x, y), x >= y, w < y, Or(y >= z, z < y)),
+                      And(Eq(x, y), x >= 1, 2 < y, y >= -1, z < y)),
+                   (Eq(x, y) & Eq(d, e) & (x >= y) & (d >= e)),
+                   )
+
+    for expression in expressions:
+        test_simplification_numerically_function(expression,
+                                                 expression.simplify())
+
+
+def test_relational_simplification_patterns_numerically():
+    from sympy.core import Wild
+    from sympy.logic.boolalg import _simplify_patterns_and, \
+        _simplify_patterns_or, _simplify_patterns_xor
+    a = Wild('a')
+    b = Wild('b')
+    c = Wild('c')
+    symb = [a, b, c]
+    patternlists = [[And, _simplify_patterns_and()],
+                    [Or, _simplify_patterns_or()],
+                    [Xor, _simplify_patterns_xor()]]
+    valuelist = list(set(combinations(list(range(-2, 3)) * 3, 3)))
+    # Skip combinations of +/-2 and 0, except for all 0
+    valuelist = [v for v in valuelist if any(w % 2 for w in v) or not any(v)]
+    for func, patternlist in patternlists:
+        for pattern in patternlist:
+            original = func(*pattern[0].args)
+            simplified = pattern[1]
+            for values in valuelist:
+                sublist = dict(zip(symb, values))
+                originalvalue = original.xreplace(sublist)
+                simplifiedvalue = simplified.xreplace(sublist)
+                assert originalvalue == simplifiedvalue, "Original: {}\nand" \
+                                                         " simplified: {}\ndo not evaluate to the same value for" \
+                                                         "{}".format(pattern[0], simplified, sublist)
+
+
+def test_issue_16803():
+    n = symbols('n')
+    # No simplification done, but should not raise an exception
+    assert ((n > 3) | (n < 0) | ((n > 0) & (n < 3))).simplify() == \
+           (n > 3) | (n < 0) | ((n > 0) & (n < 3))
+
+
+def test_issue_17530():
+    r = {x: oo, y: oo}
+    assert Or(x + y > 0, x - y < 0).subs(r)
+    assert not And(x + y < 0, x - y < 0).subs(r)
+    raises(TypeError, lambda: Or(x + y < 0, x - y < 0).subs(r))
+    raises(TypeError, lambda: And(x + y > 0, x - y < 0).subs(r))
+    raises(TypeError, lambda: And(x + y > 0, x - y < 0).subs(r))
+
+
+def test_anf_coeffs():
+    assert anf_coeffs([1, 0]) == [1, 1]
+    assert anf_coeffs([0, 0, 0, 1]) == [0, 0, 0, 1]
+    assert anf_coeffs([0, 1, 1, 1]) == [0, 1, 1, 1]
+    assert anf_coeffs([1, 1, 1, 0]) == [1, 0, 0, 1]
+    assert anf_coeffs([1, 0, 0, 0]) == [1, 1, 1, 1]
+    assert anf_coeffs([1, 0, 0, 1]) == [1, 1, 1, 0]
+    assert anf_coeffs([1, 1, 0, 1]) == [1, 0, 1, 1]
+
+
+def test_ANFform():
+    x, y = symbols('x,y')
+    assert ANFform([x], [1, 1]) == True
+    assert ANFform([x], [0, 0]) == False
+    assert ANFform([x], [1, 0]) == Xor(x, True, remove_true=False)
+    assert ANFform([x, y], [1, 1, 1, 0]) == \
+           Xor(True, And(x, y), remove_true=False)
+
+
+def test_bool_minterm():
+    x, y = symbols('x,y')
+    assert bool_minterm(3, [x, y]) == And(x, y)
+    assert bool_minterm([1, 0], [x, y]) == And(Not(y), x)
+
+
+def test_bool_maxterm():
+    x, y = symbols('x,y')
+    assert bool_maxterm(2, [x, y]) == Or(Not(x), y)
+    assert bool_maxterm([0, 1], [x, y]) == Or(Not(y), x)
+
+
+def test_bool_monomial():
+    x, y = symbols('x,y')
+    assert bool_monomial(1, [x, y]) == y
+    assert bool_monomial([1, 1], [x, y]) == And(x, y)
+
+
+def test_check_pair():
+    assert _check_pair([0, 1, 0], [0, 1, 1]) == 2
+    assert _check_pair([0, 1, 0], [1, 1, 1]) == -1
+
+
+def test_issue_19114():
+    expr = (B & C) | (A & ~C) | (~A & ~B)
+    # Expression is minimal, but there are multiple minimal forms possible
+    res1 = (A & B) | (C & ~A) | (~B & ~C)
+    result = to_dnf(expr, simplify=True)
+    assert result in (expr, res1)
+
+
+def test_issue_20870():
+    result = SOPform([a, b, c, d], [1, 2, 3, 4, 5, 6, 8, 9, 11, 12, 14, 15])
+    expected = ((d & ~b) | (a & b & c) | (a & ~c & ~d) |
+                (b & ~a & ~c) | (c & ~a & ~d))
+    assert result == expected
+
+
+def test_convert_to_varsSOP():
+    assert _convert_to_varsSOP([0, 1, 0], [x, y, z]) == And(Not(x), y, Not(z))
+    assert _convert_to_varsSOP([3, 1, 0], [x, y, z]) == And(y, Not(z))
+
+
+def test_convert_to_varsPOS():
+    assert _convert_to_varsPOS([0, 1, 0], [x, y, z]) == Or(x, Not(y), z)
+    assert _convert_to_varsPOS([3, 1, 0], [x, y, z]) == Or(Not(y), z)
+
+
+def test_gateinputcount():
+    a, b, c, d, e = symbols('a:e')
+    assert gateinputcount(And(a, b)) == 2
+    assert gateinputcount(a | b & c & d ^ (e | a)) == 9
+    assert gateinputcount(And(a, True)) == 0
+    raises(TypeError, lambda: gateinputcount(a * b))
+
+
+def test_refine():
+    # relational
+    assert not refine(x < 0, ~(x < 0))
+    assert refine(x < 0, (x < 0))
+    assert refine(x < 0, (0 > x)) is S.true
+    assert refine(x < 0, (y < 0)) == (x < 0)
+    assert not refine(x <= 0, ~(x <= 0))
+    assert refine(x <= 0, (x <= 0))
+    assert refine(x <= 0, (0 >= x)) is S.true
+    assert refine(x <= 0, (y <= 0)) == (x <= 0)
+    assert not refine(x > 0, ~(x > 0))
+    assert refine(x > 0, (x > 0))
+    assert refine(x > 0, (0 < x)) is S.true
+    assert refine(x > 0, (y > 0)) == (x > 0)
+    assert not refine(x >= 0, ~(x >= 0))
+    assert refine(x >= 0, (x >= 0))
+    assert refine(x >= 0, (0 <= x)) is S.true
+    assert refine(x >= 0, (y >= 0)) == (x >= 0)
+    assert not refine(Eq(x, 0), ~(Eq(x, 0)))
+    assert refine(Eq(x, 0), (Eq(x, 0)))
+    assert refine(Eq(x, 0), (Eq(0, x))) is S.true
+    assert refine(Eq(x, 0), (Eq(y, 0))) == Eq(x, 0)
+    assert not refine(Ne(x, 0), ~(Ne(x, 0)))
+    assert refine(Ne(x, 0), (Ne(0, x))) is S.true
+    assert refine(Ne(x, 0), (Ne(x, 0)))
+    assert refine(Ne(x, 0), (Ne(y, 0))) == (Ne(x, 0))
+
+    # boolean functions
+    assert refine(And(x > 0, y > 0), (x > 0)) == (y > 0)
+    assert refine(And(x > 0, y > 0), (x > 0) & (y > 0)) is S.true
+
+    # predicates
+    assert refine(Q.positive(x), Q.positive(x)) is S.true
+    assert refine(Q.positive(x), Q.negative(x)) is S.false
+    assert refine(Q.positive(x), Q.real(x)) == Q.positive(x)
+
+
+def test_relational_threeterm_simplification_patterns_numerically():
+    from sympy.core import Wild
+    from sympy.logic.boolalg import _simplify_patterns_and3
+    a = Wild('a')
+    b = Wild('b')
+    c = Wild('c')
+    symb = [a, b, c]
+    patternlists = [[And, _simplify_patterns_and3()]]
+    valuelist = list(set(combinations(list(range(-2, 3)) * 3, 3)))
+    # Skip combinations of +/-2 and 0, except for all 0
+    valuelist = [v for v in valuelist if any(w % 2 for w in v) or not any(v)]
+    for func, patternlist in patternlists:
+        for pattern in patternlist:
+            original = func(*pattern[0].args)
+            simplified = pattern[1]
+            for values in valuelist:
+                sublist = dict(zip(symb, values))
+                originalvalue = original.xreplace(sublist)
+                simplifiedvalue = simplified.xreplace(sublist)
+                assert originalvalue == simplifiedvalue, "Original: {}\nand" \
+                                                         " simplified: {}\ndo not evaluate to the same value for" \
+                                                         "{}".format(pattern[0], simplified, sublist)
+
+
+def test_issue_25451():
+    x = Or(And(a, c), Eq(a, b))
+    assert isinstance(x, Or)
+    assert set(x.args) == {And(a, c), Eq(a, b)}
+
+
+def test_issue_26985():
+    a, b, c, d = symbols('a b c d')
+
+    # Expression before applying to_anf
+    x = Xor(c, And(a, b), And(a, c))
+    y = Xor(a, b, And(a, c))
+
+    # Applying to_anf
+    result = Xor(Xor(d, And(x, y)), And(x, y))
+    result_anf = to_anf(Xor(to_anf(Xor(d, And(x, y))), And(x, y)))
+
+    assert result_anf == d
+    assert result == d

phivenv/Lib/site-packages/sympy/logic/tests/test_dimacs.py

@@ -0,0 +1,234 @@
+"""Various tests on satisfiability using dimacs cnf file syntax
+You can find lots of cnf files in
+ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/benchmarks/cnf/
+"""
+
+from sympy.logic.utilities.dimacs import load
+from sympy.logic.algorithms.dpll import dpll_satisfiable
+
+
+def test_f1():
+    assert bool(dpll_satisfiable(load(f1)))
+
+
+def test_f2():
+    assert bool(dpll_satisfiable(load(f2)))
+
+
+def test_f3():
+    assert bool(dpll_satisfiable(load(f3)))
+
+
+def test_f4():
+    assert not bool(dpll_satisfiable(load(f4)))
+
+
+def test_f5():
+    assert bool(dpll_satisfiable(load(f5)))
+
+f1 = """c  simple example
+c Resolution: SATISFIABLE
+c
+p cnf 3 2
+1 -3 0
+2 3 -1 0
+"""
+
+
+f2 = """c  an example from Quinn's text, 16 variables and 18 clauses.
+c Resolution: SATISFIABLE
+c
+p cnf 16 18
+  1    2  0
+ -2   -4  0
+  3    4  0
+ -4   -5  0
+  5   -6  0
+  6   -7  0
+  6    7  0
+  7  -16  0
+  8   -9  0
+ -8  -14  0
+  9   10  0
+  9  -10  0
+-10  -11  0
+ 10   12  0
+ 11   12  0
+ 13   14  0
+ 14  -15  0
+ 15   16  0
+"""
+
+f3 = """c
+p cnf 6 9
+-1 0
+-3 0
+2 -1 0
+2 -4 0
+5 -4 0
+-1 -3 0
+-4 -6 0
+1 3 -2 0
+4 6 -2 -5 0
+"""
+
+f4 = """c
+c file:   hole6.cnf [http://people.sc.fsu.edu/~jburkardt/data/cnf/hole6.cnf]
+c
+c SOURCE: John Hooker (jh38+@andrew.cmu.edu)
+c
+c DESCRIPTION: Pigeon hole problem of placing n (for file 'holen.cnf') pigeons
+c              in n+1 holes without placing 2 pigeons in the same hole
+c
+c NOTE: Part of the collection at the Forschungsinstitut fuer
+c       anwendungsorientierte Wissensverarbeitung in Ulm Germany.
+c
+c NOTE: Not satisfiable
+c
+p cnf 42 133
+-1     -7    0
+-1     -13   0
+-1     -19   0
+-1     -25   0
+-1     -31   0
+-1     -37   0
+-7     -13   0
+-7     -19   0
+-7     -25   0
+-7     -31   0
+-7     -37   0
+-13    -19   0
+-13    -25   0
+-13    -31   0
+-13    -37   0
+-19    -25   0
+-19    -31   0
+-19    -37   0
+-25    -31   0
+-25    -37   0
+-31    -37   0
+-2     -8    0
+-2     -14   0
+-2     -20   0
+-2     -26   0
+-2     -32   0
+-2     -38   0
+-8     -14   0
+-8     -20   0
+-8     -26   0
+-8     -32   0
+-8     -38   0
+-14    -20   0
+-14    -26   0
+-14    -32   0
+-14    -38   0
+-20    -26   0
+-20    -32   0
+-20    -38   0
+-26    -32   0
+-26    -38   0
+-32    -38   0
+-3     -9    0
+-3     -15   0
+-3     -21   0
+-3     -27   0
+-3     -33   0
+-3     -39   0
+-9     -15   0
+-9     -21   0
+-9     -27   0
+-9     -33   0
+-9     -39   0
+-15    -21   0
+-15    -27   0
+-15    -33   0
+-15    -39   0
+-21    -27   0
+-21    -33   0
+-21    -39   0
+-27    -33   0
+-27    -39   0
+-33    -39   0
+-4     -10   0
+-4     -16   0
+-4     -22   0
+-4     -28   0
+-4     -34   0
+-4     -40   0
+-10    -16   0
+-10    -22   0
+-10    -28   0
+-10    -34   0
+-10    -40   0
+-16    -22   0
+-16    -28   0
+-16    -34   0
+-16    -40   0
+-22    -28   0
+-22    -34   0
+-22    -40   0
+-28    -34   0
+-28    -40   0
+-34    -40   0
+-5     -11   0
+-5     -17   0
+-5     -23   0
+-5     -29   0
+-5     -35   0
+-5     -41   0
+-11    -17   0
+-11    -23   0
+-11    -29   0
+-11    -35   0
+-11    -41   0
+-17    -23   0
+-17    -29   0
+-17    -35   0
+-17    -41   0
+-23    -29   0
+-23    -35   0
+-23    -41   0
+-29    -35   0
+-29    -41   0
+-35    -41   0
+-6     -12   0
+-6     -18   0
+-6     -24   0
+-6     -30   0
+-6     -36   0
+-6     -42   0
+-12    -18   0
+-12    -24   0
+-12    -30   0
+-12    -36   0
+-12    -42   0
+-18    -24   0
+-18    -30   0
+-18    -36   0
+-18    -42   0
+-24    -30   0
+-24    -36   0
+-24    -42   0
+-30    -36   0
+-30    -42   0
+-36    -42   0
+ 6      5      4      3      2      1    0
+ 12     11     10     9      8      7    0
+ 18     17     16     15     14     13   0
+ 24     23     22     21     20     19   0
+ 30     29     28     27     26     25   0
+ 36     35     34     33     32     31   0
+ 42     41     40     39     38     37   0
+"""
+
+f5 = """c  simple example requiring variable selection
+c
+c NOTE: Satisfiable
+c
+p cnf 5 5
+1 2 3 0
+1 -2 3 0
+4 5 -3 0
+1 -4 -3 0
+-1 -5 0
+"""

phivenv/Lib/site-packages/sympy/logic/tests/test_inference.py

@@ -0,0 +1,396 @@
+"""For more tests on satisfiability, see test_dimacs"""
+
+from sympy.assumptions.ask import Q
+from sympy.core.symbol import symbols
+from sympy.core.relational import Unequality
+from sympy.logic.boolalg import And, Or, Implies, Equivalent, true, false
+from sympy.logic.inference import literal_symbol, \
+     pl_true, satisfiable, valid, entails, PropKB
+from sympy.logic.algorithms.dpll import dpll, dpll_satisfiable, \
+    find_pure_symbol, find_unit_clause, unit_propagate, \
+    find_pure_symbol_int_repr, find_unit_clause_int_repr, \
+    unit_propagate_int_repr
+from sympy.logic.algorithms.dpll2 import dpll_satisfiable as dpll2_satisfiable
+
+from sympy.logic.algorithms.z3_wrapper import z3_satisfiable
+from sympy.assumptions.cnf import CNF, EncodedCNF
+from sympy.logic.tests.test_lra_theory import make_random_problem
+from sympy.core.random import randint
+
+from sympy.testing.pytest import raises, skip
+from sympy.external import import_module
+
+
+def test_literal():
+    A, B = symbols('A,B')
+    assert literal_symbol(True) is True
+    assert literal_symbol(False) is False
+    assert literal_symbol(A) is A
+    assert literal_symbol(~A) is A
+
+
+def test_find_pure_symbol():
+    A, B, C = symbols('A,B,C')
+    assert find_pure_symbol([A], [A]) == (A, True)
+    assert find_pure_symbol([A, B], [~A | B, ~B | A]) == (None, None)
+    assert find_pure_symbol([A, B, C], [ A | ~B, ~B | ~C, C | A]) == (A, True)
+    assert find_pure_symbol([A, B, C], [~A | B, B | ~C, C | A]) == (B, True)
+    assert find_pure_symbol([A, B, C], [~A | ~B, ~B | ~C, C | A]) == (B, False)
+    assert find_pure_symbol(
+        [A, B, C], [~A | B, ~B | ~C, C | A]) == (None, None)
+
+
+def test_find_pure_symbol_int_repr():
+    assert find_pure_symbol_int_repr([1], [{1}]) == (1, True)
+    assert find_pure_symbol_int_repr([1, 2],
+                [{-1, 2}, {-2, 1}]) == (None, None)
+    assert find_pure_symbol_int_repr([1, 2, 3],
+                [{1, -2}, {-2, -3}, {3, 1}]) == (1, True)
+    assert find_pure_symbol_int_repr([1, 2, 3],
+                [{-1, 2}, {2, -3}, {3, 1}]) == (2, True)
+    assert find_pure_symbol_int_repr([1, 2, 3],
+                [{-1, -2}, {-2, -3}, {3, 1}]) == (2, False)
+    assert find_pure_symbol_int_repr([1, 2, 3],
+                [{-1, 2}, {-2, -3}, {3, 1}]) == (None, None)
+
+
+def test_unit_clause():
+    A, B, C = symbols('A,B,C')
+    assert find_unit_clause([A], {}) == (A, True)
+    assert find_unit_clause([A, ~A], {}) == (A, True)  # Wrong ??
+    assert find_unit_clause([A | B], {A: True}) == (B, True)
+    assert find_unit_clause([A | B], {B: True}) == (A, True)
+    assert find_unit_clause(
+        [A | B | C, B | ~C, A | ~B], {A: True}) == (B, False)
+    assert find_unit_clause([A | B | C, B | ~C, A | B], {A: True}) == (B, True)
+    assert find_unit_clause([A | B | C, B | ~C, A ], {}) == (A, True)
+
+
+def test_unit_clause_int_repr():
+    assert find_unit_clause_int_repr(map(set, [[1]]), {}) == (1, True)
+    assert find_unit_clause_int_repr(map(set, [[1], [-1]]), {}) == (1, True)
+    assert find_unit_clause_int_repr([{1, 2}], {1: True}) == (2, True)
+    assert find_unit_clause_int_repr([{1, 2}], {2: True}) == (1, True)
+    assert find_unit_clause_int_repr(map(set,
+        [[1, 2, 3], [2, -3], [1, -2]]), {1: True}) == (2, False)
+    assert find_unit_clause_int_repr(map(set,
+        [[1, 2, 3], [3, -3], [1, 2]]), {1: True}) == (2, True)
+
+    A, B, C = symbols('A,B,C')
+    assert find_unit_clause([A | B | C, B | ~C, A ], {}) == (A, True)
+
+
+def test_unit_propagate():
+    A, B, C = symbols('A,B,C')
+    assert unit_propagate([A | B], A) == []
+    assert unit_propagate([A | B, ~A | C, ~C | B, A], A) == [C, ~C | B, A]
+
+
+def test_unit_propagate_int_repr():
+    assert unit_propagate_int_repr([{1, 2}], 1) == []
+    assert unit_propagate_int_repr(map(set,
+        [[1, 2], [-1, 3], [-3, 2], [1]]), 1) == [{3}, {-3, 2}]
+
+
+def test_dpll():
+    """This is also tested in test_dimacs"""
+    A, B, C = symbols('A,B,C')
+    assert dpll([A | B], [A, B], {A: True, B: True}) == {A: True, B: True}
+
+
+def test_dpll_satisfiable():
+    A, B, C = symbols('A,B,C')
+    assert dpll_satisfiable( A & ~A ) is False
+    assert dpll_satisfiable( A & ~B ) == {A: True, B: False}
+    assert dpll_satisfiable(
+        A | B ) in ({A: True}, {B: True}, {A: True, B: True})
+    assert dpll_satisfiable(
+        (~A | B) & (~B | A) ) in ({A: True, B: True}, {A: False, B: False})
+    assert dpll_satisfiable( (A | B) & (~B | C) ) in ({A: True, B: False},
+            {A: True, C: True}, {B: True, C: True})
+    assert dpll_satisfiable( A & B & C  ) == {A: True, B: True, C: True}
+    assert dpll_satisfiable( (A | B) & (A >> B) ) == {B: True}
+    assert dpll_satisfiable( Equivalent(A, B) & A ) == {A: True, B: True}
+    assert dpll_satisfiable( Equivalent(A, B) & ~A ) == {A: False, B: False}
+
+
+def test_dpll2_satisfiable():
+    A, B, C = symbols('A,B,C')
+    assert dpll2_satisfiable( A & ~A ) is False
+    assert dpll2_satisfiable( A & ~B ) == {A: True, B: False}
+    assert dpll2_satisfiable(
+        A | B ) in ({A: True}, {B: True}, {A: True, B: True})
+    assert dpll2_satisfiable(
+        (~A | B) & (~B | A) ) in ({A: True, B: True}, {A: False, B: False})
+    assert dpll2_satisfiable( (A | B) & (~B | C) ) in ({A: True, B: False, C: True},
+        {A: True, B: True, C: True})
+    assert dpll2_satisfiable( A & B & C  ) == {A: True, B: True, C: True}
+    assert dpll2_satisfiable( (A | B) & (A >> B) ) in ({B: True, A: False},
+        {B: True, A: True})
+    assert dpll2_satisfiable( Equivalent(A, B) & A ) == {A: True, B: True}
+    assert dpll2_satisfiable( Equivalent(A, B) & ~A ) == {A: False, B: False}
+
+
+def test_minisat22_satisfiable():
+    A, B, C = symbols('A,B,C')
+    minisat22_satisfiable = lambda expr: satisfiable(expr, algorithm="minisat22")
+    assert minisat22_satisfiable( A & ~A ) is False
+    assert minisat22_satisfiable( A & ~B ) == {A: True, B: False}
+    assert minisat22_satisfiable(
+        A | B ) in ({A: True}, {B: False}, {A: False, B: True}, {A: True, B: True}, {A: True, B: False})
+    assert minisat22_satisfiable(
+        (~A | B) & (~B | A) ) in ({A: True, B: True}, {A: False, B: False})
+    assert minisat22_satisfiable( (A | B) & (~B | C) ) in ({A: True, B: False, C: True},
+        {A: True, B: True, C: True}, {A: False, B: True, C: True}, {A: True, B: False, C: False})
+    assert minisat22_satisfiable( A & B & C  ) == {A: True, B: True, C: True}
+    assert minisat22_satisfiable( (A | B) & (A >> B) ) in ({B: True, A: False},
+        {B: True, A: True})
+    assert minisat22_satisfiable( Equivalent(A, B) & A ) == {A: True, B: True}
+    assert minisat22_satisfiable( Equivalent(A, B) & ~A ) == {A: False, B: False}
+
+def test_minisat22_minimal_satisfiable():
+    A, B, C = symbols('A,B,C')
+    minisat22_satisfiable = lambda expr, minimal=True: satisfiable(expr, algorithm="minisat22", minimal=True)
+    assert minisat22_satisfiable( A & ~A ) is False
+    assert minisat22_satisfiable( A & ~B ) == {A: True, B: False}
+    assert minisat22_satisfiable(
+        A | B ) in ({A: True}, {B: False}, {A: False, B: True}, {A: True, B: True}, {A: True, B: False})
+    assert minisat22_satisfiable(
+        (~A | B) & (~B | A) ) in ({A: True, B: True}, {A: False, B: False})
+    assert minisat22_satisfiable( (A | B) & (~B | C) ) in ({A: True, B: False, C: True},
+        {A: True, B: True, C: True}, {A: False, B: True, C: True}, {A: True, B: False, C: False})
+    assert minisat22_satisfiable( A & B & C  ) == {A: True, B: True, C: True}
+    assert minisat22_satisfiable( (A | B) & (A >> B) ) in ({B: True, A: False},
+        {B: True, A: True})
+    assert minisat22_satisfiable( Equivalent(A, B) & A ) == {A: True, B: True}
+    assert minisat22_satisfiable( Equivalent(A, B) & ~A ) == {A: False, B: False}
+    g = satisfiable((A | B | C),algorithm="minisat22",minimal=True,all_models=True)
+    sol = next(g)
+    first_solution = {key for key, value in sol.items() if value}
+    sol=next(g)
+    second_solution = {key for key, value in sol.items() if value}
+    sol=next(g)
+    third_solution = {key for key, value in sol.items() if value}
+    assert not first_solution <= second_solution
+    assert not second_solution <= third_solution
+    assert not first_solution <= third_solution
+
+def test_satisfiable():
+    A, B, C = symbols('A,B,C')
+    assert satisfiable(A & (A >> B) & ~B) is False
+
+
+def test_valid():
+    A, B, C = symbols('A,B,C')
+    assert valid(A >> (B >> A)) is True
+    assert valid((A >> (B >> C)) >> ((A >> B) >> (A >> C))) is True
+    assert valid((~B >> ~A) >> (A >> B)) is True
+    assert valid(A | B | C) is False
+    assert valid(A >> B) is False
+
+
+def test_pl_true():
+    A, B, C = symbols('A,B,C')
+    assert pl_true(True) is True
+    assert pl_true( A & B, {A: True, B: True}) is True
+    assert pl_true( A | B, {A: True}) is True
+    assert pl_true( A | B, {B: True}) is True
+    assert pl_true( A | B, {A: None, B: True}) is True
+    assert pl_true( A >> B, {A: False}) is True
+    assert pl_true( A | B | ~C, {A: False, B: True, C: True}) is True
+    assert pl_true(Equivalent(A, B), {A: False, B: False}) is True
+
+    # test for false
+    assert pl_true(False) is False
+    assert pl_true( A & B, {A: False, B: False}) is False
+    assert pl_true( A & B, {A: False}) is False
+    assert pl_true( A & B, {B: False}) is False
+    assert pl_true( A | B, {A: False, B: False}) is False
+
+    #test for None
+    assert pl_true(B, {B: None}) is None
+    assert pl_true( A & B, {A: True, B: None}) is None
+    assert pl_true( A >> B, {A: True, B: None}) is None
+    assert pl_true(Equivalent(A, B), {A: None}) is None
+    assert pl_true(Equivalent(A, B), {A: True, B: None}) is None
+
+    # Test for deep
+    assert pl_true(A | B, {A: False}, deep=True) is None
+    assert pl_true(~A & ~B, {A: False}, deep=True) is None
+    assert pl_true(A | B, {A: False, B: False}, deep=True) is False
+    assert pl_true(A & B & (~A | ~B), {A: True}, deep=True) is False
+    assert pl_true((C >> A) >> (B >> A), {C: True}, deep=True) is True
+
+
+def test_pl_true_wrong_input():
+    from sympy.core.numbers import pi
+    raises(ValueError, lambda: pl_true('John Cleese'))
+    raises(ValueError, lambda: pl_true(42 + pi + pi ** 2))
+    raises(ValueError, lambda: pl_true(42))
+
+
+def test_entails():
+    A, B, C = symbols('A, B, C')
+    assert entails(A, [A >> B, ~B]) is False
+    assert entails(B, [Equivalent(A, B), A]) is True
+    assert entails((A >> B) >> (~A >> ~B)) is False
+    assert entails((A >> B) >> (~B >> ~A)) is True
+
+
+def test_PropKB():
+    A, B, C = symbols('A,B,C')
+    kb = PropKB()
+    assert kb.ask(A >> B) is False
+    assert kb.ask(A >> (B >> A)) is True
+    kb.tell(A >> B)
+    kb.tell(B >> C)
+    assert kb.ask(A) is False
+    assert kb.ask(B) is False
+    assert kb.ask(C) is False
+    assert kb.ask(~A) is False
+    assert kb.ask(~B) is False
+    assert kb.ask(~C) is False
+    assert kb.ask(A >> C) is True
+    kb.tell(A)
+    assert kb.ask(A) is True
+    assert kb.ask(B) is True
+    assert kb.ask(C) is True
+    assert kb.ask(~C) is False
+    kb.retract(A)
+    assert kb.ask(C) is False
+
+
+def test_propKB_tolerant():
+    """"tolerant to bad input"""
+    kb = PropKB()
+    A, B, C = symbols('A,B,C')
+    assert kb.ask(B) is False
+
+def test_satisfiable_non_symbols():
+    x, y = symbols('x y')
+    assumptions = Q.zero(x*y)
+    facts = Implies(Q.zero(x*y), Q.zero(x) | Q.zero(y))
+    query = ~Q.zero(x) & ~Q.zero(y)
+    refutations = [
+        {Q.zero(x): True, Q.zero(x*y): True},
+        {Q.zero(y): True, Q.zero(x*y): True},
+        {Q.zero(x): True, Q.zero(y): True, Q.zero(x*y): True},
+        {Q.zero(x): True, Q.zero(y): False, Q.zero(x*y): True},
+        {Q.zero(x): False, Q.zero(y): True, Q.zero(x*y): True}]
+    assert not satisfiable(And(assumptions, facts, query), algorithm='dpll')
+    assert satisfiable(And(assumptions, facts, ~query), algorithm='dpll') in refutations
+    assert not satisfiable(And(assumptions, facts, query), algorithm='dpll2')
+    assert satisfiable(And(assumptions, facts, ~query), algorithm='dpll2') in refutations
+
+def test_satisfiable_bool():
+    from sympy.core.singleton import S
+    assert satisfiable(true) == {true: true}
+    assert satisfiable(S.true) == {true: true}
+    assert satisfiable(false) is False
+    assert satisfiable(S.false) is False
+
+
+def test_satisfiable_all_models():
+    from sympy.abc import A, B
+    assert next(satisfiable(False, all_models=True)) is False
+    assert list(satisfiable((A >> ~A) & A, all_models=True)) == [False]
+    assert list(satisfiable(True, all_models=True)) == [{true: true}]
+
+    models = [{A: True, B: False}, {A: False, B: True}]
+    result = satisfiable(A ^ B, all_models=True)
+    models.remove(next(result))
+    models.remove(next(result))
+    raises(StopIteration, lambda: next(result))
+    assert not models
+
+    assert list(satisfiable(Equivalent(A, B), all_models=True)) == \
+    [{A: False, B: False}, {A: True, B: True}]
+
+    models = [{A: False, B: False}, {A: False, B: True}, {A: True, B: True}]
+    for model in satisfiable(A >> B, all_models=True):
+        models.remove(model)
+    assert not models
+
+    # This is a santiy test to check that only the required number
+    # of solutions are generated. The expr below has 2**100 - 1 models
+    # which would time out the test if all are generated at once.
+    from sympy.utilities.iterables import numbered_symbols
+    from sympy.logic.boolalg import Or
+    sym = numbered_symbols()
+    X = [next(sym) for i in range(100)]
+    result = satisfiable(Or(*X), all_models=True)
+    for i in range(10):
+        assert next(result)
+
+
+def test_z3():
+    z3 = import_module("z3")
+
+    if not z3:
+        skip("z3 not installed.")
+    A, B, C = symbols('A,B,C')
+    x, y, z = symbols('x,y,z')
+    assert z3_satisfiable((x >= 2) & (x < 1)) is False
+    assert z3_satisfiable( A & ~A ) is False
+
+    model = z3_satisfiable(A & (~A | B | C))
+    assert bool(model) is True
+    assert model[A] is True
+
+    # test nonlinear function
+    assert z3_satisfiable((x ** 2 >= 2) & (x < 1) & (x > -1)) is False
+
+
+def test_z3_vs_lra_dpll2():
+    z3 = import_module("z3")
+    if z3 is None:
+        skip("z3 not installed.")
+
+    def boolean_formula_to_encoded_cnf(bf):
+        cnf = CNF.from_prop(bf)
+        enc = EncodedCNF()
+        enc.from_cnf(cnf)
+        return enc
+
+    def make_random_cnf(num_clauses=5, num_constraints=10, num_var=2):
+        assert num_clauses <= num_constraints
+        constraints = make_random_problem(num_variables=num_var, num_constraints=num_constraints, rational=False)
+        clauses = [[cons] for cons in constraints[:num_clauses]]
+        for cons in constraints[num_clauses:]:
+            if isinstance(cons, Unequality):
+                cons = ~cons
+            i = randint(0, num_clauses-1)
+            clauses[i].append(cons)
+
+        clauses = [Or(*clause) for clause in clauses]
+        cnf = And(*clauses)
+        return boolean_formula_to_encoded_cnf(cnf)
+
+    lra_dpll2_satisfiable = lambda x: dpll2_satisfiable(x, use_lra_theory=True)
+
+    for _ in range(50):
+        cnf = make_random_cnf(num_clauses=10, num_constraints=15, num_var=2)
+
+        try:
+            z3_sat = z3_satisfiable(cnf)
+        except z3.z3types.Z3Exception:
+            continue
+
+        lra_dpll2_sat = lra_dpll2_satisfiable(cnf) is not False
+
+        assert z3_sat == lra_dpll2_sat
+
+def test_issue_27733():
+    x, y = symbols('x,y')
+    clauses = [[1, -3, -2], [5, 7, -8, -6, -4], [-10, -9, 10, 11, -4], [-12, 13, 14], [-10, 9, -6, 11, -4],
+               [16, -15, 18, -19, -17], [11, -6, 10, -9], [9, 11, -10, -9], [2, -3, -1], [-13, 12], [-15, 3, -17],
+               [-16, -15, 19, -17], [-6, -9, 10, 11, -4], [20, -1, -2], [-23, -22, -21], [10, 11, -10, -9],
+               [9, 11, -4, -10], [24, -6, -4], [-14, 12], [-10, -9, 9, -6, 11], [25, -27, -26], [-15, 19, -18, -17],
+               [5, 8, -7, -6, -4], [-30, -29, 28], [12], [14]]
+
+    encoding = {Q.gt(y, i): i for i in range(1, 31) if i != 11 and i != 12}
+    encoding[Q.gt(x, 0)] = 11
+    encoding[Q.lt(x, 0)] = 12
+
+    cnf = EncodedCNF(clauses, encoding)
+    assert satisfiable(cnf, use_lra_theory=True) is False

phivenv/Lib/site-packages/sympy/logic/tests/test_lra_theory.py

@@ -0,0 +1,440 @@
+from sympy.core.numbers import Rational, I, oo
+from sympy.core.relational import Eq
+from sympy.core.symbol import symbols
+from sympy.core.singleton import S
+from sympy.matrices.dense import Matrix
+from sympy.matrices.dense import randMatrix
+from sympy.assumptions.ask import Q
+from sympy.logic.boolalg import And
+from sympy.abc import x, y, z
+from sympy.assumptions.cnf import CNF, EncodedCNF
+from sympy.functions.elementary.trigonometric import cos
+from sympy.external import import_module
+
+from sympy.logic.algorithms.lra_theory import LRASolver, UnhandledInput, LRARational, HANDLE_NEGATION
+from sympy.core.random import random, choice, randint
+from sympy.core.sympify import sympify
+from sympy.ntheory.generate import randprime
+from sympy.core.relational import StrictLessThan, StrictGreaterThan
+import itertools
+
+from sympy.testing.pytest import raises, XFAIL, skip
+
+def make_random_problem(num_variables=2, num_constraints=2, sparsity=.1, rational=True,
+                        disable_strict = False, disable_nonstrict=False, disable_equality=False):
+    def rand(sparsity=sparsity):
+        if random() < sparsity:
+            return sympify(0)
+        if rational:
+            int1, int2 = [randprime(0, 50) for _ in range(2)]
+            return Rational(int1, int2) * choice([-1, 1])
+        else:
+            return randint(1, 10) * choice([-1, 1])
+
+    variables = symbols('x1:%s' % (num_variables + 1))
+    constraints = []
+    for _ in range(num_constraints):
+        lhs, rhs = sum(rand() * x for x in variables), rand(sparsity=0) # sparsity=0  bc of bug with smtlib_code
+        options = []
+        if not disable_equality:
+            options += [Eq(lhs, rhs)]
+        if not disable_nonstrict:
+            options += [lhs <= rhs, lhs >= rhs]
+        if not disable_strict:
+            options += [lhs < rhs, lhs > rhs]
+
+        constraints.append(choice(options))
+
+    return constraints
+
+def check_if_satisfiable_with_z3(constraints):
+    from sympy.external.importtools import import_module
+    from sympy.printing.smtlib import smtlib_code
+    from sympy.logic.boolalg import And
+    boolean_formula = And(*constraints)
+    z3 = import_module("z3")
+    if z3:
+        smtlib_string = smtlib_code(boolean_formula)
+        s = z3.Solver()
+        s.from_string(smtlib_string)
+        res = str(s.check())
+        if res == 'sat':
+            return True
+        elif res == 'unsat':
+            return False
+        else:
+            raise ValueError(f"z3 was not able to check the satisfiability of {boolean_formula}")
+
+def find_rational_assignment(constr, assignment, iter=20):
+    eps = sympify(1)
+
+    for _ in range(iter):
+        assign = {key: val[0] + val[1]*eps for key, val in assignment.items()}
+        try:
+            for cons in constr:
+                assert cons.subs(assign) == True
+            return assign
+        except AssertionError:
+            eps = eps/2
+
+    return None
+
+def boolean_formula_to_encoded_cnf(bf):
+    cnf = CNF.from_prop(bf)
+    enc = EncodedCNF()
+    enc.from_cnf(cnf)
+    return enc
+
+
+def test_from_encoded_cnf():
+    s1, s2 = symbols("s1 s2")
+
+    # Test preprocessing
+    # Example is from section 3 of paper.
+    phi = (x >= 0) & ((x + y <= 2) | (x + 2 * y - z >= 6)) & (Eq(x + y, 2) | (x + 2 * y - z > 4))
+    enc = boolean_formula_to_encoded_cnf(phi)
+    lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
+    assert lra.A.shape == (2, 5)
+    assert str(lra.slack) == '[_s1, _s2]'
+    assert str(lra.nonslack) == '[x, y, z]'
+    assert lra.A == Matrix([[ 1,  1, 0, -1,  0],
+                            [-1, -2, 1,  0, -1]])
+    assert {(str(b.var), b.bound, b.upper, b.equality, b.strict) for b in lra.enc_to_boundary.values()} == {('_s1', 2, None, True, False),
+    ('_s1', 2, True, False, False),
+    ('_s2', -4, True, False, True),
+    ('_s2', -6, True, False, False),
+    ('x', 0, False, False, False)}
+
+
+def test_problem():
+    from sympy.logic.algorithms.lra_theory import LRASolver
+    from sympy.assumptions.cnf import CNF, EncodedCNF
+    cons = [-2 * x - 2 * y >= 7, -9 * y >= 7, -6 * y >= 5]
+    cnf = CNF().from_prop(And(*cons))
+    enc = EncodedCNF()
+    enc.from_cnf(cnf)
+    lra, _ = LRASolver.from_encoded_cnf(enc)
+    lra.assert_lit(1)
+    lra.assert_lit(2)
+    lra.assert_lit(3)
+    is_sat, assignment = lra.check()
+    assert is_sat is True
+
+
+def test_random_problems():
+    z3 = import_module("z3")
+    if z3 is None:
+        skip("z3 is not installed")
+
+    special_cases = []; x1, x2, x3 = symbols("x1 x2 x3")
+    special_cases.append([x1 - 3 * x2 <= -5, 6 * x1 + 4 * x2 <= 0, -7 * x1 + 3 * x2 <= 3])
+    special_cases.append([-3 * x1 >= 3, Eq(4 * x1, -1)])
+    special_cases.append([-4 * x1 < 4, 6 * x1 <= -6])
+    special_cases.append([-3 * x2 >= 7, 6 * x1 <= -5, -3 * x2 <= -4])
+    special_cases.append([x + y >= 2, x + y <= 1])
+    special_cases.append([x >= 0, x + y <= 2, x + 2 * y - z >= 6])  # from paper example
+    special_cases.append([-2 * x1 - 2 * x2 >= 7, -9 * x1 >= 7, -6 * x1 >= 5])
+    special_cases.append([2 * x1 > -3, -9 * x1 < -6, 9 * x1 <= 6])
+    special_cases.append([-2*x1 < -4, 9*x1 > -9])
+    special_cases.append([-6*x1 >= -1, -8*x1 + x2 >= 5, -8*x1 + 7*x2 < 4, x1 > 7])
+    special_cases.append([Eq(x1, 2), Eq(5*x1, -2), Eq(-7*x2, -6), Eq(9*x1 + 10*x2, 9)])
+    special_cases.append([Eq(3*x1, 6), Eq(x1 - 8*x2, -9), Eq(-7*x1 + 5*x2, 3), Eq(3*x2, 7)])
+    special_cases.append([-4*x1 < 4, 6*x1 <= -6])
+    special_cases.append([-3*x1 + 8*x2 >= -8, -10*x2 > 9, 8*x1 - 4*x2 < 8, 10*x1 - 9*x2 >= -9])
+    special_cases.append([x1 + 5*x2 >= -6, 9*x1 - 3*x2 >= -9, 6*x1 + 6*x2 < -10, -3*x1 + 3*x2 < -7])
+    special_cases.append([-9*x1 < 7, -5*x1 - 7*x2 < -1, 3*x1 + 7*x2 > 1, -6*x1 - 6*x2 > 9])
+    special_cases.append([9*x1 - 6*x2 >= -7, 9*x1 + 4*x2 < -8, -7*x2 <= 1, 10*x2 <= -7])
+
+    feasible_count = 0
+    for i in range(50):
+        if i % 8 == 0:
+            constraints = make_random_problem(num_variables=1, num_constraints=2, rational=False)
+        elif i % 8 == 1:
+            constraints = make_random_problem(num_variables=2, num_constraints=4, rational=False, disable_equality=True,
+                                              disable_nonstrict=True)
+        elif i % 8 == 2:
+            constraints = make_random_problem(num_variables=2, num_constraints=4, rational=False, disable_strict=True)
+        elif i % 8 == 3:
+            constraints = make_random_problem(num_variables=3, num_constraints=12, rational=False)
+        else:
+            constraints = make_random_problem(num_variables=3, num_constraints=6, rational=False)
+
+        if i < len(special_cases):
+            constraints = special_cases[i]
+
+        if False in constraints or True in constraints:
+            continue
+
+        phi = And(*constraints)
+        if phi == False:
+            continue
+        cnf = CNF.from_prop(phi); enc = EncodedCNF()
+        enc.from_cnf(cnf)
+        assert all(0 not in clause for clause in enc.data)
+
+        lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
+        s_subs = lra.s_subs
+
+        lra.run_checks = True
+        s_subs_rev = {value: key for key, value in s_subs.items()}
+        lits = {lit for clause in enc.data for lit in clause}
+
+        bounds = [(lra.enc_to_boundary[l], l) for l in lits if l in lra.enc_to_boundary]
+        bounds = sorted(bounds, key=lambda x: (str(x[0].var), x[0].bound, str(x[0].upper))) # to remove nondeterminism
+
+        for b, l in bounds:
+            if lra.result and lra.result[0] == False:
+                break
+            lra.assert_lit(l)
+
+        feasible = lra.check()
+
+        if feasible[0] == True:
+            feasible_count += 1
+            assert check_if_satisfiable_with_z3(constraints) is True
+            cons_funcs = [cons.func for cons in constraints]
+            assignment = feasible[1]
+            assignment = {key.var : value for key, value in assignment.items()}
+            if not (StrictLessThan in cons_funcs or StrictGreaterThan in cons_funcs):
+                assignment = {key: value[0] for key, value in assignment.items()}
+                for cons in constraints:
+                    assert cons.subs(assignment) == True
+
+            else:
+                rat_assignment = find_rational_assignment(constraints, assignment)
+                assert rat_assignment is not None
+        else:
+            assert check_if_satisfiable_with_z3(constraints) is False
+
+            conflict = feasible[1]
+            assert len(conflict) >= 2
+            conflict = {lra.enc_to_boundary[-l].get_inequality() for l in conflict}
+            conflict = {clause.subs(s_subs_rev) for clause in conflict}
+            assert check_if_satisfiable_with_z3(conflict) is False
+
+            # check that conflict clause is probably minimal
+            for subset in itertools.combinations(conflict, len(conflict)-1):
+                assert check_if_satisfiable_with_z3(subset) is True
+
+
+@XFAIL
+def test_pos_neg_zero():
+    bf = Q.positive(x) & Q.negative(x) & Q.zero(y)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
+    for lit in enc.encoding.values():
+        if lra.assert_lit(lit) is not None:
+            break
+    assert len(lra.enc_to_boundary) == 3
+    assert lra.check()[0] == False
+
+    bf = Q.positive(x) & Q.lt(x, -1)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
+    for lit in enc.encoding.values():
+        if lra.assert_lit(lit) is not None:
+            break
+    assert len(lra.enc_to_boundary) == 2
+    assert lra.check()[0] == False
+
+    bf = Q.positive(x) & Q.zero(x)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
+    for lit in enc.encoding.values():
+        if lra.assert_lit(lit) is not None:
+            break
+    assert len(lra.enc_to_boundary) == 2
+    assert lra.check()[0] == False
+
+    bf = Q.positive(x) & Q.zero(y)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
+    for lit in enc.encoding.values():
+        if lra.assert_lit(lit) is not None:
+            break
+    assert len(lra.enc_to_boundary) == 2
+    assert lra.check()[0] == True
+
+
+@XFAIL
+def test_pos_neg_infinite():
+    bf = Q.positive_infinite(x) & Q.lt(x, 10000000) & Q.positive_infinite(y)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
+    for lit in enc.encoding.values():
+        if lra.assert_lit(lit) is not None:
+            break
+    assert len(lra.enc_to_boundary) == 3
+    assert lra.check()[0] == False
+
+    bf = Q.positive_infinite(x) & Q.gt(x, 10000000) & Q.positive_infinite(y)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
+    for lit in enc.encoding.values():
+        if lra.assert_lit(lit) is not None:
+            break
+    assert len(lra.enc_to_boundary) == 3
+    assert lra.check()[0] == True
+
+    bf = Q.positive_infinite(x) & Q.negative_infinite(x)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
+    for lit in enc.encoding.values():
+        if lra.assert_lit(lit) is not None:
+            break
+    assert len(lra.enc_to_boundary) == 2
+    assert lra.check()[0] == False
+
+
+def test_binrel_evaluation():
+    bf = Q.gt(3, 2)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    lra, conflicts = LRASolver.from_encoded_cnf(enc, testing_mode=True)
+    assert len(lra.enc_to_boundary) == 0
+    assert conflicts == [[1]]
+
+    bf = Q.lt(3, 2)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    lra, conflicts = LRASolver.from_encoded_cnf(enc, testing_mode=True)
+    assert len(lra.enc_to_boundary) == 0
+    assert conflicts == [[-1]]
+
+
+def test_negation():
+    assert HANDLE_NEGATION is True
+    bf = Q.gt(x, 1) & ~Q.gt(x, 0)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
+    for clause in enc.data:
+        for lit in clause:
+            lra.assert_lit(lit)
+    assert len(lra.enc_to_boundary) == 2
+    assert lra.check()[0] == False
+    assert sorted(lra.check()[1]) in [[-1, 2], [-2, 1]]
+
+    bf = ~Q.gt(x, 1) & ~Q.lt(x, 0)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
+    for clause in enc.data:
+        for lit in clause:
+            lra.assert_lit(lit)
+    assert len(lra.enc_to_boundary) == 2
+    assert lra.check()[0] == True
+
+    bf = ~Q.gt(x, 0) & ~Q.lt(x, 1)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
+    for clause in enc.data:
+        for lit in clause:
+            lra.assert_lit(lit)
+    assert len(lra.enc_to_boundary) == 2
+    assert lra.check()[0] == False
+
+    bf = ~Q.gt(x, 0) & ~Q.le(x, 0)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
+    for clause in enc.data:
+        for lit in clause:
+            lra.assert_lit(lit)
+    assert len(lra.enc_to_boundary) == 2
+    assert lra.check()[0] == False
+
+    bf = ~Q.le(x+y, 2) & ~Q.ge(x-y, 2) & ~Q.ge(y, 0)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
+    for clause in enc.data:
+        for lit in clause:
+            lra.assert_lit(lit)
+    assert len(lra.enc_to_boundary) == 3
+    assert lra.check()[0] == False
+    assert len(lra.check()[1]) == 3
+    assert all(i > 0 for i in lra.check()[1])
+
+
+def test_unhandled_input():
+    nan = S.NaN
+    bf = Q.gt(3, nan) & Q.gt(x, nan)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    raises(ValueError, lambda: LRASolver.from_encoded_cnf(enc, testing_mode=True))
+
+    bf = Q.gt(3, I) & Q.gt(x, I)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    raises(UnhandledInput, lambda: LRASolver.from_encoded_cnf(enc, testing_mode=True))
+
+    bf = Q.gt(3, float("inf")) & Q.gt(x, float("inf"))
+    enc = boolean_formula_to_encoded_cnf(bf)
+    raises(UnhandledInput, lambda: LRASolver.from_encoded_cnf(enc, testing_mode=True))
+
+    bf = Q.gt(3, oo) & Q.gt(x, oo)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    raises(UnhandledInput, lambda: LRASolver.from_encoded_cnf(enc, testing_mode=True))
+
+    # test non-linearity
+    bf = Q.gt(x**2 + x, 2)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    raises(UnhandledInput, lambda: LRASolver.from_encoded_cnf(enc, testing_mode=True))
+
+    bf = Q.gt(cos(x) + x, 2)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    raises(UnhandledInput, lambda: LRASolver.from_encoded_cnf(enc, testing_mode=True))
+
+@XFAIL
+def test_infinite_strict_inequalities():
+    # Extensive testing of the interaction between strict inequalities
+    # and constraints containing infinity is needed because
+    # the paper's rule for strict inequalities don't work when
+    # infinite numbers are allowed. Using the paper's rules you
+    # can end up with situations where oo + delta > oo is considered
+    # True when oo + delta should be equal to oo.
+    # See https://math.stackexchange.com/questions/4757069/can-this-method-of-converting-strict-inequalities-to-equisatisfiable-nonstrict-i
+    bf = (-x - y >= -float("inf")) & (x > 0) & (y >= float("inf"))
+    enc = boolean_formula_to_encoded_cnf(bf)
+    lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
+    for lit in sorted(enc.encoding.values()):
+        if lra.assert_lit(lit) is not None:
+            break
+    assert len(lra.enc_to_boundary) == 3
+    assert lra.check()[0] == True
+
+
+def test_pivot():
+    for _ in range(10):
+        m = randMatrix(5)
+        rref = m.rref()
+        for _ in range(5):
+            i, j = randint(0, 4), randint(0, 4)
+            if m[i, j] != 0:
+                assert LRASolver._pivot(m, i, j).rref() == rref
+
+
+def test_reset_bounds():
+    bf = Q.ge(x, 1) & Q.lt(x, 1)
+    enc = boolean_formula_to_encoded_cnf(bf)
+    lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
+    for clause in enc.data:
+        for lit in clause:
+            lra.assert_lit(lit)
+    assert len(lra.enc_to_boundary) == 2
+    assert lra.check()[0] == False
+
+    lra.reset_bounds()
+    assert lra.check()[0] == True
+    for var in lra.all_var:
+        assert var.upper == LRARational(float("inf"), 0)
+        assert var.upper_from_eq == False
+        assert var.upper_from_neg == False
+        assert var.lower == LRARational(-float("inf"), 0)
+        assert var.lower_from_eq == False
+        assert var.lower_from_neg == False
+        assert var.assign == LRARational(0, 0)
+        assert var.var is not None
+        assert var.col_idx is not None
+
+
+def test_empty_cnf():
+    cnf = CNF()
+    enc = EncodedCNF()
+    enc.from_cnf(cnf)
+    lra, conflict = LRASolver.from_encoded_cnf(enc)
+    assert len(conflict) == 0
+    assert lra.check() == (True, {})

phivenv/Lib/site-packages/sympy/logic/utilities/__init__.py

@@ -0,0 +1,3 @@
+from .dimacs import load_file
+
+__all__ = ['load_file']

phivenv/Lib/site-packages/sympy/logic/utilities/dimacs.py

@@ -0,0 +1,69 @@
+"""For reading in DIMACS file format
+
+www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/satformat.ps
+
+"""
+
+from sympy.core import Symbol
+from sympy.logic.boolalg import And, Or
+import re
+from pathlib import Path
+
+
+def load(s):
+    """Loads a boolean expression from a string.
+
+    Examples
+    ========
+
+    >>> from sympy.logic.utilities.dimacs import load
+    >>> load('1')
+    cnf_1
+    >>> load('1 2')
+    cnf_1 | cnf_2
+    >>> load('1 \\n 2')
+    cnf_1 & cnf_2
+    >>> load('1 2 \\n 3')
+    cnf_3 & (cnf_1 | cnf_2)
+    """
+    clauses = []
+
+    lines = s.split('\n')
+
+    pComment = re.compile(r'c.*')
+    pStats = re.compile(r'p\s*cnf\s*(\d*)\s*(\d*)')
+
+    while len(lines) > 0:
+        line = lines.pop(0)
+
+        # Only deal with lines that aren't comments
+        if not pComment.match(line):
+            m = pStats.match(line)
+
+            if not m:
+                nums = line.rstrip('\n').split(' ')
+                list = []
+                for lit in nums:
+                    if lit != '':
+                        if int(lit) == 0:
+                            continue
+                        num = abs(int(lit))
+                        sign = True
+                        if int(lit) < 0:
+                            sign = False
+
+                        if sign:
+                            list.append(Symbol("cnf_%s" % num))
+                        else:
+                            list.append(~Symbol("cnf_%s" % num))
+
+                if len(list) > 0:
+                    clauses.append(Or(*list))
+
+    return And(*clauses)
+
+
+def load_file(location):
+    """Loads a boolean expression from a file."""
+    s = Path(location).read_text()
+    return load(s)

phivenv/Lib/site-packages/sympy/matrices/__init__.py

@@ -0,0 +1,72 @@
+"""A module that handles matrices.
+
+Includes functions for fast creating matrices like zero, one/eye, random
+matrix, etc.
+"""
+from .exceptions import ShapeError, NonSquareMatrixError
+from .kind import MatrixKind
+from .dense import (
+    GramSchmidt, casoratian, diag, eye, hessian, jordan_cell,
+    list2numpy, matrix2numpy, matrix_multiply_elementwise, ones,
+    randMatrix, rot_axis1, rot_axis2, rot_axis3, rot_ccw_axis1,
+    rot_ccw_axis2, rot_ccw_axis3, rot_givens,
+    symarray, wronskian, zeros)
+from .dense import MutableDenseMatrix
+from .matrixbase import DeferredVector, MatrixBase
+
+MutableMatrix = MutableDenseMatrix
+Matrix = MutableMatrix
+
+from .sparse import MutableSparseMatrix
+from .sparsetools import banded
+from .immutable import ImmutableDenseMatrix, ImmutableSparseMatrix
+
+ImmutableMatrix = ImmutableDenseMatrix
+SparseMatrix = MutableSparseMatrix
+
+from .expressions import (
+    MatrixSlice, BlockDiagMatrix, BlockMatrix, FunctionMatrix, Identity,
+    Inverse, MatAdd, MatMul, MatPow, MatrixExpr, MatrixSymbol, Trace,
+    Transpose, ZeroMatrix, OneMatrix, blockcut, block_collapse, matrix_symbols, Adjoint,
+    hadamard_product, HadamardProduct, HadamardPower, Determinant, det,
+    diagonalize_vector, DiagMatrix, DiagonalMatrix, DiagonalOf, trace,
+    DotProduct, kronecker_product, KroneckerProduct,
+    PermutationMatrix, MatrixPermute, MatrixSet, Permanent, per)
+
+from .utilities import dotprodsimp
+
+__all__ = [
+    'ShapeError', 'NonSquareMatrixError', 'MatrixKind',
+
+    'GramSchmidt', 'casoratian', 'diag', 'eye', 'hessian', 'jordan_cell',
+    'list2numpy', 'matrix2numpy', 'matrix_multiply_elementwise', 'ones',
+    'randMatrix', 'rot_axis1', 'rot_axis2', 'rot_axis3', 'symarray',
+    'wronskian', 'zeros', 'rot_ccw_axis1', 'rot_ccw_axis2', 'rot_ccw_axis3',
+    'rot_givens',
+
+    'MutableDenseMatrix',
+
+    'DeferredVector', 'MatrixBase',
+
+    'Matrix', 'MutableMatrix',
+
+    'MutableSparseMatrix',
+
+    'banded',
+
+    'ImmutableDenseMatrix', 'ImmutableSparseMatrix',
+
+    'ImmutableMatrix', 'SparseMatrix',
+
+    'MatrixSlice', 'BlockDiagMatrix', 'BlockMatrix', 'FunctionMatrix',
+    'Identity', 'Inverse', 'MatAdd', 'MatMul', 'MatPow', 'MatrixExpr',
+    'MatrixSymbol', 'Trace', 'Transpose', 'ZeroMatrix', 'OneMatrix',
+    'blockcut', 'block_collapse', 'matrix_symbols', 'Adjoint',
+    'hadamard_product', 'HadamardProduct', 'HadamardPower', 'Determinant',
+    'det', 'diagonalize_vector', 'DiagMatrix', 'DiagonalMatrix',
+    'DiagonalOf', 'trace', 'DotProduct', 'kronecker_product',
+    'KroneckerProduct', 'PermutationMatrix', 'MatrixPermute', 'MatrixSet',
+    'Permanent', 'per',
+
+    'dotprodsimp',
+]