SMTLIB/Simplify - Help

Online Help

All Products    Maple    MapleSim


Home : Support : Online Help : SMTLIB/Simplify

SMTLIB

  

Simplify

  

simplify SMT problem

 

Calling Sequence

Parameters

Options

Description

Type inference and declaration

Compatibility

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;

¬x0.a=0.

(1)
  

Perform the same simplification over the integers.

Simplify(x>0 or And(a=0,a*c^2=0)) assuming integer;

¬x0a=0

(2)

Compatibility

• 

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

• 

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

See Also

SMTLIB