module Make:
Implementation of diagrams.
type
type
| |
Empty |
| |
Unit |
| |
And of var * t * t * t |
type t_raw HashCons.hc
module DiagCons: HashCons.S with type data = t_raw
and type other_value = var list
The consing module.
val get : t -> var Diagram.diag
Export to unordered generic type.
val build : var Diagram.diag -> t
Import from unordered generic type.
val clear : unit -> unit
Clears the hash table. Only use in special cases!
val cEmpty : t
Smart constructors, cAnd hashes and enforces the assertions (0) - (4).
val cUnit : t
val cAnd : var * t * t * t -> t
val diag_of_cnf : var list list -> t
Create a diagram from a CNF. Work in n log n + memory management.
val diag_str : ?vars:bool -> t -> string
Print a diagram as a formula.
val log : string -> var -> t -> var list -> unit
Log a variable, diagram and variable assignment.
val size : t -> int * int
The size of a diagram - as a dag (first) and as a tree (second).
val vars : t -> (var * int) list
All variables in a diagram, with the number of path they appear on.
val singletons : t -> var list
All singletons true in a diagram.
val mk_and : t -> t -> t
Conjunction of two diagrams. Linear.
val mk_or : t -> t -> t
Disjunction of two diagrams. Might grow fast.
val propagate_once : var list -> t -> t
Propagate variables and all other singletons. Does not remove.
val propagate : var list -> t -> t
Fixed-point of propagate_once.
val remove : var -> t -> t
Remove all occurences of the given variable, whatever they mean.
val elim_var : ?log:bool ->
?bound:int option ->
?sat:bool -> ?universal:bool -> var -> t -> t
Eliminate an existential variable (or universal, if set).
Reduces upper ones to be equivalent.
val elim_top_until : ?log:bool -> int -> t -> t
Eliminate the top variable recursively up to the given size.
val top_reduce : ?log:bool -> int -> t -> t
Reduction from top.
val top_sat : ?log:bool -> t -> bool
Sat check by reduction from top.
val elim_sat : t -> bool
Sat check by repeated top variable elimination.
val mixed_sat : ?log:bool -> t -> bool
val elim_bounded : ?universal:bool ->
?until:(var -> bool) ->
?sat:bool -> int -> t -> t
Top variable elimination until size, else branch elimination.
val elim_bounded_sat : t -> bool
Sat check based on elim_bounded.
val formula : t -> QBF.bool_formula