diff options
-rw-r--r-- | src/trace/smtCommands.ml | 27 | ||||
-rw-r--r-- | src/verit/verit.ml | 40 | ||||
-rw-r--r-- | src/verit/veritSyntax.ml | 4 | ||||
-rw-r--r-- | unit-tests/Tests_verit.v | 26 | ||||
-rw-r--r-- | unit-tests/debug_coq | 73 |
5 files changed, 122 insertions, 48 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" diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v index cfb8f16..9117864 100644 --- a/unit-tests/Tests_verit.v +++ b/unit-tests/Tests_verit.v @@ -1040,12 +1040,12 @@ Lemma taut4 : forall f, f 3 =? 5 -> f 2 =? 0 -> f 2 =? 0. Proof. intros f p1 p2. verit_bool_base p1 p2; vauto. Qed. -(* Lemma test_eq_sym a b : implb (a =? b) (b =? a). *) -(* Proof. verit. *) +Lemma test_eq_sym a b : implb (a =? b) (b =? a). +Proof. verit. Qed. -(* Lemma taut5 : *) -(* forall f, 0 =? f 2 -> f 2 =? 0. *) -(* Proof. intros f p. verit_bool_base p; vauto. Qed. *) +Lemma taut5 : + forall f, 0 =? f 2 -> f 2 =? 0. +Proof. intros f p. verit_bool_base p; vauto. Qed. Lemma fun_const_Z : forall f , (forall x, f x =? 2) -> @@ -1101,14 +1101,14 @@ Proof. intros x H. verit_bool_base H; vauto. Qed. Lemma test21 : forall x, (forall a, negb (x <=? a)) -> negb (0 <=? x). Proof. intros x H. verit_bool_base H; vauto. Qed. -(* Lemma un_menteur (a b c d : Z) dit: *) -(* dit a =? c -> *) -(* dit b =? d -> *) -(* (d =? a) || (b =? c) -> *) -(* (a =? c) || (a =? d) -> *) -(* (b =? c) || (b =? d) -> *) -(* a =? d. *) -(* Proof. intros H1 H2 H3 H4 H5. verit_bool_base H1 H2 H3 H4 H5; vauto. Qed. *) +Lemma un_menteur (a b c d : Z) dit: + dit a =? c -> + dit b =? d -> + (d =? a) || (b =? c) -> + (a =? c) || (a =? d) -> + (b =? c) || (b =? d) -> + a =? d. +Proof. intros H1 H2 H3 H4 H5. verit_bool_base H1 H2 H3 H4 H5; vauto. Qed. Lemma const_fun_is_eq_val_0 : forall f : Z -> Z, diff --git a/unit-tests/debug_coq b/unit-tests/debug_coq new file mode 100644 index 0000000..61b9fd9 --- /dev/null +++ b/unit-tests/debug_coq @@ -0,0 +1,73 @@ +(* This file is useful when the tactic goes through but not hte Qed *) +(* It is works as is for standard-coq and checker_b but can be adapted for native-coq and/or checker_eq *) +(* Paste the environment and the following code : *) + + +Definition l := TO_FILL. (* find l in the expression <checker_b l b c> *) +Definition nclauses := let (nclauses, _, _) := c in nclauses. (* different in native-coq *) +Definition confl := let (_, _, confl) := c in confl. (* different in native-coq *) +Definition t := let (_, t, _) := c in t. (* different in native-coq *) + + +Definition nl := Lit.neg l. +Definition d := PArray.make nclauses nl. +Definition s := add_roots (S.make nclauses) d None. + +Compute (checker_b l true c). +Compute (checker (PArray.make nclauses nl) None c). + +Compute (Form.check_form t_form). +Compute (Atom.check_atom t_atom). +Compute (Atom.wt t_i t_func t_atom). +Compute (euf_checker (* t_atom t_form *) C.is_false s t confl). + +(* Check where the false comes from, if its the last one it means the certificate is wring *) +(* To find what rule is causing this, use : *) + + + +Definition flatten {A : Type} (trace : _trace_ A) := + let (t0, _) := t in t0. + +(* INSTEAD in native-coq, use : *) +(* Definition flatten {A : Type} (trace : _trace_ A) := *) +(* PArray.fold_left (fun l_step arr_step => l_step ++ PArray.to_list arr_step) *) +(* nil trace. *) + +Import ListNotations. +Fixpoint firsts {A : Type} (n : nat) (l : list A) := + match n with + | O => [] + | S n => match l with + | [] => [] + | he :: ta => he :: firsts n ta end end. + +Definition step_euf := @step_checker t_i t_func t_atom t_form. +Definition l_t := flatten t. + + +Definition up_to n := List.fold_left step_euf (firsts n l_t) s. +Definition nth n := List.nth (n-1) l_t (ImmBuildProj t_func t_atom t_form 99 99 99). + +Compute (List.length l_t). + + +Compute (up_to 0). +Compute (up_to 1). +Compute (up_to 2). + +Compute (up_to 3). +Compute (up_to 4). +Compute (up_to 5). +Compute (up_to 6). +Compute (nth 6). + +Compute (up_to 7). +Compute (up_to 8). +Compute (up_to 9). +Compute (nth 9). +Compute (up_to 10). +Compute (nth 10). + +Compute (Zpos (xO (xO (xI xH)))). + |