SMTLIB/ParseFile - Maple 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 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

 > $\mathrm{with}\left(\mathrm{SMTLIB}\right):$
 > $\mathrm{fname}≔\mathrm{FileTools}:-\mathrm{JoinPath}\left(\left["example/pythagorean.smt2"\right],\mathrm{base}=\mathrm{datadir}\right)$
 ${\mathrm{fname}}{≔}{"/maple/cbat/active/169462/data/example/pythagorean.smt2"}$ (1)
 > $\mathrm{pythagorean_triple}≔\mathrm{ParseFile}\left(\mathrm{fname}\right)$
 ${\mathrm{pythagorean_triple}}{≔}{{x}}^{{2}}{+}{{y}}^{{2}}{=}{{z}}^{{2}}{\wedge }{1}{\le }{x}{\wedge }{1}{\le }{y}{\wedge }{1}{\le }{z}$ (2)
 > $\mathrm{Satisfy}\left(\mathrm{pythagorean_triple}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{assuming}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathrm{integer}$
 $\left\{{x}{=}{4}{,}{y}{=}{3}{,}{z}{=}{5}\right\}$ (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