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: Pivots basic variable xi with nonbasic variable xj,
  and sets value of xi to v and adjusts the values of all basic variables
  to keep equations satisfied.
code: def _pivot_and_update(self, M, basic, nonbasic, xi, xj, v):
      """
      Pivots basic variable xi with nonbasic variable xj,
      and sets value of xi to v and adjusts the values of all basic variables
      to keep equations satisfied.
      """
      i, j = basic[xi], xj.col_idx
      assert M[i, j] != 0
      theta = (v - xi.assign) * (1 / M[i, j])
      xi.assign = v
      xj.assign = xj.assign + theta
      for xk in basic:
          if xk != xi:
              k = basic[xk]
              akj = M[k, j]
              xk.assign = xk.assign + theta * akj
      # pivot
      basic[xj] = basic[xi]
      del basic[xi]
      nonbasic.add(xi)
      nonbasic.remove(xj)
      return self._pivot(M, i, j)
  
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 9 for calling the LRASolver obj's underlying member method code with example usage: obj._pivot_and_update(M, basic, nonbasic, xi, xj, v) and returns: self