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.

logic = string or the symbol auto

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.

When logic=auto, the default, the logic is inferred automatically from the input expression.

The ToString(expr) command translates the expression expr to the SMT-LIB 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 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.

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

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.

$\mathrm{with}\left(\mathrm{SMTLIB}\right)\:$

$\mathrm{ToString}\left(a\mathbf{xor}b\Rightarrow c\right)$

$''(declare-fun\; a\; ()\; Bool)\; (declare-fun\; b\; ()\; Bool)\; (declare-fun\; c\; ()\; Bool)\; (assert\; (=>\; (xor\; a\; b)\; c))\; (check-sat)\; (exit)''$

$\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)$

$''(set-option\; :produce-assignments\; true)\; (declare-fun\; x\; ()\; Bool)\; (declare-fun\; y\; ()\; Bool)\; (declare-fun\; z\; ()\; Bool)\; (assert\; (and\; (or\; x\; y\; z)\; (or\; x\; z\; (not\; y))\; (or\; y\; z\; (not\; x))\; (or\; y\; (not\; x)\; (not\; z))\; (or\; z\; (not\; x)\; (not\; y))\; (or\; (not\; x)\; (not\; y)\; (not\; z))))\; (check-sat)\; (get-assignment)\; (exit)''$

$\mathrm{ToString}\left(\left\{x+y=3\,2x+3y=5\right\}\,\mathrm{logic}=''QF\_LIA''\,\mathrm{getvalue}=\left[x\,y\right]\right)$

$''(set-option\; :produce-models\; true)\; (set-logic\; QF\_LIA)\; (declare-fun\; x\; ()\; Int)\; (declare-fun\; y\; ()\; Int)\; (assert\; (and\; (=\; (+\; x\; y)\; 3)\; (=\; (+\; (*\; x\; 2)\; (*\; y\; 3))\; 5)))\; (check-sat)\; (get-value\; (x\; y))\; (exit)''$

$\mathrm{ToString}\left(\left\{x+y=3\,2x+3y=5\right\}\,\mathrm{logic}=''QF\_LIA''\,\mathrm{getproof}\right)$

$''(set-option\; :produce-proofs\; true)\; (set-logic\; QF\_LIA)\; (declare-fun\; x\; ()\; Int)\; (declare-fun\; y\; ()\; Int)\; (assert\; (and\; (=\; (+\; x\; y)\; 3)\; (=\; (+\; (*\; x\; 2)\; (*\; y\; 3))\; 5)))\; (check-sat)\; (get-proof)\; (exit)''$

$\mathrm{formula}≔\mathrm{`and`}\left(\mathrm{`or`}\left(x\,y\,z\right)\,\mathrm{`or`}\left(x\,y\,\mathbf{not}z\right)\,\mathrm{`or`}\left(x\,\mathbf{not}y\,z\right)\,\mathrm{`or`}\left(x\,\mathbf{not}y\,\mathbf{not}z\right)\,\mathrm{`or`}\left(\mathbf{not}x\,y\,z\right)\,\mathrm{`or`}\left(\mathbf{not}x\,y\,\mathbf{not}z\right)\,\mathrm{`or`}\left(\mathbf{not}x\,\mathbf{not}y\,z\right)\,\mathrm{`or`}\left(\mathbf{not}x\,\mathbf{not}y\,\mathbf{not}z\right)\right)$

$\mathrm{formula}≔\left(x\mathbf{or}y\mathbf{or}z\right)\mathbf{and}\left(x\mathbf{or}y\mathbf{or}\mathbf{not}z\right)\mathbf{and}\left(x\mathbf{or}\mathbf{not}y\mathbf{or}z\right)\mathbf{and}\left(x\mathbf{or}\mathbf{not}y\mathbf{or}\mathbf{not}z\right)\mathbf{and}\left(\mathbf{not}x\mathbf{or}y\mathbf{or}z\right)\mathbf{and}\left(\mathbf{not}x\mathbf{or}y\mathbf{or}\mathbf{not}z\right)\mathbf{and}\left(\mathbf{not}\left(x\mathbf{and}y\right)\mathbf{or}z\right)\mathbf{and}\mathbf{not}\left(x\mathbf{and}y\mathbf{and}z\right)$

$\mathrm{ToString}\left(\mathrm{formula}\,\mathrm{getunsatcore}\right)\mathbf{assuming}\mathrm{boolean}$

$''(set-option\; :produce-unsat-cores\; true)\; (declare-fun\; x\; ()\; Bool)\; (declare-fun\; y\; ()\; Bool)\; (declare-fun\; z\; ()\; Bool)\; (assert\; (and\; (or\; x\; y\; z)\; (or\; x\; y\; (not\; z))\; (or\; x\; (not\; y)\; z)\; (or\; x\; (not\; y)\; (not\; z))\; (or\; (not\; x)\; y\; z)\; (or\; (not\; x)\; y\; (not\; z))\; (or\; (not\; (and\; x\; y))\; z)\; (not\; (and\; x\; y\; z))))\; (check-sat)\; (get-unsat-core)\; (exit)''$

$\mathrm{ToString}\left(a\mathbf{and}2<b\Rightarrow d<3.5\&comma;\mathrm{logic}=''QF\_LRA''\right)\mathbf{assuming}a::\mathrm{boolean},b::\mathrm{integer},c::\mathrm{numeric}$

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

For more information on Maple 2017 changes, see Updates in Maple 2017.