Library
Module
Module type
Parameter
Class
Class type
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 -> TouistTypes.AstSet.elt -> TouistTypes.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:bool -> TouistTypes.Ast.t -> TouistTypes.AstSet.elt
cnf ast
calls TouistCnf.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 print_qdimacs :
Pervasives.out_channel ->
Pervasives.out_channel ->
TouistTypes.Ast.t ->
unit
print_qdimacs out out_table ast
takes a Prenex-CNF formula TouistTypes.Ast.t
and prints the following:
val qbfclauses_of_cnf :
TouistTypes.Ast.t ->
int quantlist list * int list list * (int, string) Hashtbl.t
qbfclauses_of_cnf
translates an AST (which is in CNF) to three structures:
val is_unquant : TouistTypes.AstSet.elt -> bool
is_unquant
checks that the given formula does not contain any quantors.
val is_prenex : TouistTypes.AstSet.elt -> bool
val regroup_quantors :
TouistTypes.Ast.t ->
string quantlist list ->
string quantlist list * TouistTypes.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"]]