Parse (p.touist.3.5.0.doc.touist.Touist.Parse)

Module Touist.ParseSource

Parse a TouIST string into an Abstract Syntaxic Tree (AST).

After this step, the AST (its type is Types.Ast.t) can go through different functions:

(1) Eval.eval for type-checking and evaluation of the expressions (bigor, bigand, variables...):

(2) Cnf.ast_to_cnf and then SatSolve.minisat_clauses_of_cnf to transform the AST into a clause ready to use by Minisat

(2') Smt.to_smt2 to transform the AST into LIB-SMT2

(2'') Qbf.prenex to transform the CNF AST into QDIMACS

Sourceval parse_sat : ?debug_syntax:bool -> ?filename:string -> string -> Types.Ast.t

parse_sat text parses text and outputs the corresponding ast.

~debug:true enable the display of the automata state number on parser errors.

~filename:"foo.touist" enables the display of a file name in errors.

Sourceval parse_smt : ?debug_syntax:bool -> ?filename:string -> string -> Types.Ast.t

Sourceval parse_qbf : ?debug_syntax:bool -> ?filename:string -> string -> Types.Ast.t

Sourceval string_of_chan : in_channel -> string

Sourceval string_of_file : string -> string