type var = {
vid : int;
pa : atom;
na : atom;
mutable weight : float;
mutable sweight : int;
mutable seen : bool;
mutable level : int;
mutable index : int;
mutable reason : reason;
mutable vpremise : premise;
}
and atom = {
var : var;
lit : Expr.t;
neg : atom;
mutable watched : clause Vec.t;
mutable is_true : bool;
mutable timp : int;
mutable is_guard : bool;
aid : int;
}
and clause = {
name : string;
mutable atoms : atom Vec.t;
mutable activity : float;
mutable removed : bool;
learnt : bool;
cpremise : premise;
form : Expr.t;
}
val pr_atom : Stdlib.Format.formatter -> atom -> unit
val pr_clause : Stdlib.Format.formatter -> clause -> unit
val weight : atom -> float
val is_true : atom -> bool
val to_float : int -> float
val to_int : float -> int
val fresh_name : unit -> string
val fresh_lname : unit -> string
val fresh_dname : unit -> string
val hash_atom : atom -> int
val tag_atom : atom -> int
module Set : Stdlib.Set.S with type elt = atom
module Map : Stdlib.Map.S with type key = atom