package touist

  1. Overview
  2. Docs

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

The order of calls is prenex -> cnf -> print_qdimacs

Prenex and CNF

From an evaluated AST, you want to

  • (1) get the Prenex Normal (PNF) Form using prenex
  • (2) on the PNF, get the Prenex-CNF using cnf
val prenex : ?debug:bool -> Types.AstSet.elt -> Types.Ast.t

prenex ast takes an evaluated AST and applies the transformation rules in order to transform an evaluated AST into Prenex Normal Form (PNF).

IMPORTANT Because we do not know any to transform 'xor' and '<=>', these two connectors will be re-written using the other connectors.

val cnf : ?debug_cnf:bool -> Types.Ast.t -> Types.AstSet.elt

cnf ast calls Cnf.ast_to_cnf on the inner formula (with no quantifiers) and existentially quantifies any Tseitlin variable in an innermost way.

ast must be in Prenex Normal Form.

CNF to clauses

type 'a quantlist =
  1. | A of 'a list
  2. | E of 'a list

A means 'forall', E means 'exists'

val qbfclauses_of_cnf : Types.Ast.t -> int quantlist list * int list list * (int, string) Hashtbl.t

qbfclauses_of_cnf translates an AST (which is in CNF) to the tuple (quants, int_clauses, int_table):

  • 1) quants is a list of quantlist which reprensents the grouped quantifiers in the Prenex Normal Form.
  • 2) int_clauses a list of lists of integers which represents the CNF formula embedded in the Prenex Normal Form.
  • 3) int_table is the mapping table from litteral integers to names.
val print_qdimacs : ?debug_dimacs:bool -> (int quantlist list * int list list * (int, string) Hashtbl.t) -> ?out_table:out_channel -> out_channel -> unit

print_qdimacs (quants, int_clauses, int_table) out takes the result of qbfclauses_of_cnf and prints the following:

  • 1) If ~out_table is given, print the mapping table from litterals integers to names. If out and out_table are the same, then the mapping table will be printed in DIMACS comments (e.g., 'c p(a,b) 5').
  • 2) the DIMACS standard header line ('p cnf 3 2')
  • 3) the quantifiers lines grouped (one quantifier per line, beginning with 'e' or 'a' and ending by 0)
  • 4) the clauses (one conjunction per line, one line is a disjunction, minus means 'not').

Utility functions

val is_unquant : Types.AstSet.elt -> bool

is_unquant checks that the given formula does not contain any quantors.

val is_prenex : Types.AstSet.elt -> bool
val regroup_quantors : Types.Ast.t -> string quantlist list -> string quantlist list * Types.Ast.t

regroup_quantors gathers all succeeding Forall and Exists to a list of list such that each sublist only contains one type of quantor. Example: 

Forall ("a",Forall ("b",Exists ("c", Forall ("d",_)))

becomes 

[A of ["a";"b"]; E of ["c"]; A of ["d"]]