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: Use the "from_encoded_cnf" method to create a new LRASolver.
code: 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 Boundry 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
  
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 1 to create a new LRASolver object  with example: obj = LRASolver(A, slack_variables, nonslack_variables, enc_to_boundary, s_subs, testing_mode)