package touist

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Legend:
Library
Module
Module type
Parameter
Class
Class type

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
(3) SatSolve.minisat_clauses_of_cnf and SatSolve.solve_clauses to solve the SAT problem

val 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.

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

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

val string_of_chan : in_channel -> string

val string_of_file : string -> string