code: def test_from_encoded_cnf():
      s1, s2 = symbols("s1 s2")
  
      # Test preprocessing
      # Example is from section 3 of paper.
      phi = (
          (x >= 0)
          & ((x + y <= 2) | (x + 2 * y - z >= 6))
          & (Eq(x + y, 2) | (x + 2 * y - z > 4))
      )
      enc = boolean_formula_to_encoded_cnf(phi)
      lra, _ = LRASolver.from_encoded_cnf(enc, testing_mode=True)
      assert lra.A.shape == (2, 5)
      assert str(lra.slack) == "[_s1, _s2]"
      assert str(lra.nonslack) == "[x, y, z]"
      assert lra.A == Matrix([[1, 1, 0, -1, 0], [-1, -2, 1, 0, -1]])
      assert {
          (str(b.var), b.bound, b.upper, b.equality, b.strict)
          for b in lra.enc_to_boundary.values()
      } == {
          ("_s1", 2, None, True, False),
          ("_s1", 2, True, False, False),
          ("_s2", -4, True, False, True),
          ("_s2", -6, True, False, False),
          ("x", 0, False, False, False),
      }
  
imports: from sympy.core.numbers import Rational, I, oo
  from sympy.core.relational import Eq
  from sympy.core.symbol import symbols
  from sympy.core.singleton import S
  from sympy.matrices.dense import Matrix
  from sympy.matrices.dense import randMatrix
  from sympy.assumptions.ask import Q
  from sympy.logic.boolalg import And
  from sympy.abc import x, y, z
  from sympy.assumptions.cnf import CNF, EncodedCNF
  from sympy.functions.elementary.trigonometric import cos
  from sympy.external import import_module
  from sympy.logic.algorithms.lra_theory import LRASolver, UnhandledInput, LRARational, HANDLE_NEGATION
  from sympy.core.random import random, choice, randint
  from sympy.core.sympify import sympify
  from sympy.ntheory.generate import randprime
  from sympy.core.relational import StrictLessThan, StrictGreaterThan
  import itertools
  from sympy.testing.pytest import raises, XFAIL, skip
label_desc: Use image node_id 5 for calling a global function with example usage: test_from_encoded_cnf() without return types