 ToString - Maple Help

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

 • 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. Description

 • 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 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.5em}{0.0ex}}\mathbf{xor}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}b\mathbf{⇒}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.5em}{0.0ex}}z\right),\mathrm{or}\left(x,\mathbf{not}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}y,z\right),\mathrm{or}\left(x,\mathbf{not}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}y,\mathbf{not}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}z\right),\mathrm{or}\left(\mathbf{not}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}x,y,z\right),\mathrm{or}\left(\mathbf{not}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}x,y,\mathbf{not}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}z\right),\mathrm{or}\left(\mathbf{not}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}x,\mathbf{not}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}y,z\right),\mathrm{or}\left(\mathbf{not}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}x,\mathbf{not}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}y,\mathbf{not}\phantom{\rule[-0.0ex]{0.5em}{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.5em}{0.0ex}}assuming\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}\mathrm{boolean}$
 ${"\left(set-option :produce-unsat-cores 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 y \left(not z\right)\right) \left(or x \left(not y\right) z\right) \left(or x \left(not y\right) \left(not z\right)\right) \left(or \left(not x\right) y z\right) \left(or \left(not x\right) y \left(not z\right)\right) \left(or \left(not \left(and x y\right)\right) z\right) \left(not \left(and x y z\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.5em}{0.0ex}}\mathbf{and}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}2
 ${"\left(set-logic QF_LRA\right) \left(declare-fun a \left(\right) Bool\right) \left(declare-fun b \left(\right) Int\right) \left(declare-fun d \left(\right) Real\right) \left(assert \left(=> \left(and a \left(< 2 b\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.