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: 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.
code: 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
  
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 6 for calling the LRASolver obj's underlying member method code with example usage: obj._assert_lower(xi, ci, from_equality, from_neg) and returns: None, None, self