SMTLIBSatisfiablecheck if SMT problem is satisfiableSatisfyfind satisfying instance for SMT problem
Calling SequenceParametersOptionsDescriptionDetailsCompatibility
<Text-field style="Heading 2" layout="Heading 2" bookmark="usage">Calling Sequence</Text-field>
Satisfiable(expr,options)
Satisfy(expr,options)
<Text-field style="Heading 2" layout="Heading 2" bookmark="bkmrk0">Parameters</Text-field>expr-set, function, or boolean; expression to be checked for satisfiabilityoptions-(optional) options as specified below
<Text-field style="Heading 2" layout="Heading 2" bookmark="bkmrk1">Options</Text-field>
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.
timelimit = positive or infinity
Specify a time limit for the call to the SMT solver. A nonzero value represents a time budget in seconds. The default is infinity, meaning no limit is imposed.
<Text-field style="Heading 2" layout="Heading 2" bookmark="info">Description</Text-field>
The Satisfiable(expr) command checks whether the SMT problem given by the expression expr can be satisfied.
The Satisfy(expr) command finds a solution for the SMT problem given by the expression expr.
<Text-field style="Heading 2" layout="Heading 2" bookmark="compatibility">Compatibility</Text-field>
The SMTLIB[Satisfiable] and SMTLIB[Satisfy] commands were introduced in Maple 2018.
For more information on Maple 2018 changes, see Updates in Maple 2018.
The SMTLIB[Satisfiable] and SMTLIB[Satisfy] commands were updated in Maple 2020.
The timelimit option was introduced in Maple 2020.
For more information on Maple 2020 changes, see Updates in Maple 2020.See AlsoLogic[Satisfy]SMTLIB