SMTLIB/ParseFile - Help

Online Help

All Products    Maple    MapleSim


Home : Support : Online Help : SMTLIB/ParseFile

SMTLIB

  

ParseFile

  

parse SMT-LIB file

  

ParseString

  

parse SMT-LIB script

 

Calling Sequence

Parameters

Description

Examples

Compatibility

Calling Sequence

ParseFile(fname)

ParseString(s)

Parameters

fname

-

string; path to SMT-LIB file

s

-

string; SMT-LIB script

Description

• 

The ParseFile command parses the specified file in the SMT-LIB format and returns the a conjunction of all top-level asserted expression(s) as a Maple expression.

• 

The ParseFile command behaves identically to ParseFile, but reads the SMT-LIB script from a string input instead of a file.

Examples

withSMTLIB:

fnameFileTools:-JoinPathexample/pythagorean.smt2,base=datadir

fname/maple/cbat/active/147321/data/example/pythagorean.smt2

(1)

pythagorean_tripleParseFilefname

pythagorean_triplex2+y2=z21x1y1z

(2)

Satisfypythagorean_tripleassuminginteger

x=4,y=3,z=5

(3)

Compatibility

• 

The SMTLIB[ParseFile] and SMTLIB[ParseString] commands were introduced in Maple 2018.

• 

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

See Also

SMTLIB

SMTLIB/Satisfiable

SMTLIB/Satisfy

SMTLIB/ToString