verit also works when it doesn't use the conclusion (#24)

Fixes issue #20

6 files changed, 46 insertions, 33 deletions

diff --git a/examples/Example.v b/examples/Example.v
index 2141843..0dba915 100644
--- a/examples/Example.v
+++ b/examples/Example.v
@@ -191,7 +191,7 @@ Section mult3.
   Hypothesis mult3_Sn : forall n, mult3 (n+1) =? mult3 n + 3.
   Add_lemmas mult3_0 mult3_Sn.
 
-  Lemma mult3_21 : mult3 7 =? 21.
+  Lemma mult3_21 : mult3 4 =? 12.
   Proof. verit. Qed.
 
   Clear_lemmas.
diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml
index a0af59d..275f6d1 100644
--- a/src/trace/smtCertif.ml
+++ b/src/trace/smtCertif.ml
@@ -146,7 +146,7 @@ let used_clauses r =
   | EqTr _ | EqCgr _ | EqCgrP _
   | LiaMicromega _ | LiaDiseq _ -> []
 
-(* for debugging *)                                       
+(* For debugging certif processing purposes : <add_scertif> <select> <occur> <alloc> *)
 let to_string r =
   match r with
             Root -> "Root"
@@ -181,3 +181,32 @@ let to_string r =
                          | Forall_inst _ -> "Forall_inst"  end ^ ")"
 
 
+
+(* To use <print_certif>, pass, as first and second argument, <Form.to_smt> and <Atom.to_string> *)
+let print_certif form_to_smt atom_to_string c where=
+  let rec start c =
+    match c.prev with
+    | None -> c
+    | Some c -> start c in
+  let r = ref (start c) in
+  let out_channel = open_out where in
+  let fmt = Format.formatter_of_out_channel out_channel in
+  let continue = ref true in
+  while !continue do
+    let kind = to_string (!r.kind) in
+    let id = !r.id in
+    let pos = match !r.pos with
+      | None -> "None"
+      | Some p -> string_of_int p in
+    let used = !r.used in
+    Format.fprintf fmt "id:%i kind:%s pos:%s used:%i value:" id kind pos used;
+    begin match !r.value with
+    | None -> Format.fprintf fmt "None"
+    | Some l -> List.iter (fun f -> form_to_smt atom_to_string fmt f;
+                                    Format.fprintf fmt " ") l end;
+    Format.fprintf fmt "\n";
+    match !r.next with
+    | None -> continue := false
+    | Some n -> r := n 
+  done;
+  Format.fprintf fmt "@."; close_out out_channel
diff --git a/src/trace/smtCertif.mli b/src/trace/smtCertif.mli
index 942262c..010934a 100644
--- a/src/trace/smtCertif.mli
+++ b/src/trace/smtCertif.mli
@@ -44,3 +44,4 @@ and 'hform resolution = {
 }
 val used_clauses : 'a rule -> 'a clause list
 val to_string : 'a clause_kind -> string
+val print_certif : ('a -> Format.formatter -> 'b -> 'c) -> 'a -> 'b clause -> string -> unit
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index c408343..d2e039b 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -449,7 +449,9 @@ module Make (Atom:ATOM) =
 
     (** Producing Coq terms *)
 
-    let to_coq hf = mkInt (to_lit hf)
+    let to_coq hf = let i = to_lit hf in
+                    if i < 0 then failwith "This formula should'nt be in Coq"
+                    else mkInt i
 
     let args_to_coq args =
       let cargs = Array.make (Array.length args + 1) (mkInt 0) in
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 8eb1b60..16968cc 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -38,31 +38,6 @@ exception Import_trace of int
 let get_val = function
     Some a -> a
   | None -> assert false
-
-(* For debugging certif processing : <add_scertif> <select> <occur> <alloc> *)
-let print_certif c where=
-  let r = ref c in
-  let out_channel = open_out where in
-  let fmt = Format.formatter_of_out_channel out_channel in
-  let continue = ref true in
-  while !continue do
-    let kind = to_string (!r.kind) in
-    let id = !r.id in
-    let pos = match !r.pos with
-      | None -> "None"
-      | Some p -> string_of_int p in
-    let used = !r.used in
-    Format.fprintf fmt "id:%i kind:%s pos:%s used:%i value:" id kind pos used;
-    begin match !r.value with
-    | None -> Format.fprintf fmt "None"
-    | Some l -> List.iter (fun f -> Form.to_smt Atom.to_string fmt f;
-                                    Format.fprintf fmt " ") l end;
-    Format.fprintf fmt "\n";
-    match !r.next with
-    | None -> continue := false
-    | Some n -> r := n 
-  done;
-  Format.fprintf fmt "@."; close_out out_channel
                             
 let import_trace ra' rf' filename first lsmt =
   let chan = open_in filename in
@@ -91,13 +66,13 @@ let import_trace ra' rf' filename first lsmt =
        begin match first with
        | None -> ()
        | Some _ ->
-          let cf, lr = order_roots (VeritSyntax.init_index lsmt re_hash)
-                         !cfirst in
+          let init_index = VeritSyntax.init_index lsmt re_hash in
+          let cf, lr = order_roots init_index !cfirst in
           cfirst := cf;
           let to_add = VeritSyntax.qf_to_add (List.tl lr) in
           let to_add =
             (match first, !cfirst.value with
-             | Some (root, l), Some [fl] when not (Form.equal l (re_hash fl)) ->
+             | Some (root, l), Some [fl] when init_index fl = 1 && not (Form.equal l (re_hash fl)) ->
                 let cfirst_value = !cfirst.value in
                 !cfirst.value <- root.value;
                 [Other (ImmFlatten (root, fl)), cfirst_value, !cfirst]
diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v
index f39e904..ba69110 100644
--- a/unit-tests/Tests_verit.v
+++ b/unit-tests/Tests_verit.v
@@ -1045,6 +1045,12 @@ Lemma lcongr3 (P:Z -> Z -> bool) x y z:
   x =? y -> P z x -> P z y.
 Proof. intros eqxy pzx. verit_base eqxy pzx; vauto. Qed.
 
+Lemma test20 :  forall x, (forall a, a <? x) -> 0 <=? x = false.
+Proof. intros x H. verit_base H; vauto. Qed.
+
+Lemma test21 : forall x, (forall a, negb (x <=? a)) -> negb (0 <=? x).
+Proof. intros x H. verit_base H; vauto. Qed.
+
 Lemma un_menteur (a b c d : Z) dit:
   dit a =? c ->
   dit b =? d ->
@@ -1123,8 +1129,8 @@ Section mult3.
   Hypothesis mult3_Sn : forall n, mult3 (n+1) =? mult3 n + 3.
   Add_lemmas mult3_0 mult3_Sn.
 
-  Lemma mult3_21 : mult3 14 =? 42.
-  Proof. verit. Qed. (* very slow to verify with standard coq *)
+  Lemma mult3_21 : mult3 4 =? 12.
+  Proof. verit. Qed. (* slow to verify with standard coq *)
 
   Clear_lemmas.
 End mult3.