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: Performs a pivot operation about entry i, j of M by performing
  a series of row operations on a copy of M and returing the result.
  The original M is left unmodified.
  
  Conceptually, M represents a system of equations and pivoting
  can be thought of as rearranging equation i to be in terms of
  variable j and then substituting in the rest of the equations
  to get rid of other occurances of variable j.
  
  Example
  =======
  
  >>> from sympy.matrices.dense import Matrix
  >>> from sympy.logic.algorithms.lra_theory import LRASolver
  >>> from sympy import var
  >>> Matrix(3, 3, var('a:i'))
  Matrix([
  [a, b, c],
  [d, e, f],
  [g, h, i]])
  
  This matrix is equivalent to:
  0 = a*x + b*y + c*z
  0 = d*x + e*y + f*z
  0 = g*x + h*y + i*z
  
  >>> LRASolver._pivot(_, 1, 0)
  Matrix([
  [ 0, -a*e/d + b, -a*f/d + c],
  [-1,       -e/d,       -f/d],
  [ 0,  h - e*g/d,  i - f*g/d]])
  
  We rearrange equation 1 in terms of variable 0 (x)
  and substitute to remove x from the other equations.
  
  0 = 0 + (-a*e/d + b)*y + (-a*f/d + c)*z
  0 = -x + (-e/d)*y + (-f/d)*z
  0 = 0 + (h - e*g/d)*y + (i - f*g/d)*z
code: def _pivot(M, i, j):
      """
      Performs a pivot operation about entry i, j of M by performing
      a series of row operations on a copy of M and returing the result.
      The original M is left unmodified.
  
      Conceptually, M represents a system of equations and pivoting
      can be thought of as rearranging equation i to be in terms of
      variable j and then substituting in the rest of the equations
      to get rid of other occurances of variable j.
  
      Example
      =======
  
      >>> from sympy.matrices.dense import Matrix
      >>> from sympy.logic.algorithms.lra_theory import LRASolver
      >>> from sympy import var
      >>> Matrix(3, 3, var('a:i'))
      Matrix([
      [a, b, c],
      [d, e, f],
      [g, h, i]])
  
      This matrix is equivalent to:
      0 = a*x + b*y + c*z
      0 = d*x + e*y + f*z
      0 = g*x + h*y + i*z
  
      >>> LRASolver._pivot(_, 1, 0)
      Matrix([
      [ 0, -a*e/d + b, -a*f/d + c],
      [-1,       -e/d,       -f/d],
      [ 0,  h - e*g/d,  i - f*g/d]])
  
      We rearrange equation 1 in terms of variable 0 (x)
      and substitute to remove x from the other equations.
  
      0 = 0 + (-a*e/d + b)*y + (-a*f/d + c)*z
      0 = -x + (-e/d)*y + (-f/d)*z
      0 = 0 + (h - e*g/d)*y + (i - f*g/d)*z
      """
      _, _, Mij = M[i, :], M[:, j], M[i, j]
      if Mij == 0:
          raise ZeroDivisionError(
              "Tried to pivot about zero-valued entry."
          )
      A = M.copy()
      A[i, :] = -A[i, :] / Mij
      for row in range(M.shape[0]):
          if row != i:
              A[row, :] = A[row, :] + A[row, j] * A[i, :]
  
      return A
  
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 10 for calling the LRASolver obj's underlying member method code with example usage: obj._pivot(M, i, j) and returns: A