Module type Satml_types.ATOM

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;
aid : int;
}
and clause = {
name : string;
mutable atoms : atom Vec.t;
mutable activity : float;
mutable removed : bool;
learnt : bool;
cpremise : premise;
form : Expr.t;
}
and reason = clause option
and premise = clause list
type hcons_env
val empty_hcons_env : unit -> hcons_env
val copy_hcons_env : hcons_env -> hcons_env
val nb_made_vars : hcons_env -> int
val pr_atom : Stdlib.Format.formatter -> atom -> unit
val pr_clause : Stdlib.Format.formatter -> clause -> unit
val get_atom : hcons_env -> Expr.t -> atom
val literal : atom -> Expr.t
val weight : atom -> float
val is_true : atom -> bool
val neg : atom -> atom
val vrai_atom : atom
val faux_atom : atom
val level : atom -> int
val index : atom -> int
val reason : atom -> reason
val reason_atoms : atom -> atom list
val dummy_var : var
val dummy_atom : atom
val dummy_clause : clause
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 make_clause : string -> atom list -> Expr.t -> int -> bool -> premise -> clause
val cmp_atom : atom -> atom -> int
val eq_atom : atom -> atom -> bool
val hash_atom : atom -> int
val tag_atom : atom -> int
val add_atom : hcons_env -> Expr.t -> var list -> atom * var list
module Set : Stdlib.Set.S with type elt = atom
module Map : Stdlib.Map.S with type key = atom