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.

$\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-build/active/297794/data/example/pythagorean.smt2''$

$\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$

$\mathrm{Satisfy}\left(\mathrm{pythagorean\_triple}\right)\mathbf{assuming}\mathrm{integer}$

$\left\{x=4\,y=3\,z=5\right\}$

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

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