Module TouistSource

Process an evaluated AST given by Eval.eval to produce a CNF AST and output DIMACS

This is where the compiler errors are managed.

Evaluate an AST produced by Parse.parse_sat (or any other parse function) so it becomes a semantically correct formula.

Transform any AST (at any stage of transformation) to latex.

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

Handles errors in Parse.parse produced by the menhir in incremental parser. report is the main function.

Transform any AST (at any stage of transformation) to a string.

Transform an evaluated AST into prenex form, CNF and QDIMACS.

Requires minisat Process a CNF AST to clauses in order to solve them with Minisat.

Process an evaluated AST given by Eval.eval and produces a string in SMT-LIB2 format.

Definition of types Ast.t and AstSet.t constituting the Abstract Syntaxic Tree (AST)