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: 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.
code: 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
  
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 4 for calling the LRASolver obj's underlying member method code with example usage: obj.assert_lit(enc_constraint) and returns: res, None, None, None