package touist

  1. Overview
  2. Docs

Module TouistSource

Sourcemodule Cnf : sig ... end

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

Sourcemodule Err : sig ... end

This is where the compiler errors are managed.

Sourcemodule Eval : sig ... end

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

Sourcemodule Latex : sig ... end

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

Sourcemodule Lexer : sig ... end
Sourcemodule Parse : sig ... end

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

Sourcemodule Parser : sig ... end
Sourcemodule ParserMsgs : sig ... end
Sourcemodule ParserReport : sig ... end

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

Sourcemodule Pprint : sig ... end

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

Sourcemodule Qbf : sig ... end

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

Sourcemodule SatSolve : sig ... end

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

Sourcemodule Smt : sig ... end

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

Sourcemodule Types : sig ... end

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