Fix passing the goal strongly hashed (in ra' rf') instead of normal goal (hashed in ra rf) (#28)

Fix flatten hashing in the wrong table

veriT now has a happy ending

added a debug_coq file

3 files changed, 36 insertions, 35 deletions

diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 58793b6..43365ef 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -683,9 +683,9 @@ let get_arguments concl =
   | _ -> failwith ("Verit.tactic: can only deal with equality over bool")
 
 
-let make_proof call_solver env rt ro ra' rf' l' ls_smtc =
-  let root = SmtTrace.mkRootV [l'] in
-  call_solver env rt ro ra' rf' (root,l') ls_smtc
+let make_proof call_solver env rt ro ra' rf' l ls_smtc =
+  let root = SmtTrace.mkRootV [l] in
+  call_solver env rt ro ra' rf' (root,l) ls_smtc
 (* TODO: not generic anymore, the "lemma" part is currently specific to veriT *)
 
 (* <of_coq_lemma> reifies the coq lemma given, we can then easily print it in a
@@ -755,21 +755,22 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl
     if ((Term.eq_constr b (Lazy.force ctrue)) ||
         (Term.eq_constr b (Lazy.force cfalse))) then
       let l = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf a in
-      let l' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' a in
-      let l' =
-        if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l' else l' in
-      let max_id_confl = make_proof call_solver env rt ro ra' rf' l' lsmt in
+      let nl = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
+      let _ = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' a in
+      let lsmt = Form.flatten rf nl :: lsmt in
+      let max_id_confl = make_proof call_solver env rt ro ra' rf' nl lsmt in
       build_body rt ro ra rf (Form.to_coq l) b max_id_confl (vm_cast env) (Some find_lemma)
     else
       let l1 = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf a in
+      let _ = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' a in
       let l2 = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf b in
-      let l = Form.neg (Form.get rf (Fapp(Fiff,[|l1;l2|]))) in
-      let l1' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' a in
-      let l2' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' b in
-      let l' = Form.neg (Form.get rf' (Fapp(Fiff,[|l1';l2'|]))) in
-      let max_id_confl = make_proof call_solver env rt ro ra' rf' l' lsmt in
+      let _ = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' b in
+      let l = Form.get rf (Fapp(Fiff,[|l1;l2|])) in
+      let nl = Form.neg l in
+      let lsmt = Form.flatten rf nl :: lsmt in
+      let max_id_confl = make_proof call_solver env rt ro ra' rf' nl lsmt in
       build_body_eq rt ro ra rf (Form.to_coq l1) (Form.to_coq l2)
-        (Form.to_coq l) max_id_confl (vm_cast env) (Some find_lemma) in
+        (Form.to_coq nl) max_id_confl (vm_cast env) (Some find_lemma) in
 
       let cuts = (SmtBtype.get_cuts rt) @ cuts in
 
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 6406500..32f76f1 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -94,9 +94,9 @@ let import_trace ra' rf' filename first lsmt =
           let to_add =
             (match first, !cfirst.value with
              | 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]
+                 let cfirst_value = !cfirst.value in
+                 !cfirst.value <- root.value;
+                 [Other (ImmFlatten (root, fl)), cfirst_value, !cfirst]
              | _ -> []) @ to_add in
        match to_add with
        | [] -> ()
@@ -171,11 +171,9 @@ let export out_channel rt ro lsmt =
 
   Format.fprintf fmt "(check-sat)\n(exit)@."
 
+exception Non_empty_warnings
 
 let call_verit _ rt ro ra' rf' first lsmt =
-  let (_, l') = first in
-  let fl' = Form.flatten rf' l' in
-  let lsmt = fl'::lsmt in
   let (filename, outchan) = Filename.open_temp_file "verit_coq" ".smt2" in
   export outchan rt ro lsmt;
   close_out outchan;
@@ -189,23 +187,25 @@ let call_verit _ rt ro ra' rf' first lsmt =
   let t1 = Sys.time () in
   Format.eprintf "Verit = %.5f@." (t1-.t0);
 
-  (* TODO: improve readability: remove the three nested try *)
   let win = open_in wname in
+
+  let assert_empty_warnings () =
+    try let _ = input_line win in raise Non_empty_warnings
+    with End_of_file -> () in
+
   try
-    if exit_code <> 0 then
-      failwith ("Verit.call_verit: command " ^ command ^
-	          " exited with code " ^ string_of_int exit_code);
-
-    try let _ = input_line win in
-        Structures.error "veriT returns 'unknown'"
-    with End_of_file ->
-          try
-            let res = import_trace ra' rf' logfilename (Some first) lsmt in
-            close_in win; Sys.remove wname; res
-          with
+    assert (exit_code = 0);
+    assert_empty_warnings ();
+    let res = import_trace ra' rf' logfilename (Some first) lsmt in
+    close_in win; Sys.remove wname; res
+  with x -> close_in win; Sys.remove wname;
+            match x with
+            | Assert_failure _ ->
+                failwith ("Verit.call_verit: command " ^ command ^
+	                    " exited with code " ^ string_of_int exit_code)
+            | Non_empty_warnings -> Structures.error "veriT returns 'unknown'"
             | VeritSyntax.Sat -> Structures.error "veriT found a counter-example"
-  with x -> close_in win; Sys.remove wname; raise x
-
+            | _ -> raise x
 
 let verit_logic =
   SL.of_list [LUF; LLia]
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index c4427b7..32e03f8 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -575,7 +575,7 @@ let init_index lsmt re_hash =
   let find = Hashtbl.find form_index_init_rank in
   let rec walk rank = function
     | [] -> ()
-    | h::t -> add (Form.to_lit h) rank;
+    | h::t -> add (Form.to_lit (re_hash h)) rank;
               walk (rank+1) t in
   walk 1 lsmt;
   fun hf -> let re_hf = re_hash hf in
@@ -584,7 +584,7 @@ let init_index lsmt re_hash =
               let oc = open_out "/tmp/input_not_found.log" in
               let fmt = Format.formatter_of_out_channel oc in
               List.iter (fun h -> Format.fprintf fmt "%a\n" hform_to_smt h) lsmt;
-              Format.fprintf fmt "\n%a\n" hform_to_smt re_hf;
+              Format.fprintf fmt "\n%a\n@." hform_to_smt re_hf;
               flush oc; close_out oc;
               failwith "not found: log available"