code: def _preprocess(enc_cnf):
      """
      Returns an encoded cnf with only Q.eq, Q.gt, Q.lt,
      Q.ge, and Q.le predicate.
  
      Converts every unequality into a disjunction of strict
      inequalities. For example, x != 3 would become
      x < 3 OR x > 3.
  
      Also converts all negated Q.ne predicates into
      equalities.
      """
  
      # loops through each literal in each clause
      # to construct a new, preprocessed encodedCNF
  
      enc_cnf = enc_cnf.copy()
      cur_enc = 1
      rev_encoding = {
          value: key for key, value in enc_cnf.encoding.items()
      }
  
      new_encoding = {}
      new_data = []
      for clause in enc_cnf.data:
          new_clause = []
          for lit in clause:
              if lit == 0:
                  new_clause.append(lit)
                  new_encoding[lit] = False
                  continue
              prop = rev_encoding[abs(lit)]
              negated = lit < 0
              sign = (lit > 0) - (lit < 0)
  
              prop = _pred_to_binrel(prop)
  
              if not isinstance(prop, AppliedPredicate):
                  if prop not in new_encoding:
                      new_encoding[prop] = cur_enc
                      cur_enc += 1
                  lit = new_encoding[prop]
                  new_clause.append(sign * lit)
                  continue
  
              if negated and prop.function == Q.eq:
                  negated = False
                  prop = Q.ne(*prop.arguments)
  
              if prop.function == Q.ne:
                  arg1, arg2 = prop.arguments
                  if negated:
                      new_prop = Q.eq(arg1, arg2)
                      if new_prop not in new_encoding:
                          new_encoding[new_prop] = cur_enc
                          cur_enc += 1
  
                      new_enc = new_encoding[new_prop]
                      new_clause.append(new_enc)
                      continue
                  else:
                      new_props = (Q.gt(arg1, arg2), Q.lt(arg1, arg2))
                      for new_prop in new_props:
                          if new_prop not in new_encoding:
                              new_encoding[new_prop] = cur_enc
                              cur_enc += 1
  
                          new_enc = new_encoding[new_prop]
                          new_clause.append(new_enc)
                      continue
  
              if prop.function == Q.eq and negated:
                  assert False
  
              if prop not in new_encoding:
                  new_encoding[prop] = cur_enc
                  cur_enc += 1
              new_clause.append(new_encoding[prop] * sign)
          new_data.append(new_clause)
  
      assert len(new_encoding) >= cur_enc - 1
  
      enc_cnf = EncodedCNF(new_data, new_encoding)
      return enc_cnf
  
file_path: sympy/sympy/assumptions/lra_satask.py
imports: from sympy.assumptions.assume import global_assumptions
  from sympy.assumptions.cnf import CNF, EncodedCNF
  from sympy.assumptions.ask import Q
  from sympy.logic.inference import satisfiable
  from sympy.logic.algorithms.lra_theory import UnhandledInput, ALLOWED_PRED
  from sympy.matrices.kind import MatrixKind
  from sympy.core.kind import NumberKind
  from sympy.assumptions.assume import AppliedPredicate
  from sympy.core.mul import Mul
  from sympy.core.singleton import S
label_desc: Use image node_id 3 for calling a global function with example usage: _preprocess(enc_cnf) and returns: enc_cnf