package touist

  1. Overview
  2. Docs

Module Touist.QbfSource

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
Sourceval 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.

Sourceval 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

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

A means 'forall', E means 'exists'

Sourceval 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.
Sourceval 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

Sourceval is_unquant : Types.AstSet.elt -> bool

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

Sourceval is_prenex : Types.AstSet.elt -> bool
Sourceval 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"]]