 SMTLIB - Maple Programming Help

Home : Support : Online Help : Programming : Logic : SMTLIB Package : SMTLIB/ToString

SMTLIB

 ToString
 format expression as SMT-LIB string

 Calling Sequence ToString(expr,options)

Parameters

 expr - expression; expr to be encoded as SMT-LIB options - (optional) options as specified below

Options

 • logic=string

The value of option logic is a string which must correspond to one of the following logic names defined by the SMT-LIB standard: "QF_UF", "QF_LIA", "QF_NIA", "QF_LRA", "QF_NRA", "LIA", and "LRA".

 For an explanation of these logics, see Formats,SMTLIB.
 • getassignment=truefalse

Indicates whether the SMT-LIB script should include the (get-assignment) command, which instructs the SMT solver to return a list representing a satisfying assignment. Default is false.

 • getproof=truefalse

Indicates whether the SMT-LIB script should include the (get-proof) command, which instructs the SMT solver to produce a proof of unsatisfiability. Default is false.

 • getunsatcore=truefalse

Indicates whether the SMT-LIB script should include the (get-unsat-core) command, which instructs the SMT solver to produce an unsatisfiable core if the input is unsatisfiable. Default is false.

 • getvalue=list

Indicates that the SMT-LIB script should request a satisfying value for each of the names in this list.

Description

 • The ToString(expr) command translates the expression expr to the SMTLIB input format, expressed as a Maple string.
 • The input expr must be a valid SMT Boolean expression; that is:
 • one of the values true or false
 • an equation or inequation whose left- and right-hand sides are valid SMT Boolean or algebraic expressions
 • an inequality whose left- and right-hand sides are valid SMT algebraic expressions
 • a function from the list of supported functions whose arguments are SMT Boolean or algebraic expressions
 • a set or Boolean combination of SMT Boolean expressions

An SMT algebraic expression is:

 • an integer or real constant
 • a function from the list of supported functions whose arguments are SMT Boolean or algebraic expressions
 • a sum, product, or constant integer power of SMT algebraic expressions.

Supported functions and operators

 • The ToString command supports expressions which are expressible in the SMT-LIB language using the Core and Reals_Ints theories.
 • This consists of symbols and indexed names and numeric literals (integers, fractions, and floating-point numbers), and expressions formed from these using the following operators and functions:
 Supported operators

 Supported functions

Type inference and declaration

 • As the SMT-LIB format requires each symbol to have a declared type, ToString will attempt to infer types for any unassigned names occurring in expr.
 • A type for a particular variable can be forced by using the assume or assuming commands to place an appropriate assumption on the variable.

Examples

Generate an SMT-LIB query testing for satisfiability of this Boolean problem.

 > $\mathrm{with}\left(\mathrm{SMTLIB}\right):$
 > $\mathrm{ToString}\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{xor}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}b⇒c\right)$
 ${"\left(declare-fun a \left(\right) Bool\right) \left(declare-fun b \left(\right) Bool\right) \left(declare-fun c \left(\right) Bool\right) \left(assert \left(=> \left(xor a b\right) c\right)\right) \left(check-sat\right) \left(exit\right)"}$ (1)

Generate an SMT-LIB query testing for finding a satisfying assignment to a randomly generated Boolean problem.

 > $\mathrm{expr}≔\mathrm{Logic}:-\mathrm{Random}\left(\left[x,y,z\right],\mathrm{form}=\mathrm{CNF},\mathrm{clauses}=6,\mathrm{literals}=3\right):$
 > $\mathrm{ToString}\left(\mathrm{expr},\mathrm{getassignment}\right)$
 ${"\left(set-option :produce-assignments true\right) \left(declare-fun x \left(\right) Bool\right) \left(declare-fun y \left(\right) Bool\right) \left(declare-fun z \left(\right) Bool\right) \left(assert \left(and \left(or x y z\right) \left(or x z \left(not y\right)\right) \left(or y z \left(not x\right)\right) \left(or y \left(not x\right) \left(not z\right)\right) \left(or z \left(not x\right) \left(not y\right)\right) \left(or \left(not x\right) \left(not y\right) \left(not z\right)\right)\right)\right) \left(check-sat\right) \left(get-assignment\right) \left(exit\right)"}$ (2)

Generate an SMT-LIB query requesting a solution for the specified variables in this Diophantine problem over quantifier-free integer linear arithmetic.

 > $\mathrm{ToString}\left(\left\{x+y=3,2x+3y=5\right\},\mathrm{logic}="QF_LIA",\mathrm{getvalue}=\left[x,y\right]\right)$
 ${"\left(set-option :produce-models true\right) \left(set-logic QF_LIA\right) \left(declare-fun x \left(\right) Int\right) \left(declare-fun y \left(\right) Int\right) \left(assert \left(and \left(= \left(+ x y\right) 3\right) \left(= \left(+ \left(* x 2\right) \left(* y 3\right)\right) 5\right)\right)\right) \left(check-sat\right) \left(get-value \left(x y\right)\right) \left(exit\right)"}$ (3)

Generate an SMT-LIB query requesting a proof of solvability for the preceding Diophantine problem example.

 > $\mathrm{ToString}\left(\left\{x+y=3,2x+3y=5\right\},\mathrm{logic}="QF_LIA",\mathrm{getproof}\right)$
 ${"\left(set-option :produce-proofs true\right) \left(set-logic QF_LIA\right) \left(declare-fun x \left(\right) Int\right) \left(declare-fun y \left(\right) Int\right) \left(assert \left(and \left(= \left(+ x y\right) 3\right) \left(= \left(+ \left(* x 2\right) \left(* y 3\right)\right) 5\right)\right)\right) \left(check-sat\right) \left(get-proof\right) \left(exit\right)"}$ (4)

Generate an SMT-LIB query requesting an unsatisfiable core (that is, a proof of unsolvability) for the specified Boolean problem.

 > $\mathrm{formula}≔\mathrm{and}\left(\mathrm{or}\left(x,y,z\right),\mathrm{or}\left(x,y,\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}z\right),\mathrm{or}\left(x,\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}y,z\right),\mathrm{or}\left(x,\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}y,\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}z\right),\mathrm{or}\left(\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}x,y,z\right),\mathrm{or}\left(\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}x,y,\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}z\right),\mathrm{or}\left(\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}x,\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}y,z\right),\mathrm{or}\left(\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}x,\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}y,\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}z\right)\right)$
 ${\mathrm{formula}}{≔}\left({x}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{y}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{z}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({x}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{y}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{z}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({x}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{y}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{z}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({x}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{y}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{z}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{x}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{y}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{z}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{x}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{y}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{z}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({x}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{y}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{z}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({x}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{y}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{z}\right)$ (5)
 > $\mathrm{ToString}\left(\mathrm{formula},\mathrm{getunsatcore}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{assuming}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathrm{boolean}$
 ${"\left(set-option :produce-unsat-cores true\right) \left(declare-fun V1 \left(\right) Bool\right) \left(declare-fun V2 \left(\right) Bool\right) \left(declare-fun V3 \left(\right) Bool\right) \left(assert \left(and \left(or V1 V2 V3\right) \left(or V1 V2 \left(not V3\right)\right) \left(or V1 \left(not V2\right) V3\right) \left(or V1 \left(not V2\right) \left(not V3\right)\right) \left(or \left(not V1\right) V2 V3\right) \left(or \left(not V1\right) V2 \left(not V3\right)\right) \left(or \left(not \left(and V1 V2\right)\right) V3\right) \left(not \left(and V1 V2 V3\right)\right)\right)\right) \left(check-sat\right) \left(get-unsat-core\right) \left(exit\right)"}$ (6)

Generate an SMT-LIB query testing for satisfiability of this problem over quantifier-free real arithmetic, in which the types of each variable are specified explicitly (not inferred).

 > $\mathrm{ToString}\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}2
 ${"\left(set-logic QF_LRA\right) \left(declare-fun V1 \left(\right) Bool\right) \left(declare-fun V2 \left(\right) Int\right) \left(declare-fun d \left(\right) Real\right) \left(assert \left(=> \left(and V1 \left(< 2 V2\right)\right) \left(< d 3.5\right)\right)\right) \left(check-sat\right) \left(exit\right)"}$ (7)

Compatibility

 • The SMTLIB[ToString] command was introduced in Maple 2017.