SMTLIB/Satisfy - Help

Online Help

All Products    Maple    MapleSim


Home : Support : Online Help : SMTLIB/Satisfy

SMTLIB

  

Satisfiable

  

check if SMT problem is satisfiable

  

Satisfy

  

find satisfying instance for SMT problem

 

Calling Sequence

Parameters

Options

Description

Details

Compatibility

Calling Sequence

Satisfiable(expr,options)

Satisfy(expr,options)

Parameters

expr

-

set, function, or boolean; expression to be checked for satisfiability

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.

• 

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.

Description

• 

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.

Details

• 

The Satisfiable and Satisfy commands first transform the input expr to the SMTLIB input format using ToString, and pass the resulting SMT-LIB expression to an SMT solver.

• 

For details on what operators and functions are permitted in the input expression and how types are inferred and declared, see the ToString help page.

• 

As all Boolean formulas are SMT expressions, the Satisfiable and Satisfy commands may be viewed as generalizations of the functionality of Logic[Satisfiable] and Logic[Satisfy] respectively.

  

Test for the satisfiability of this simple Boolean problem.

with(SMTLIB):

e := (a or b) and (not a or not b) and (a or not b);

eaorbandnotaandbandaornotb

(1)

Satisfiable(e);

true

(2)
  

Generate a satisfying instance for the preceding problem.

Satisfy(e);

a=true,b=false

(3)
  

Find a solution for this Diophantine problem over quantifier-free integer linear arithmetic.

Satisfy( {x+y=3,2*x+3*y=5}, logic="QF_LIA" );

x=4,y=−1

(4)
  

Find a Pythagorean triple.

Satisfy( x^2+y^2=z^2 ) assuming posint;

x=5,y=12,z=13

(5)
  

Find a bigger Pythagorean triple.

Satisfy( x^2+y^2=z^2 ) assuming posint,x>1000,y>1000,z>1000;

x=1647,y=2196,z=2745

(6)
  

Show that there are no solutions to the following problem.

Satisfiable( {x^2+y^2+z^2<1, x*y*z>1} ) assuming real;

false

(7)

Compatibility

• 

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 Also

Logic[Satisfy]

SMTLIB