Transform an evaluated AST into prenex form, CNF and QDIMACS.
The order of calls is prenex -> cnf -> print_qdimacs
From an evaluated AST, you want to
val prenex : ?debug:bool ‑> Types.AstSet.elt ‑> Types.Ast.tprenex 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.eltcnf 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.
val qbfclauses_of_cnf : Types.Ast.t ‑> int quantlist list * int list list * (int, string) Hashtbl.tqbfclauses_of_cnf translates an AST (which is in CNF) to the tuple
(quants, int_clauses, int_table):
quants is a list of quantlist which reprensents the grouped
quantifiers in the Prenex Normal Form.int_clauses a list of lists of integers which represents the
CNF formula embedded in the Prenex Normal Form.int_table is the mapping table from litteral integers to names.val print_qdimacs : ?line_begin:string ‑> ?debug_dimacs:bool ‑> (int quantlist list * int list list * (int, string) Hashtbl.t) ‑> ?out_table:Pervasives.out_channel ‑> Pervasives.out_channel ‑> unitprint_qdimacs (quants, int_clauses, int_table) out takes the
result of qbfclauses_of_cnf and prints the following:
~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').val is_unquant : Types.AstSet.elt ‑> boolis_unquant checks that the given formula does not contain any quantors.
val is_prenex : Types.AstSet.elt ‑> boolval regroup_quantors : Types.Ast.t ‑> string quantlist list ‑> string quantlist list * Types.Ast.tregroup_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"]]