Adding support for lemmas in the command verit

1 files changed, 42 insertions, 3 deletions

diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml
index a0972d4..a0af59d 100644
--- a/src/trace/smtCertif.ml
+++ b/src/trace/smtCertif.ml
@@ -110,15 +110,17 @@ type 'hform rule =
 
   (* Possibility to introduce "holes" in proofs (that should be filled in Coq) *)
   | Hole of ('hform clause) list * 'hform list
+  | Forall_inst of 'hform clause * 'hform
+  | Qf_lemma of 'hform clause * 'hform
 
 and 'hform clause = {
-            id    : clause_id;
+    mutable id    : clause_id;
     mutable kind  : 'hform clause_kind;
     mutable pos   : int option;
     mutable used  : used;
     mutable prev  : 'hform clause option;
     mutable next  : 'hform clause option;
-            value : 'hform list option
+    mutable value : 'hform list option
               (* This field should be defined for rules which can create atoms :
                  EqTr, EqCgr, EqCgrP, Lia, Dlde, Lra *)
 }
@@ -137,8 +139,45 @@ and 'hform resolution = {
 let used_clauses r =
   match r with
   | ImmBuildProj (c, _) | ImmBuildDef c | ImmBuildDef2 c
-  | ImmFlatten (c,_)  | SplArith (c,_,_) | SplDistinctElim (c,_) -> [c]
+  | ImmFlatten (c,_)  | SplArith (c,_,_) | SplDistinctElim (c,_)
+  | Forall_inst (c, _) | Qf_lemma (c, _) -> [c]
   | Hole (cs, _) -> cs
   | True | False | BuildDef _ | BuildDef2 _ | BuildProj _
   | EqTr _ | EqCgr _ | EqCgrP _
   | LiaMicromega _ | LiaDiseq _ -> []
+
+(* for debugging *)                                       
+let to_string r =
+  match r with
+            Root -> "Root"
+          | Same c -> "Same(" ^ string_of_int (c.id) ^ ")"
+          | Res r ->
+             let id1 = string_of_int r.rc1.id in
+             let id2 = string_of_int r.rc2.id in
+             let rest_ids = List.fold_left (fun str rc -> str ^ "; " ^ string_of_int rc.id) "" r.rtail in
+             "Res [" ^ id1 ^ "; " ^ id2 ^ rest_ids ^"]"
+          | Other x -> "Other(" ^
+                         begin match x with
+                         | True -> "True"
+                         | False -> "False"
+                         | BuildDef _ -> "BuildDef"
+                         | BuildDef2 _ -> "BuildDef2"
+                         | BuildProj _ -> "BuildProj"
+                         | EqTr _ -> "EqTr"
+                         | EqCgr _ -> "EqCgr"
+                         | EqCgrP _ -> "EqCgrP"
+                         | LiaMicromega _ -> "LiaMicromega"
+                         | LiaDiseq _ -> "LiaDiseq"
+                         | Qf_lemma _ -> "Qf_lemma"
+                                         
+                         | Hole _ -> "Hole"
+
+                         | ImmFlatten _ -> "ImmFlatten"
+                         | ImmBuildDef _ -> "ImmBuildDef"
+                         | ImmBuildDef2 _ -> "ImmBuildDef2"
+                         | ImmBuildProj _ -> "ImmBuildProj"
+                         | SplArith _ -> "SplArith"
+                         | SplDistinctElim _ -> "SplDistinctElim"
+                         | Forall_inst _ -> "Forall_inst"  end ^ ")"
+
+