package touist

  1. Overview
  2. Docs
module Cnf : sig ... end

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

module Err : sig ... end

This is where the compiler errors are managed.

module Eval : sig ... end

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

module Latex : sig ... end

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

module Lexer : sig ... end
module Parse : sig ... end

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

module Parser : sig ... end
module ParserMsgs : sig ... end
module ParserReport : sig ... end

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

module Pprint : sig ... end

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

module Qbf : sig ... end

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

module SatSolve : sig ... end

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

module Smt : sig ... end

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

module Types : sig ... end

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