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 TouistTypes.Ast.t) can go through different functions:

(1) TouistEval.eval for type-checking and evaluation of the expressions (bigor, bigand, variables...):
(2) TouistCnf.ast_to_cnf and then TouistSatSolve.minisat_clauses_of_cnf to transform the AST into a clause ready to use by Minisat
(2') TouistSmt.to_smt2 to transform the AST into LIB-SMT2
(2'') TouistQbf.prenex to transform the CNF AST into QDIMACS
(3) TouistSatSolve.minisat_clauses_of_cnf and TouistSatSolve.solve_clauses to solve the SAT problem

val parse_sat : ?debug:bool -> ?filename:string -> string -> TouistTypes.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:bool -> ?filename:string -> string -> TouistTypes.Ast.t

val parse_qbf : ?debug:bool -> ?filename:string -> string -> TouistTypes.Ast.t

val string_of_chan : Pervasives.in_channel -> string

val string_of_file : string -> string