Module BoolFormula

module BoolFormula: sig .. end

Represent Boolean combinations of integer literals.

Basic type definitions.

type bool_formula =

`\|`	`BVar of int`
`\|`	`BNot of bool_formula`
`\|`	`BAnd of bool_formula list`
`\|`	`BOr of bool_formula list`

This type describes formulas of relational logic with equality. We allow only simple boolean junctors, other are resolved during parsing.

Printing functions.

val var_str : int -> string

Print a variable as a string.

val str : ?names:(int, string) Hashtbl.t -> bool_formula -> string

Print a formula as a string.

val flatten_sort : bool_formula -> bool_formula

Helper function to flatten multiple or's and and's.

Boolean Formulas.

val bool_formula_of_formula : Formula.formula -> bool_formula

Convert an arbitrary formula to a Boolean combination of literals

val formula_of_bool_formula_arg : bool_formula ->
       (Formula.formula, int) Hashtbl.t * (int, Formula.formula) Hashtbl.t *
       int Pervasives.ref -> Formula.formula

Convert a Boolean combination back to a formula

val bool_formula_of_formula_arg : Formula.formula ->
       (Formula.formula, int) Hashtbl.t * (int, Formula.formula) Hashtbl.t *
       int Pervasives.ref -> bool_formula

val simplify : bool_formula -> bool_formula

Simplify a Boolean combination

val full_simplify : bool_formula -> bool_formula

Simplify a Boolean combination with all reductions; may be slower.

val sort : bool_formula -> bool_formula

Sort a Boolean combination

val auxcnf_of_bool_formula : bool_formula -> int * bool_formula

Convert a reduced Boolean combination into a CNF with auxiliary variables

val pg_auxcnf_of_bool_formula : ?setmax:int -> bool_formula -> int * bool_formula

val to_reduced_form : ?neg:bool -> bool_formula -> bool_formula

Convert a Boolean combination into reduced form (over 'not' and 'or')

val to_nnf : ?neg:bool -> bool_formula -> bool_formula

Convert a Boolean formula to NNF and additionally negate if neg is set.

val cnf_of_bool_formula : ?use_pg:bool ->
       ?setmax:int -> bool_formula -> int * int list list

Convert a Boolean formula to an equisatisfiable CNF.

val print_dimacs : int list list -> unit

Print dimacs for a cnf.

val find_model : ?logtime:float ->
       ?logprefix:string -> bool_formula -> int list option

Find a model for a Boolean formula.

val convert : ?disc_vars:int list -> bool_formula -> int list list

Convert a Boolean formula to CNF. If you only want SAT, use find_model.

val formula_to_cnf : Formula.formula -> Formula.formula

Convert an arbitrary formula to CNF via Boolean combinations.

val to_cnf : ?disc_vars:int list ->
       ?tm:float -> bool_formula -> bool_formula option

Convert a Boolean formula to CNF, fail on timeout.

val to_dnf : ?disc_vars:int list ->
       ?tm:float -> bool_formula -> bool_formula option

Convert a Boolean formula to DNF, fail on timeout.

val to_sat : ?tm:float -> bool_formula -> bool_formula option

Convert a Boolean formula to Sat-equivalent form, "BOr []" on Unsat.

Boolean Quantifier Elimination and QBF

val elim_all : int list -> bool_formula -> bool_formula

Returns a quantifier-free formula equivalent to All (vars, phi).

val elim_ex : int list -> bool_formula -> bool_formula

Returns a quantifier-free formula equivalent to Ex (vars, phi).

type qbf_raw =

`\|`	`QVar of int`
`\|`	`QNot of qbf`
`\|`	`QAnd of qbf list`
`\|`	`QOr of qbf list`
`\|`	`QEx of int list * qbf`
`\|`	`QAll of int list * qbf`

Type for quantified Boolean formulas.

type qbf = qbf_raw HashCons.hc

module QBFCons: HashCons.S  with type data = qbf_raw 
                            and type other_value = int list

val qbf_hc : qbf_raw -> qbf

Hash-cons a raw QBF formula.

val clear_qbf_consing : unit -> unit

Clear QBF consing table -- only for strict test repeatability.

val qbf_of_bf : bool_formula -> qbf

Convert a boolean formula to QBF.

val qbf_str : ?names:(int, string) Hashtbl.t -> qbf -> string

Print a QBF formula.

val nnf : ?neg:bool -> qbf -> qbf

Convert a QBF to NNF and additionally negate if neg is set.

val has_quantifiers : qbf -> bool

Check if a qbf has quantifiers inside.

val read_qdimacs : string -> qbf

Read a qdimacs description of a QBF from a string.

val elim_quant : qbf -> bool_formula

Eliminating quantifiers from QBF formulas.

val sat_of_qbf : qbf -> bool_formula

Reduce QBF to SAT by taking all possibilities for universal variables

val free_vars : qbf -> int list

Free variables in a QBF.

val max_var : qbf -> int

Maximal variable number occuring (positively or negatively) in phi.

val iter_vars : (int -> unit) -> qbf -> unit

Iterate given function on all variables of the qbf.

val flatten_qbf : ?unit_prop:bool -> qbf -> qbf

Helper function to flatten multiple or's, and's, and quantifiers.

val unique : qbf list -> qbf list

Helper function: list of unique qbfs from l, in unspecified order.

val subst : (int, qbf) Hashtbl.t -> qbf -> qbf

Substitute for variables in a QBF.

val find_model_qbf : ?maximize:bool ->
       ?logtime:float -> ?logprefix:string -> qbf -> int list option

Find a model for a QBF formula without quantifiers

val force_order : qbf -> int array

Variable ordering heuristiv called FORCE, a center-of-gravity positioning based simulation of MINCE, from the paper by Aloul, Markov and Sakallah.

val print_qdimacs : ?negate:bool -> qbf -> string

Print a QBF formula in qdimacs format.

val print_qpro : qbf -> string

Print a QBF formula in qpro format.

val print_lparse : ?universal_vars:int list -> qbf -> string

Print a 2QBF formula in lparse format. The QBF must be quantifier free, free variables that are not specified as universal are made existential.