package alt-ergo-lib

  1. Overview
  2. Docs
package alt-ergo-lib
Legend:
Library
Module
Module type
Parameter
Class
Class type
type var = {
  1. vid : int;
  2. pa : atom;
  3. na : atom;
  4. mutable weight : float;
  5. mutable sweight : int;
  6. mutable seen : bool;
  7. mutable level : int;
  8. mutable index : int;
  9. mutable reason : reason;
  10. mutable vpremise : premise;
}
and atom = {
  1. var : var;
  2. lit : Expr.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 : Format.formatter -> atom -> unit
val pr_clause : 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 : Set.S with type elt = atom
module Map : Map.S with type key = atom