Coverage for /usr/lib/python3/dist-packages/sympy/printing/smtlib.py: 26%
176 statements
« prev ^ index » next coverage.py v7.9.1, created at 2025-06-14 15:55 +0200
1import typing
3import sympy
4from sympy.core import Add, Mul
5from sympy.core import Symbol, Expr, Float, Rational, Integer, Basic
6from sympy.core.function import UndefinedFunction, Function
7from sympy.core.relational import Relational, Unequality, Equality, LessThan, GreaterThan, StrictLessThan, StrictGreaterThan
8from sympy.functions.elementary.complexes import Abs
9from sympy.functions.elementary.exponential import exp, log, Pow
10from sympy.functions.elementary.hyperbolic import sinh, cosh, tanh
11from sympy.functions.elementary.miscellaneous import Min, Max
12from sympy.functions.elementary.piecewise import Piecewise
13from sympy.functions.elementary.trigonometric import sin, cos, tan, asin, acos, atan, atan2
14from sympy.logic.boolalg import And, Or, Xor, Implies, Boolean
15from sympy.logic.boolalg import BooleanTrue, BooleanFalse, BooleanFunction, Not, ITE
16from sympy.printing.printer import Printer
17from sympy.sets import Interval
20class SMTLibPrinter(Printer):
21 printmethod = "_smtlib"
23 # based on dReal, an automated reasoning tool for solving problems that can be encoded as first-order logic formulas over the real numbers.
24 # dReal's special strength is in handling problems that involve a wide range of nonlinear real functions.
25 _default_settings: dict = {
26 'precision': None,
27 'known_types': {
28 bool: 'Bool',
29 int: 'Int',
30 float: 'Real'
31 },
32 'known_constants': {
33 # pi: 'MY_VARIABLE_PI_DECLARED_ELSEWHERE',
34 },
35 'known_functions': {
36 Add: '+',
37 Mul: '*',
39 Equality: '=',
40 LessThan: '<=',
41 GreaterThan: '>=',
42 StrictLessThan: '<',
43 StrictGreaterThan: '>',
45 exp: 'exp',
46 log: 'log',
47 Abs: 'abs',
48 sin: 'sin',
49 cos: 'cos',
50 tan: 'tan',
51 asin: 'arcsin',
52 acos: 'arccos',
53 atan: 'arctan',
54 atan2: 'arctan2',
55 sinh: 'sinh',
56 cosh: 'cosh',
57 tanh: 'tanh',
58 Min: 'min',
59 Max: 'max',
60 Pow: 'pow',
62 And: 'and',
63 Or: 'or',
64 Xor: 'xor',
65 Not: 'not',
66 ITE: 'ite',
67 Implies: '=>',
68 }
69 }
71 symbol_table: dict
73 def __init__(self, settings: typing.Optional[dict] = None,
74 symbol_table=None):
75 settings = settings or {}
76 self.symbol_table = symbol_table or {}
77 Printer.__init__(self, settings)
78 self._precision = self._settings['precision']
79 self._known_types = dict(self._settings['known_types'])
80 self._known_constants = dict(self._settings['known_constants'])
81 self._known_functions = dict(self._settings['known_functions'])
83 for _ in self._known_types.values(): assert self._is_legal_name(_)
84 for _ in self._known_constants.values(): assert self._is_legal_name(_)
85 # for _ in self._known_functions.values(): assert self._is_legal_name(_) # +, *, <, >, etc.
87 def _is_legal_name(self, s: str):
88 if not s: return False
89 if s[0].isnumeric(): return False
90 return all(_.isalnum() or _ == '_' for _ in s)
92 def _s_expr(self, op: str, args: typing.Union[list, tuple]) -> str:
93 args_str = ' '.join(
94 a if isinstance(a, str)
95 else self._print(a)
96 for a in args
97 )
98 return f'({op} {args_str})'
100 def _print_Function(self, e):
101 if e in self._known_functions:
102 op = self._known_functions[e]
103 elif type(e) in self._known_functions:
104 op = self._known_functions[type(e)]
105 elif type(type(e)) == UndefinedFunction:
106 op = e.name
107 else:
108 op = self._known_functions[e] # throw KeyError
110 return self._s_expr(op, e.args)
112 def _print_Relational(self, e: Relational):
113 return self._print_Function(e)
115 def _print_BooleanFunction(self, e: BooleanFunction):
116 return self._print_Function(e)
118 def _print_Expr(self, e: Expr):
119 return self._print_Function(e)
121 def _print_Unequality(self, e: Unequality):
122 if type(e) in self._known_functions:
123 return self._print_Relational(e) # default
124 else:
125 eq_op = self._known_functions[Equality]
126 not_op = self._known_functions[Not]
127 return self._s_expr(not_op, [self._s_expr(eq_op, e.args)])
129 def _print_Piecewise(self, e: Piecewise):
130 def _print_Piecewise_recursive(args: typing.Union[list, tuple]):
131 e, c = args[0]
132 if len(args) == 1:
133 assert (c is True) or isinstance(c, BooleanTrue)
134 return self._print(e)
135 else:
136 ite = self._known_functions[ITE]
137 return self._s_expr(ite, [
138 c, e, _print_Piecewise_recursive(args[1:])
139 ])
141 return _print_Piecewise_recursive(e.args)
143 def _print_Interval(self, e: Interval):
144 if e.start.is_infinite and e.end.is_infinite:
145 return ''
146 elif e.start.is_infinite != e.end.is_infinite:
147 raise ValueError(f'One-sided intervals (`{e}`) are not supported in SMT.')
148 else:
149 return f'[{e.start}, {e.end}]'
151 # todo: Sympy does not support quantifiers yet as of 2022, but quantifiers can be handy in SMT.
152 # For now, users can extend this class and build in their own quantifier support.
153 # See `test_quantifier_extensions()` in test_smtlib.py for an example of how this might look.
155 # def _print_ForAll(self, e: ForAll):
156 # return self._s('forall', [
157 # self._s('', [
158 # self._s(sym.name, [self._type_name(sym), Interval(start, end)])
159 # for sym, start, end in e.limits
160 # ]),
161 # e.function
162 # ])
164 def _print_BooleanTrue(self, x: BooleanTrue):
165 return 'true'
167 def _print_BooleanFalse(self, x: BooleanFalse):
168 return 'false'
170 def _print_Float(self, x: Float):
171 f = x.evalf(self._precision) if self._precision else x.evalf()
172 return str(f).rstrip('0')
174 def _print_float(self, x: float):
175 return str(x)
177 def _print_Rational(self, x: Rational):
178 return self._s_expr('/', [x.p, x.q])
180 def _print_Integer(self, x: Integer):
181 assert x.q == 1
182 return str(x.p)
184 def _print_int(self, x: int):
185 return str(x)
187 def _print_Symbol(self, x: Symbol):
188 assert self._is_legal_name(x.name)
189 return x.name
191 def _print_NumberSymbol(self, x):
192 name = self._known_constants.get(x)
193 return name if name else self._print_Float(x)
195 def _print_UndefinedFunction(self, x):
196 assert self._is_legal_name(x.name)
197 return x.name
199 def _print_Exp1(self, x):
200 return (
201 self._print_Function(exp(1, evaluate=False))
202 if exp in self._known_functions else
203 self._print_NumberSymbol(x)
204 )
206 def emptyPrinter(self, expr):
207 raise NotImplementedError(f'Cannot convert `{repr(expr)}` of type `{type(expr)}` to SMT.')
210def smtlib_code(
211 expr,
212 auto_assert=True, auto_declare=True,
213 precision=None,
214 symbol_table=None,
215 known_types=None, known_constants=None, known_functions=None,
216 prefix_expressions=None, suffix_expressions=None,
217 log_warn=None
218):
219 r"""Converts ``expr`` to a string of smtlib code.
221 Parameters
222 ==========
224 expr : Expr | List[Expr]
225 A SymPy expression or system to be converted.
226 auto_assert : bool, optional
227 If false, do not modify expr and produce only the S-Expression equivalent of expr.
228 If true, assume expr is a system and assert each boolean element.
229 auto_declare : bool, optional
230 If false, do not produce declarations for the symbols used in expr.
231 If true, prepend all necessary declarations for variables used in expr based on symbol_table.
232 precision : integer, optional
233 The ``evalf(..)`` precision for numbers such as pi.
234 symbol_table : dict, optional
235 A dictionary where keys are ``Symbol`` or ``Function`` instances and values are their Python type i.e. ``bool``, ``int``, ``float``, or ``Callable[...]``.
236 If incomplete, an attempt will be made to infer types from ``expr``.
237 known_types: dict, optional
238 A dictionary where keys are ``bool``, ``int``, ``float`` etc. and values are their corresponding SMT type names.
239 If not given, a partial listing compatible with several solvers will be used.
240 known_functions : dict, optional
241 A dictionary where keys are ``Function``, ``Relational``, ``BooleanFunction``, or ``Expr`` instances and values are their SMT string representations.
242 If not given, a partial listing optimized for dReal solver (but compatible with others) will be used.
243 known_constants: dict, optional
244 A dictionary where keys are ``NumberSymbol`` instances and values are their SMT variable names.
245 When using this feature, extra caution must be taken to avoid naming collisions between user symbols and listed constants.
246 If not given, constants will be expanded inline i.e. ``3.14159`` instead of ``MY_SMT_VARIABLE_FOR_PI``.
247 prefix_expressions: list, optional
248 A list of lists of ``str`` and/or expressions to convert into SMTLib and prefix to the output.
249 suffix_expressions: list, optional
250 A list of lists of ``str`` and/or expressions to convert into SMTLib and postfix to the output.
251 log_warn: lambda function, optional
252 A function to record all warnings during potentially risky operations.
253 Soundness is a core value in SMT solving, so it is good to log all assumptions made.
255 Examples
256 ========
257 >>> from sympy import smtlib_code, symbols, sin, Eq
258 >>> x = symbols('x')
259 >>> smtlib_code(sin(x).series(x).removeO(), log_warn=print)
260 Could not infer type of `x`. Defaulting to float.
261 Non-Boolean expression `x**5/120 - x**3/6 + x` will not be asserted. Converting to SMTLib verbatim.
262 '(declare-const x Real)\n(+ x (* (/ -1 6) (pow x 3)) (* (/ 1 120) (pow x 5)))'
264 >>> from sympy import Rational
265 >>> x, y, tau = symbols("x, y, tau")
266 >>> smtlib_code((2*tau)**Rational(7, 2), log_warn=print)
267 Could not infer type of `tau`. Defaulting to float.
268 Non-Boolean expression `8*sqrt(2)*tau**(7/2)` will not be asserted. Converting to SMTLib verbatim.
269 '(declare-const tau Real)\n(* 8 (pow 2 (/ 1 2)) (pow tau (/ 7 2)))'
271 ``Piecewise`` expressions are implemented with ``ite`` expressions by default.
272 Note that if the ``Piecewise`` lacks a default term, represented by
273 ``(expr, True)`` then an error will be thrown. This is to prevent
274 generating an expression that may not evaluate to anything.
276 >>> from sympy import Piecewise
277 >>> pw = Piecewise((x + 1, x > 0), (x, True))
278 >>> smtlib_code(Eq(pw, 3), symbol_table={x: float}, log_warn=print)
279 '(declare-const x Real)\n(assert (= (ite (> x 0) (+ 1 x) x) 3))'
281 Custom printing can be defined for certain types by passing a dictionary of
282 PythonType : "SMT Name" to the ``known_types``, ``known_constants``, and ``known_functions`` kwargs.
284 >>> from typing import Callable
285 >>> from sympy import Function, Add
286 >>> f = Function('f')
287 >>> g = Function('g')
288 >>> smt_builtin_funcs = { # functions our SMT solver will understand
289 ... f: "existing_smtlib_fcn",
290 ... Add: "sum",
291 ... }
292 >>> user_def_funcs = { # functions defined by the user must have their types specified explicitly
293 ... g: Callable[[int], float],
294 ... }
295 >>> smtlib_code(f(x) + g(x), symbol_table=user_def_funcs, known_functions=smt_builtin_funcs, log_warn=print)
296 Non-Boolean expression `f(x) + g(x)` will not be asserted. Converting to SMTLib verbatim.
297 '(declare-const x Int)\n(declare-fun g (Int) Real)\n(sum (existing_smtlib_fcn x) (g x))'
298 """
299 log_warn = log_warn or (lambda _: None)
301 if not isinstance(expr, list): expr = [expr]
302 expr = [
303 sympy.sympify(_, strict=True, evaluate=False, convert_xor=False)
304 for _ in expr
305 ]
307 if not symbol_table: symbol_table = {}
308 symbol_table = _auto_infer_smtlib_types(
309 *expr, symbol_table=symbol_table
310 )
311 # See [FALLBACK RULES]
312 # Need SMTLibPrinter to populate known_functions and known_constants first.
314 settings = {}
315 if precision: settings['precision'] = precision
316 del precision
318 if known_types: settings['known_types'] = known_types
319 del known_types
321 if known_functions: settings['known_functions'] = known_functions
322 del known_functions
324 if known_constants: settings['known_constants'] = known_constants
325 del known_constants
327 if not prefix_expressions: prefix_expressions = []
328 if not suffix_expressions: suffix_expressions = []
330 p = SMTLibPrinter(settings, symbol_table)
331 del symbol_table
333 # [FALLBACK RULES]
334 for e in expr:
335 for sym in e.atoms(Symbol, Function):
336 if (
337 sym.is_Symbol and
338 sym not in p._known_constants and
339 sym not in p.symbol_table
340 ):
341 log_warn(f"Could not infer type of `{sym}`. Defaulting to float.")
342 p.symbol_table[sym] = float
343 if (
344 sym.is_Function and
345 type(sym) not in p._known_functions and
346 type(sym) not in p.symbol_table and
347 not sym.is_Piecewise
348 ): raise TypeError(
349 f"Unknown type of undefined function `{sym}`. "
350 f"Must be mapped to ``str`` in known_functions or mapped to ``Callable[..]`` in symbol_table."
351 )
353 declarations = []
354 if auto_declare:
355 constants = {sym.name: sym for e in expr for sym in e.free_symbols
356 if sym not in p._known_constants}
357 functions = {fnc.name: fnc for e in expr for fnc in e.atoms(Function)
358 if type(fnc) not in p._known_functions and not fnc.is_Piecewise}
359 declarations = \
360 [
361 _auto_declare_smtlib(sym, p, log_warn)
362 for sym in constants.values()
363 ] + [
364 _auto_declare_smtlib(fnc, p, log_warn)
365 for fnc in functions.values()
366 ]
367 declarations = [decl for decl in declarations if decl]
369 if auto_assert:
370 expr = [_auto_assert_smtlib(e, p, log_warn) for e in expr]
372 # return SMTLibPrinter().doprint(expr)
373 return '\n'.join([
374 # ';; PREFIX EXPRESSIONS',
375 *[
376 e if isinstance(e, str) else p.doprint(e)
377 for e in prefix_expressions
378 ],
380 # ';; DECLARATIONS',
381 *sorted(e for e in declarations),
383 # ';; EXPRESSIONS',
384 *[
385 e if isinstance(e, str) else p.doprint(e)
386 for e in expr
387 ],
389 # ';; SUFFIX EXPRESSIONS',
390 *[
391 e if isinstance(e, str) else p.doprint(e)
392 for e in suffix_expressions
393 ],
394 ])
397def _auto_declare_smtlib(sym: typing.Union[Symbol, Function], p: SMTLibPrinter, log_warn: typing.Callable[[str], None]):
398 if sym.is_Symbol:
399 type_signature = p.symbol_table[sym]
400 assert isinstance(type_signature, type)
401 type_signature = p._known_types[type_signature]
402 return p._s_expr('declare-const', [sym, type_signature])
404 elif sym.is_Function:
405 type_signature = p.symbol_table[type(sym)]
406 assert callable(type_signature)
407 type_signature = [p._known_types[_] for _ in type_signature.__args__]
408 assert len(type_signature) > 0
409 params_signature = f"({' '.join(type_signature[:-1])})"
410 return_signature = type_signature[-1]
411 return p._s_expr('declare-fun', [type(sym), params_signature, return_signature])
413 else:
414 log_warn(f"Non-Symbol/Function `{sym}` will not be declared.")
415 return None
418def _auto_assert_smtlib(e: Expr, p: SMTLibPrinter, log_warn: typing.Callable[[str], None]):
419 if isinstance(e, Boolean) or (
420 e in p.symbol_table and p.symbol_table[e] == bool
421 ) or (
422 e.is_Function and
423 type(e) in p.symbol_table and
424 p.symbol_table[type(e)].__args__[-1] == bool
425 ):
426 return p._s_expr('assert', [e])
427 else:
428 log_warn(f"Non-Boolean expression `{e}` will not be asserted. Converting to SMTLib verbatim.")
429 return e
432def _auto_infer_smtlib_types(
433 *exprs: Basic,
434 symbol_table: typing.Optional[dict] = None
435) -> dict:
436 # [TYPE INFERENCE RULES]
437 # X is alone in an expr => X is bool
438 # X in BooleanFunction.args => X is bool
439 # X matches to a bool param of a symbol_table function => X is bool
440 # X matches to an int param of a symbol_table function => X is int
441 # X.is_integer => X is int
442 # X == Y, where X is T => Y is T
444 # [FALLBACK RULES]
445 # see _auto_declare_smtlib(..)
446 # X is not bool and X is not int and X is Symbol => X is float
447 # else (e.g. X is Function) => error. must be specified explicitly.
449 _symbols = dict(symbol_table) if symbol_table else {}
451 def safe_update(syms: set, inf):
452 for s in syms:
453 assert s.is_Symbol
454 if (old_type := _symbols.setdefault(s, inf)) != inf:
455 raise TypeError(f"Could not infer type of `{s}`. Apparently both `{old_type}` and `{inf}`?")
457 # EXPLICIT TYPES
458 safe_update({
459 e
460 for e in exprs
461 if e.is_Symbol
462 }, bool)
464 safe_update({
465 symbol
466 for e in exprs
467 for boolfunc in e.atoms(BooleanFunction)
468 for symbol in boolfunc.args
469 if symbol.is_Symbol
470 }, bool)
472 safe_update({
473 symbol
474 for e in exprs
475 for boolfunc in e.atoms(Function)
476 if type(boolfunc) in _symbols
477 for symbol, param in zip(boolfunc.args, _symbols[type(boolfunc)].__args__)
478 if symbol.is_Symbol and param == bool
479 }, bool)
481 safe_update({
482 symbol
483 for e in exprs
484 for intfunc in e.atoms(Function)
485 if type(intfunc) in _symbols
486 for symbol, param in zip(intfunc.args, _symbols[type(intfunc)].__args__)
487 if symbol.is_Symbol and param == int
488 }, int)
490 safe_update({
491 symbol
492 for e in exprs
493 for symbol in e.atoms(Symbol)
494 if symbol.is_integer
495 }, int)
497 safe_update({
498 symbol
499 for e in exprs
500 for symbol in e.atoms(Symbol)
501 if symbol.is_real and not symbol.is_integer
502 }, float)
504 # EQUALITY RELATION RULE
505 rels = [rel for expr in exprs for rel in expr.atoms(Equality)]
506 rels = [
507 (rel.lhs, rel.rhs) for rel in rels if rel.lhs.is_Symbol
508 ] + [
509 (rel.rhs, rel.lhs) for rel in rels if rel.rhs.is_Symbol
510 ]
511 for infer, reltd in rels:
512 inference = (
513 _symbols[infer] if infer in _symbols else
514 _symbols[reltd] if reltd in _symbols else
516 _symbols[type(reltd)].__args__[-1]
517 if reltd.is_Function and type(reltd) in _symbols else
519 bool if reltd.is_Boolean else
520 int if reltd.is_integer or reltd.is_Integer else
521 float if reltd.is_real else
522 None
523 )
524 if inference: safe_update({infer}, inference)
526 return _symbols