From faaa2848c37444f8f37ac432c25f9f813e1df39b Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Sat, 27 Oct 2018 20:08:44 +0200
Subject: Adding support for lemmas in the command verit

---
 src/trace/smtAtom.mli | 45 +++++++++++++++++++++++++++++++--------------
 1 file changed, 31 insertions(+), 14 deletions(-)

(limited to 'src/trace/smtAtom.mli')

diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli
index 8e69265..47734fb 100644
--- a/src/trace/smtAtom.mli
+++ b/src/trace/smtAtom.mli
@@ -43,7 +43,10 @@ type nop =
 
 type indexed_op
 
-val dummy_indexed_op: int -> btype array -> btype -> indexed_op
+type index = Index of int
+           | Rel_name of string
+
+val dummy_indexed_op: index -> btype array -> btype -> indexed_op
 val indexed_op_index : indexed_op -> int
 
 module Op :
@@ -53,7 +56,8 @@ module Op :
 
     val create : unit -> reify_tbl
 
-    val declare : reify_tbl -> Term.constr -> btype array -> btype -> indexed_op
+    val declare : reify_tbl -> Term.constr -> btype array ->
+                  btype -> string option -> indexed_op
 
     val of_coq : reify_tbl -> Term.constr -> indexed_op
 
@@ -92,6 +96,8 @@ module Atom :
  
       val type_of : hatom -> btype
 
+      val to_string : ?pi:bool -> hatom -> string
+                               
       val to_smt : Format.formatter -> t -> unit
 
       exception NotWellTyped of atom
@@ -102,10 +108,22 @@ module Atom :
 
       val clear : reify_tbl -> unit
 
-      val get : reify_tbl -> atom -> hatom
+      val get : ?declare:bool -> reify_tbl -> atom -> hatom
+
+      val mk_eq : reify_tbl -> bool -> btype -> hatom -> hatom -> hatom
+
+      val mk_neg : reify_tbl -> hatom -> hatom
+                                                                    
+      val hash_hatom : reify_tbl -> hatom -> hatom
+
+      (** for debugging purposes **)
 
+      val copy : reify_tbl -> reify_tbl
+                                                        
+      val print_atoms : reify_tbl -> string -> unit
+                                       
       (** Given a coq term, build the corresponding atom *)
-      val of_coq : SmtBtype.reify_tbl -> Op.reify_tbl ->
+      val of_coq : ?hash:bool -> SmtBtype.reify_tbl -> Op.reify_tbl ->
         reify_tbl -> Environ.env -> Evd.evar_map -> Term.constr -> t
 
       val to_coq : hatom -> Term.constr
@@ -121,16 +139,15 @@ module Atom :
       val hatom_Z_of_int : reify_tbl -> int -> hatom
       val hatom_Z_of_bigint : reify_tbl -> Big_int.big_int -> hatom
 
-      val mk_eq : reify_tbl -> btype -> hatom -> hatom -> hatom
-      val mk_lt : reify_tbl -> hatom -> hatom -> hatom
-      val mk_le : reify_tbl -> hatom -> hatom -> hatom
-      val mk_gt : reify_tbl -> hatom -> hatom -> hatom
-      val mk_ge : reify_tbl -> hatom -> hatom -> hatom
-      val mk_plus : reify_tbl -> hatom -> hatom -> hatom
-      val mk_minus : reify_tbl -> hatom -> hatom -> hatom
-      val mk_mult : reify_tbl -> hatom -> hatom -> hatom
-      val mk_opp : reify_tbl -> hatom -> hatom
-      val mk_distinct : reify_tbl -> btype -> hatom array -> hatom
+      val mk_lt : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_le : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_gt : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_ge : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_plus : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_minus : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_mult : reify_tbl -> bool -> hatom -> hatom -> hatom
+      val mk_opp : reify_tbl -> ?declare:bool -> hatom -> hatom
+      val mk_distinct : reify_tbl -> btype -> ?declare:bool -> hatom array -> hatom
 
     end
 
-- 
cgit