Module Satml_types.Atom

type var = {
  1. vid : int;
  2. pa : atom;
  3. na : atom;
  4. mutable weight : float;
  5. mutable seen : bool;
  6. mutable level : int;
  7. mutable index : int;
  8. mutable hindex : int;
  9. mutable reason : reason;
  10. mutable vpremise : premise;
}
and atom = {
  1. var : var;
  2. lit : Shostak.Literal.t;
  3. neg : atom;
  4. mutable watched : clause Vec.t;
  5. mutable is_true : bool;
  6. mutable timp : int;
  7. mutable is_guard : bool;
  8. aid : int;
}
and clause = {
  1. name : string;
  2. mutable atoms : atom Vec.t;
  3. mutable activity : float;
  4. mutable removed : bool;
  5. learnt : bool;
  6. cpremise : premise;
  7. 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 -> Shostak.Literal.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 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 -> bool -> premise -> clause
val equal_var : var -> var -> bool
val compare_var : var -> var -> int
val hash_var : var -> int
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 -> Shostak.Literal.t -> var list -> atom * var list
val add_expr_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