simplify SMT problem
Type inference and declaration
set, function, or boolean; expression to be simplified
(optional) options as specified below
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.
The Simplify(expr) command applies several heuristics to simplify redundant expressions in expr.
For details on the format of the input expr, see SMTLIB[ToString].
As the SMT-LIB format requires each symbol to have a declared type, Maple 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 and placing an appropriate assumption on the variable.
Remove redundant clauses from a conjunction.
Simplify(x>0 or And(a=0,a*c^2=0)) assuming real;
Perform the same simplification over the integers.
Simplify(x>0 or And(a=0,a*c^2=0)) assuming integer;
The SMTLIB[Simplify] command was introduced in Maple 2018.
For more information on Maple 2018 changes, see Updates in Maple 2018.
Download Help Document
What kind of issue would you like to report? (Optional)