SMTLIB/Simplify - Help

SMTLIB

 Simplify
 simplify SMT problem

 Calling Sequence Simplify(expr,options)

Parameters

 expr - set, function, or boolean; expression to be simplified 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.

Description

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

Type inference and declaration

 • 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.
 > with(SMTLIB):
 > Simplify(x>0 or And(a=0,a*c^2=0)) assuming real;
 ${¬}\left({x}{\le }{0.}\right){\vee }{a}{=}{0.}$ (1)
 Perform the same simplification over the integers.
 > Simplify(x>0 or And(a=0,a*c^2=0)) assuming integer;
 ${¬}\left({x}{\le }{0}\right){\vee }{a}{=}{0}$ (2)

Compatibility

 • The SMTLIB[Simplify] command was introduced in Maple 2018.