Module QBF
module QBF: sig .. end
Quantified Boolean Formulas
type
| |
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_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 read_ppm : ?xd:int -> ?yd:int -> string -> qbf array array list
Read a PPM grayscale image into a list of 8 bit-matrices.
val read_qdimacs : string -> qbf
Read a qdimacs description of a QBF from a string.
val qbf_str : ?names:(int, string) Hashtbl.t -> qbf -> string
Print a QBF formula.
val dag_str : ?names:(int, string) Hashtbl.t -> qbf -> string
Print a QBF formula as a dag.
val size : qbf -> int * int
Size of a QBF - as a dag and as a tree.
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 free_vars : qbf -> int list
Free variables in a QBF.
val free_vars_hash : qbf -> (int, unit) Hashtbl.t -> unit
Add free variables of a QBF to the given hash table.
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 to_array : int -> qbf list -> qbf array * qbf list
Helper function - put a list into an array of length k,
pad with false, return whatever is left over.
val binary_add : ?carry:qbf -> qbf array -> qbf array -> qbf array * qbf
Binary addition. We assume lower-bit first binary representation.
We require both numbers to be arrays of the same size,
and we return the array of the same bit number plus the overflow.
val unary_add : qbf array -> qbf array -> qbf array
val binary_sub : qbf array -> qbf array -> qbf array
Binary subtraction. We assume lower-bit first binary representation
We require both numbers to be of the same size, use the 2-complement.
val binary_minus : qbf array -> qbf array
Given (binary) number n returns -n in our (2-complement) representation.
val binary_abs : qbf array -> qbf array
Given a signed binary number n returns |n|.
val unsigned_gt : qbf array -> qbf array -> qbf
QBF saying if one number (unsigned lower-endian) is greater that another.
val sum_gt0 : ?unary:bool -> ?bits:qbf list -> qbf array list -> qbf
QBF saying if the sum of signed numbers (lower-endian) is > 0.
Optionally we give a list of bits of the same length and then
only numbers for which the bits are set are counted.
val use_sum_gates : bool Pervasives.ref
Whether to use DNF or TC=sums as gates in convolution. (default: DNF)
val convolve : ?unary:bool ->
int -> qbf array list -> qbf array array list -> qbf array array
Convolve a NxNxL+1 list of (signed) weights with a list of L bit-images
of size XxY. The result is a (X-N+1)x(Y-N+1) bit-image - the convolution.
val maxpool : qbf array array -> qbf array array
Max-pool a XxY bit-image to a (X/2)x(Y/2) bit-image.
val nbits : int Pervasives.ref
How many bits to use in numbers or conjunctions in gates.
val make_layer : int ->
?unary:bool ->
?weights:qbf array list list ->
?minvar:int ->
?maxpool:bool ->
int ->
qbf array array list ->
qbf array array list * qbf array list list * int * qbf
Make a layer of a convolutional network with k maps. Optionally take a list
of weights. It does convolution and max-pooling, so on an (2X+N-1)x(2Y+N-1)
image we return a XxY comvolved-and-max-pooled image, and the weights.
If maxpool is set to false, then max-pooling is omitted and the result is
then a (2X)x(2Y) image, weights, the next free weight, and assumptions.
val subst : (int, qbf) Hashtbl.t -> qbf -> qbf
Substitute for variables in a QBF.
val no_external : int Pervasives.ref
Upto this clause number we don't use external solvers (default: 4).
val find_model_qbf : ?maximize:bool ->
?logtime:float -> ?logprefix:string -> qbf -> int list option
Find a model for a QBF formula.
val find_model_qbf_qf : ?maximize:bool ->
?logtime:float -> ?logprefix:string -> qbf -> int list option
Find a model for a quantifier free QBF formula.
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 simplify : qbf -> qbf
Recursive QBF simplification.
val convert : ?disc_vars:int list -> qbf -> int list list
Convert a QBF to CNF.
val formula_to_cnf : Formula.formula -> Formula.formula
Convert an arbitrary formula to CNF via Boolean combinations.
val simplify_formula : Formula.formula -> Formula.formula
Given a formula, simplify its Boolean structure.
val print_dimacs : int list list -> unit
Print dimacs for a cnf.
val print_qdimacs : qbf -> string
Print a QBF formula in qdimacs format.
val print_qiscas : ?prenex:bool -> qbf -> string
Print a QBF formula in qiscas format.
val print_cqbf : qbf -> string
Print a QBF formula in cqbf 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.
type
val bf_str : ?names:(int, string) Hashtbl.t -> bool_formula -> string
Print a Boolean formula as a string.
val qbf_of_bf : bool_formula -> qbf
Convert a boolean formula to QBF.
val sat_of_qbf : qbf -> bool_formula
Reduce QBF to SAT by taking all possibilities for universal variables.