1 files changed, 65 insertions, 0 deletions
diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml
new file mode 100644
index 0000000..ca72504
--- /dev/null
+++ b/src/trace/satAtom.ml
@@ -0,0 +1,65 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+open SmtMisc
+open CoqTerms
+
+module Atom = 
+  struct 
+
+    type t = int 
+
+    let index a = a
+
+    let equal a1 a2 = a1 == a2
+
+    let is_bool_type a = true
+
+    type reify_tbl =
+        { mutable count : int;
+	          tbl : (Term.constr, int) Hashtbl.t 
+	}
+
+    let create () = 
+      { count = 0;
+	tbl =  Hashtbl.create 17 }
+
+    let declare reify a = 
+      let res = reify.count in
+      Hashtbl.add reify.tbl a res;
+      reify.count <- res + 1;
+      res
+
+    let get reify a =
+      try Hashtbl.find reify.tbl a 
+      with Not_found -> declare reify a
+
+    let atom_tbl reify =
+      let t = Array.make (reify.count + 1) (Lazy.force ctrue) in
+      let set c i = t.(i) <- c in
+      Hashtbl.iter set reify.tbl;
+      t
+
+    let interp_tbl reify =
+      Term.mkArray (Lazy.force cbool, atom_tbl reify)
+
+  end
+
+module Form = SmtForm.Make(Atom)
+module Trace = SmtTrace.MakeOpt(Form)
+module Cnf = SmtCnf.MakeCnf(Form)
+
+      
+