class_docstr: 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
class_docstr_tok: ["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"]
docstr: 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]]
code: 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 matirx 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,
      )
  
imports: 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
label_desc: Use image node_id 2 for calling the LRASolver obj's underlying member method code with example usage: obj.from_encoded_cnf(encoded_cnf, testing_mode) and returns: LRASolver,  conflicts