code: def smtlib_code(
      expr,
      auto_assert=True,
      auto_declare=True,
      precision=None,
      symbol_table=None,
      known_types=None,
      known_constants=None,
      known_functions=None,
      prefix_expressions=None,
      suffix_expressions=None,
      log_warn=None,
  ):
      r"""Converts ``expr`` to a string of smtlib code.
  
      Parameters
      ==========
  
      expr : Expr | List[Expr]
          A SymPy expression or system to be converted.
      auto_assert : bool, optional
          If false, do not modify expr and produce only the S-Expression equivalent of expr.
          If true, assume expr is a system and assert each boolean element.
      auto_declare : bool, optional
          If false, do not produce declarations for the symbols used in expr.
          If true, prepend all necessary declarations for variables used in expr based on symbol_table.
      precision : integer, optional
          The ``evalf(..)`` precision for numbers such as pi.
      symbol_table : dict, optional
          A dictionary where keys are ``Symbol`` or ``Function`` instances and values are their Python type i.e. ``bool``, ``int``, ``float``, or ``Callable[...]``.
          If incomplete, an attempt will be made to infer types from ``expr``.
      known_types: dict, optional
          A dictionary where keys are ``bool``, ``int``, ``float`` etc. and values are their corresponding SMT type names.
          If not given, a partial listing compatible with several solvers will be used.
      known_functions : dict, optional
          A dictionary where keys are ``Function``, ``Relational``, ``BooleanFunction``, or ``Expr`` instances and values are their SMT string representations.
          If not given, a partial listing optimized for dReal solver (but compatible with others) will be used.
      known_constants: dict, optional
          A dictionary where keys are ``NumberSymbol`` instances and values are their SMT variable names.
          When using this feature, extra caution must be taken to avoid naming collisions between user symbols and listed constants.
          If not given, constants will be expanded inline i.e. ``3.14159`` instead of ``MY_SMT_VARIABLE_FOR_PI``.
      prefix_expressions: list, optional
          A list of lists of ``str`` and/or expressions to convert into SMTLib and prefix to the output.
      suffix_expressions: list, optional
          A list of lists of ``str`` and/or expressions to convert into SMTLib and postfix to the output.
      log_warn: lambda function, optional
          A function to record all warnings during potentially risky operations.
          Soundness is a core value in SMT solving, so it is good to log all assumptions made.
  
      Examples
      ========
      >>> from sympy import smtlib_code, symbols, sin, Eq
      >>> x = symbols('x')
      >>> smtlib_code(sin(x).series(x).removeO(), log_warn=print)
      Could not infer type of `x`. Defaulting to float.
      Non-Boolean expression `x**5/120 - x**3/6 + x` will not be asserted. Converting to SMTLib verbatim.
      '(declare-const x Real)\n(+ x (* (/ -1 6) (pow x 3)) (* (/ 1 120) (pow x 5)))'
  
      >>> from sympy import Rational
      >>> x, y, tau = symbols("x, y, tau")
      >>> smtlib_code((2*tau)**Rational(7, 2), log_warn=print)
      Could not infer type of `tau`. Defaulting to float.
      Non-Boolean expression `8*sqrt(2)*tau**(7/2)` will not be asserted. Converting to SMTLib verbatim.
      '(declare-const tau Real)\n(* 8 (pow 2 (/ 1 2)) (pow tau (/ 7 2)))'
  
      ``Piecewise`` expressions are implemented with ``ite`` expressions by default.
      Note that if the ``Piecewise`` lacks a default term, represented by
      ``(expr, True)`` then an error will be thrown.  This is to prevent
      generating an expression that may not evaluate to anything.
  
      >>> from sympy import Piecewise
      >>> pw = Piecewise((x + 1, x > 0), (x, True))
      >>> smtlib_code(Eq(pw, 3), symbol_table={x: float}, log_warn=print)
      '(declare-const x Real)\n(assert (= (ite (> x 0) (+ 1 x) x) 3))'
  
      Custom printing can be defined for certain types by passing a dictionary of
      PythonType : "SMT Name" to the ``known_types``, ``known_constants``, and ``known_functions`` kwargs.
  
      >>> from typing import Callable
      >>> from sympy import Function, Add
      >>> f = Function('f')
      >>> g = Function('g')
      >>> smt_builtin_funcs = {  # functions our SMT solver will understand
      ...   f: "existing_smtlib_fcn",
      ...   Add: "sum",
      ... }
      >>> user_def_funcs = {  # functions defined by the user must have their types specified explicitly
      ...   g: Callable[[int], float],
      ... }
      >>> smtlib_code(f(x) + g(x), symbol_table=user_def_funcs, known_functions=smt_builtin_funcs, log_warn=print)
      Non-Boolean expression `f(x) + g(x)` will not be asserted. Converting to SMTLib verbatim.
      '(declare-const x Int)\n(declare-fun g (Int) Real)\n(sum (existing_smtlib_fcn x) (g x))'
      """
      log_warn = log_warn or (lambda _: None)
  
      if not isinstance(expr, list):
          expr = [expr]
      expr = [
          sympy.sympify(
              _, strict=True, evaluate=False, convert_xor=False
          )
          for _ in expr
      ]
  
      if not symbol_table:
          symbol_table = {}
      symbol_table = _auto_infer_smtlib_types(
          *expr, symbol_table=symbol_table
      )
      # See [FALLBACK RULES]
      # Need SMTLibPrinter to populate known_functions and known_constants first.
  
      settings = {}
      if precision:
          settings["precision"] = precision
      del precision
  
      if known_types:
          settings["known_types"] = known_types
      del known_types
  
      if known_functions:
          settings["known_functions"] = known_functions
      del known_functions
  
      if known_constants:
          settings["known_constants"] = known_constants
      del known_constants
  
      if not prefix_expressions:
          prefix_expressions = []
      if not suffix_expressions:
          suffix_expressions = []
  
      p = SMTLibPrinter(settings, symbol_table)
      del symbol_table
  
      # [FALLBACK RULES]
      for e in expr:
          for sym in e.atoms(Symbol, Function):
              if (
                  sym.is_Symbol
                  and sym not in p._known_constants
                  and sym not in p.symbol_table
              ):
                  log_warn(
                      f"Could not infer type of `{sym}`. Defaulting to float."
                  )
                  p.symbol_table[sym] = float
              if (
                  sym.is_Function
                  and type(sym) not in p._known_functions
                  and type(sym) not in p.symbol_table
                  and not sym.is_Piecewise
              ):
                  raise TypeError(
                      f"Unknown type of undefined function `{sym}`. "
                      f"Must be mapped to ``str`` in known_functions or mapped to ``Callable[..]`` in symbol_table."
                  )
  
      declarations = []
      if auto_declare:
          constants = {
              sym.name: sym
              for e in expr
              for sym in e.free_symbols
              if sym not in p._known_constants
          }
          functions = {
              fnc.name: fnc
              for e in expr
              for fnc in e.atoms(Function)
              if type(fnc) not in p._known_functions
              and not fnc.is_Piecewise
          }
          declarations = [
              _auto_declare_smtlib(sym, p, log_warn)
              for sym in constants.values()
          ] + [
              _auto_declare_smtlib(fnc, p, log_warn)
              for fnc in functions.values()
          ]
          declarations = [decl for decl in declarations if decl]
  
      if auto_assert:
          expr = [_auto_assert_smtlib(e, p, log_warn) for e in expr]
  
      # return SMTLibPrinter().doprint(expr)
      return "\n".join(
          [
              # ';; PREFIX EXPRESSIONS',
              *[
                  e if isinstance(e, str) else p.doprint(e)
                  for e in prefix_expressions
              ],
              # ';; DECLARATIONS',
              *sorted(e for e in declarations),
              # ';; EXPRESSIONS',
              *[
                  e if isinstance(e, str) else p.doprint(e)
                  for e in expr
              ],
              # ';; SUFFIX EXPRESSIONS',
              *[
                  e if isinstance(e, str) else p.doprint(e)
                  for e in suffix_expressions
              ],
          ]
      )
  
imports: import typing
  import sympy
  from sympy.core import Add, Mul
  from sympy.core import Symbol, Expr, Float, Rational, Integer, Basic
  from sympy.core.function import UndefinedFunction, Function
  from sympy.core.relational import Relational, Unequality, Equality, LessThan, GreaterThan, StrictLessThan, StrictGreaterThan
  from sympy.functions.elementary.complexes import Abs
  from sympy.functions.elementary.exponential import exp, log, Pow
  from sympy.functions.elementary.hyperbolic import sinh, cosh, tanh
  from sympy.functions.elementary.miscellaneous import Min, Max
  from sympy.functions.elementary.piecewise import Piecewise
  from sympy.functions.elementary.trigonometric import sin, cos, tan, asin, acos, atan, atan2
  from sympy.logic.boolalg import And, Or, Xor, Implies, Boolean
  from sympy.logic.boolalg import BooleanTrue, BooleanFalse, BooleanFunction, Not, ITE
  from sympy.printing.printer import Printer
  from sympy.sets import Interval
  from mpmath.libmp.libmpf import prec_to_dps, to_str
  from sympy.assumptions.assume import AppliedPredicate
  from sympy.assumptions.relation.binrel import AppliedBinaryRelation
  from sympy.assumptions.ask import Q
  from sympy.assumptions.relation.equality import StrictGreaterThanPredicate, StrictLessThanPredicate, GreaterThanPredicate, LessThanPredicate, EqualityPredicate
label_desc: Use image node_id 1 for calling a global function with example usage: smtlib_code(expr, auto_assert, auto_declare, precision, symbol_table, known_types, known_constants, known_functions, prefix_expressions, suffix_expressions, log_warn) and returns: str