1 files changed, 112 insertions, 0 deletions
diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli
new file mode 100644
index 0000000..5d4201b
--- /dev/null
+++ b/src/trace/satAtom.mli
@@ -0,0 +1,112 @@
+module Atom :
+  sig
+    type t = int
+    val index : 'a -> 'a
+    val equal : 'a -> 'a -> bool
+    val is_bool_type : 'a -> bool
+    type reify_tbl = {
+      mutable count : int;
+      tbl : (Term.constr, int) Hashtbl.t;
+    }
+    val create : unit -> reify_tbl
+    val declare : reify_tbl -> Term.constr -> int
+    val get : reify_tbl -> Term.constr -> int
+    val atom_tbl : reify_tbl -> Term.constr array
+    val interp_tbl : reify_tbl -> Term.constr
+  end
+module Form :
+  sig
+    type hatom = Atom.t
+    type t = SmtForm.Make(Atom).t
+    type pform = (hatom, t) SmtForm.gen_pform
+    val pform_true : pform
+    val pform_false : pform
+    val equal : t -> t -> bool
+    val to_lit : t -> int
+    val index : t -> int
+    val pform : t -> pform
+    val neg : t -> t
+    val is_pos : t -> bool
+    val is_neg : t -> bool
+    val to_smt :
+      (Format.formatter -> hatom -> unit) -> Format.formatter -> t -> unit
+    exception NotWellTyped of pform
+    type reify = SmtForm.Make(Atom).reify
+    val create : unit -> reify
+    val clear : reify -> unit
+    val get : reify -> pform -> t
+    val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
+    val flatten : reify -> t -> t
+    val to_coq : t -> Term.constr
+    val pform_tbl : reify -> pform array
+    val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
+    val interp_tbl : reify -> Term.constr * Term.constr
+    val nvars : reify -> int
+    val interp_to_coq :
+      (hatom -> Term.constr) ->
+      (int, Term.constr) Hashtbl.t -> t -> Term.constr
+  end
+module Trace :
+  sig
+    val share_value : Form.t SmtCertif.clause -> unit
+    module HashedHeadRes :
+      sig
+        type t = Form.t SmtCertif.resolution
+        val equal :
+          'a SmtCertif.resolution -> 'b SmtCertif.resolution -> bool
+        val hash : 'a SmtCertif.resolution -> int
+      end
+    module HRtbl :
+      sig
+        type key = HashedHeadRes.t
+        type 'a t = 'a Hashtbl.Make(HashedHeadRes).t
+        val create : int -> 'a t
+        val clear : 'a t -> unit
+        val reset : 'a t -> unit
+        val copy : 'a t -> 'a t
+        val add : 'a t -> key -> 'a -> unit
+        val remove : 'a t -> key -> unit
+        val find : 'a t -> key -> 'a
+        val find_all : 'a t -> key -> 'a list
+        val replace : 'a t -> key -> 'a -> unit
+        val mem : 'a t -> key -> bool
+        val iter : (key -> 'a -> unit) -> 'a t -> unit
+        val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+        val length : 'a t -> int
+        val stats : 'a t -> Hashtbl.statistics
+      end
+    val common_head :
+      'a SmtCertif.clause list ->
+      'b SmtCertif.clause list ->
+      'a SmtCertif.clause list * 'a SmtCertif.clause list *
+      'b SmtCertif.clause list
+    val share_prefix : Form.t SmtCertif.clause -> int -> unit
+  end
+module Cnf :
+  sig
+    type form_info =
+      SmtCnf.MakeCnf(Form).form_info =
+        Immediate of bool
+      | Done
+      | Todo
+    val info : (int, form_info) Hashtbl.t
+    val init_last : Form.t SmtCertif.clause
+    val last : Form.t SmtCertif.clause ref
+    val cnf_todo : Form.t array list ref
+    val clear : unit -> unit
+    val push_cnf : Form.t array -> unit
+    val get_info : Form.t -> form_info
+    val set_done : Form.t -> unit
+    val set_immediate : Form.t -> unit
+    val test_immediate : Form.t -> bool
+    val check_trivial : Form.t list -> bool
+    val link_Other : Form.t SmtCertif.rule -> Form.t list -> unit
+    val both_lit : Form.t -> Form.t * Form.t
+    val or_of_imp : Form.t array -> Form.t array
+    val cnf : Form.t -> unit
+    exception Cnf_done
+    val imm_link_Other : Form.t SmtCertif.rule -> Form.t -> unit
+    val imm_cnf : Form.t SmtCertif.clause -> unit
+    val make_cnf :
+      Form.reify -> Form.t SmtCertif.clause -> Form.t SmtCertif.clause
+  end