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: 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
code: 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)
      iteration = 0
      while True:
          iteration += 1
  
          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 = sorted(cand, key=lambda v: v.col_idx)[0]  # 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 = sorted(cand, key=lambda v: str(v))[0]
              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 = sorted(cand, key=lambda v: v.col_idx)[0]
              M = self._pivot_and_update(
                  M, basic, nonbasic, xi, xj, xi.upper
              )
  
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 8 for calling the LRASolver obj's underlying member method code with example usage: obj.check() and returns: True,  unknown, self, True,  unknown, False,  conflict, False,  conflict