From 296e3c78c2d56f0e08d654cb473f86f5b24375f4 Mon Sep 17 00:00:00 2001 From: QGarchery Date: Thu, 7 Feb 2019 19:30:58 +0100 Subject: 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 --- src/trace/smtCommands.ml | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) (limited to 'src/trace') 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 *) (* 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 -- cgit