diff options
| -rw-r--r-- | src/Trace.v | 138 | ||||
| -rw-r--r-- | src/trace/coqTerms.ml | 25 | ||||
| -rw-r--r-- | src/trace/smtCertif.ml | 6 | ||||
| -rw-r--r-- | src/trace/smtCommands.ml | 137 | ||||
| -rw-r--r-- | src/trace/smtTrace.ml | 26 | ||||
| -rw-r--r-- | src/zchaff/zchaff.ml | 22 | ||||
| -rw-r--r-- | unit-tests/Tests_verit.v | 60 |
7 files changed, 199 insertions, 215 deletions
diff --git a/src/Trace.v b/src/Trace.v index 9ae42c2..3b6ac47 100644 --- a/src/Trace.v +++ b/src/Trace.v @@ -308,6 +308,13 @@ End Cnf_Checker. Module Euf_Checker. + Section Checker. + + Variable t_i : array typ_eqb. + Variable t_func : array (Atom.tval t_i). + Variable t_atom : array Atom.atom. + Variable t_form : array Form.form. + Inductive step := | Res (pos:int) (res:resolution) | ImmFlatten (pos:int) (cid:clause_id) (lf:_lit) @@ -325,13 +332,18 @@ Module Euf_Checker. | LiaMicromega (pos:int) (cl:list _lit) (c:list ZMicromega.ZArithProof) | LiaDiseq (pos:int) (l:_lit) | SplArith (pos:int) (orig:clause_id) (res:_lit) (l:list ZMicromega.ZArithProof) - | SplDistinctElim (pos:int) (orig:clause_id) (res:_lit). + | SplDistinctElim (pos:int) (orig:clause_id) (res:_lit) + (* Offer the possibility to discharge parts of the proof to (manual) Coq proofs. + WARNING: this breaks extraction. *) + | Hole (pos:int) (res:_lit) + (p:Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) res) + . Local Open Scope list_scope. Local Notation check_flatten t_atom t_form := (check_flatten t_form (check_hatom t_atom) (check_neg_hatom t_atom)) (only parsing). - Definition step_checker t_atom t_form s (st:step) := + Definition step_checker s (st:step) := match st with | Res pos res => S.set_resolve s pos res | ImmFlatten pos cid lf => S.set_clause s pos (check_flatten t_atom t_form s cid lf) @@ -350,16 +362,17 @@ Module Euf_Checker. | LiaDiseq pos l => S.set_clause s pos (check_diseq t_form t_atom l) | SplArith pos orig res l => S.set_clause s pos (check_spl_arith t_form t_atom (S.get s orig) res l) | SplDistinctElim pos orig res => S.set_clause s pos (check_distinct_elim t_form t_atom (S.get s orig) res) + | @Hole pos res _ => S.set_clause s pos (res::nil) end. - Lemma step_checker_correct : forall t_i t_func t_atom t_form, + Lemma step_checker_correct : let rho := Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form in Form.check_form t_form -> Atom.check_atom t_atom -> Atom.wt t_i t_func t_atom -> forall s, S.valid rho s -> - forall st : step, S.valid rho (step_checker t_atom t_form s st). + forall st : step, S.valid rho (step_checker s st). Proof. - intros t_i t_func t_atom t_form rho H1 H2 H10 s Hs. destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [[Ht1 Ht2] Ht3]. destruct (Atom.check_atom_correct _ H2) as [Ha1 Ha2]. intros [pos res|pos cid lf|pos|pos|pos l|pos l|pos l i|pos cid|pos cid|pos cid i|pos l fl|pos l fl|pos l1 l2 fl|pos cl c|pos l|pos orig res l|pos orig res]; simpl; try apply S.valid_set_clause; auto. + intros rho H1 H2 H10 s Hs. destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [[Ht1 Ht2] Ht3]. destruct (Atom.check_atom_correct _ H2) as [Ha1 Ha2]. intros [pos res|pos cid lf|pos|pos|pos l|pos l|pos l i|pos cid|pos cid|pos cid i|pos l fl|pos l fl|pos l1 l2 fl|pos cl c|pos l|pos orig res l|pos orig res|pos res p]; simpl; try apply S.valid_set_clause; auto. apply S.valid_set_resolve; auto. apply valid_check_flatten; auto; intros h1 h2 H. rewrite (Syntactic.check_hatom_correct_bool _ _ _ Ha1 Ha2 _ _ H); auto. @@ -379,20 +392,21 @@ Module Euf_Checker. apply valid_check_diseq; auto. apply valid_check_spl_arith; auto. apply valid_check_distinct_elim; auto. + unfold C.valid; simpl; unfold rho; rewrite p; auto. Qed. - Definition euf_checker t_atom t_form s t := - _checker_ (step_checker t_atom t_form) s t. + Definition euf_checker (* t_atom t_form *) s t := + _checker_ (step_checker (* t_atom t_form *)) s t. - Lemma euf_checker_correct : forall t_i t_func t_atom t_form, + Lemma euf_checker_correct : (* forall t_i t_func t_atom t_form, *) let rho := Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form in Form.check_form t_form -> Atom.check_atom t_atom -> Atom.wt t_i t_func t_atom -> forall s t confl, - euf_checker t_atom t_form C.is_false s t confl -> + euf_checker (* t_atom t_form *) C.is_false s t confl -> ~ (S.valid rho s). Proof. - unfold euf_checker; intros t_i t_func t_atom t_form rho H1 H2 H10; apply _checker__correct. + unfold euf_checker; intros (* t_i t_func t_atom t_form *) rho H1 H2 H10; apply _checker__correct. intros c H; apply C.is_false_correct; auto. apply step_checker_correct; auto. Qed. @@ -412,63 +426,63 @@ Module Euf_Checker. let rho := Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form in afold_left _ _ true andb (Lit.interp rho) d. - Lemma add_roots_correct : forall t_i t_func t_atom t_form, + Lemma add_roots_correct : (* forall t_i t_func t_atom t_form, *) let rho := Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form in Form.check_form t_form -> Atom.check_atom t_atom -> Atom.wt t_i t_func t_atom -> forall s d used_roots, S.valid rho s -> valid t_func t_atom t_form d -> S.valid rho (add_roots s d used_roots). Proof. - intros t_i t_func t_atom t_form rho H1 H2 H10 s d used_roots H3; unfold valid; intro H4; pose (H5 := (afold_left_andb_true_inv _ _ _ H4)); unfold add_roots; assert (Valuation.wf rho) by (destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [_ H]; auto); case used_roots. + intros (* t_i t_func t_atom t_form *) rho H1 H2 H10 s d used_roots H3; unfold valid; intro H4; pose (H5 := (afold_left_andb_true_inv _ _ _ H4)); unfold add_roots; assert (Valuation.wf rho) by (destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [_ H]; auto); case used_roots. intro ur; apply (foldi_right_Ind _ _ (fun _ a => S.valid rho a)); auto; intros a i H6 Ha; apply S.valid_set_clause; auto; case_eq (ur .[ i] < length d). intro; unfold C.valid; simpl; rewrite H5; auto. intros; apply C.interp_true; auto. apply (foldi_right_Ind _ _ (fun _ a => S.valid rho a)); auto; intros a i H6 Ha; apply S.valid_set_clause; auto; unfold C.valid; simpl; rewrite H5; auto. Qed. - Definition checker t_i t_func t_atom t_form d used_roots (c:certif) := + Definition checker (* t_i t_func t_atom t_form *) d used_roots (c:certif) := let (nclauses, t, confl) := c in Form.check_form t_form && Atom.check_atom t_atom && Atom.wt t_i t_func t_atom && - euf_checker t_atom t_form C.is_false (add_roots (S.make nclauses) d used_roots) t confl. + euf_checker (* t_atom t_form *) C.is_false (add_roots (S.make nclauses) d used_roots) t confl. Implicit Arguments checker []. - Lemma checker_correct : forall t_i t_func t_atom t_form d used_roots c, - checker t_i t_func t_atom t_form d used_roots c = true -> + Lemma checker_correct : forall (* t_i t_func t_atom t_form *) d used_roots c, + checker (* t_i t_func t_atom t_form *) d used_roots c = true -> ~ valid t_func t_atom t_form d. Proof. - unfold checker; intros t_i t_func t_atom t_form d used_roots (nclauses, t, confl); rewrite !andb_true_iff; intros [[[H1 H2] H10] H3] H; eelim euf_checker_correct; try eassumption; apply add_roots_correct; try eassumption; apply S.valid_make; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [_ H4]; auto. + unfold checker; intros (* t_i t_func t_atom t_form *) d used_roots (nclauses, t, confl); rewrite !andb_true_iff; intros [[[H1 H2] H10] H3] H; eelim euf_checker_correct; try eassumption; apply add_roots_correct; try eassumption; apply S.valid_make; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [_ H4]; auto. Qed. - Definition checker_b t_i t_func t_atom t_form l (b:bool) (c:certif) := + Definition checker_b (* t_i t_func t_atom t_form *) l (b:bool) (c:certif) := let l := if b then Lit.neg l else l in let (nclauses,_,_) := c in - checker t_i t_func t_atom t_form (PArray.make nclauses l) None c. + checker (* t_i t_func t_atom t_form *) (PArray.make nclauses l) None c. - Lemma checker_b_correct : forall t_i t_func t_atom t_form l b c, - checker_b t_func t_atom t_form l b c = true -> + Lemma checker_b_correct : forall (* t_i t_func t_atom t_form *) l b c, + checker_b (* t_func t_atom t_form *) l b c = true -> Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) l = b. Proof. - unfold checker_b; intros t_i t_func t_atom t_form l b (nclauses, t, confl); case b; intros H2; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) l); auto; intros H1; elim (checker_correct H2 (t_func:=t_func)); auto; unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; auto; rewrite Lit.interp_neg, H1; auto. + unfold checker_b; intros (* t_i t_func t_atom t_form *) l b (nclauses, t, confl); case b; intros H2; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) l); auto; intros H1; elim (checker_correct H2); auto; unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; auto; rewrite Lit.interp_neg, H1; auto. Qed. - Definition checker_eq t_i t_func t_atom t_form l1 l2 l (c:certif) := + Definition checker_eq (* t_i t_func t_atom t_form *) l1 l2 l (c:certif) := negb (Lit.is_pos l) && match t_form.[Lit.blit l] with | Form.Fiff l1' l2' => (l1 == l1') && (l2 == l2') | _ => false end && let (nclauses,_,_) := c in - checker t_i t_func t_atom t_form (PArray.make nclauses l) None c. + checker (* t_i t_func t_atom t_form *) (PArray.make nclauses l) None c. - Lemma checker_eq_correct : forall t_i t_func t_atom t_form l1 l2 l c, - checker_eq t_func t_atom t_form l1 l2 l c = true -> + Lemma checker_eq_correct : forall (* t_i t_func t_atom t_form *) l1 l2 l c, + checker_eq (* t_func t_atom t_form *) l1 l2 l c = true -> Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) l1 = Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) l2. Proof. - unfold checker_eq; intros t_i t_func t_atom t_form l1 l2 l (nclauses, t, confl); rewrite !andb_true_iff; case_eq (t_form .[ Lit.blit l]); [intros _ _|intros _|intros _|intros _ _ _|intros _ _|intros _ _|intros _ _|intros _ _ _|intros l1' l2' Heq|intros _ _ _ _]; intros [[H1 H2] H3]; try discriminate; rewrite andb_true_iff in H2; rewrite !Int63Properties.eqb_spec in H2; destruct H2 as [H2 H4]; subst l1' l2'; case_eq (Lit.is_pos l); intro Heq'; rewrite Heq' in H1; try discriminate; clear H1; assert (H:PArray.default t_form = Form.Ftrue /\ Form.wf t_form). + unfold checker_eq; intros (* t_i t_func t_atom t_form *) l1 l2 l (nclauses, t, confl); rewrite !andb_true_iff; case_eq (t_form .[ Lit.blit l]); [intros _ _|intros _|intros _|intros _ _ _|intros _ _|intros _ _|intros _ _|intros _ _ _|intros l1' l2' Heq|intros _ _ _ _]; intros [[H1 H2] H3]; try discriminate; rewrite andb_true_iff in H2; rewrite !Int63Properties.eqb_spec in H2; destruct H2 as [H2 H4]; subst l1' l2'; case_eq (Lit.is_pos l); intro Heq'; rewrite Heq' in H1; try discriminate; clear H1; assert (H:PArray.default t_form = Form.Ftrue /\ Form.wf t_form). unfold checker in H3; rewrite !andb_true_iff in H3; destruct H3 as [[[H3 _] _] _]; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H3) as [[Ht1 Ht2] Ht3]; split; auto. - destruct H as [H1 H2]; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) l1); intro Heq1; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) l2); intro Heq2; auto; elim (checker_correct H3 (t_func:=t_func)); unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; unfold Lit.interp; rewrite Heq'; unfold Var.interp; rewrite Form.wf_interp_form; auto; rewrite Heq; simpl; rewrite Heq1, Heq2; auto. + destruct H as [H1 H2]; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) l1); intro Heq1; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) l2); intro Heq2; auto; elim (checker_correct H3); unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; unfold Lit.interp; rewrite Heq'; unfold Var.interp; rewrite Form.wf_interp_form; auto; rewrite Heq; simpl; rewrite Heq1, Heq2; auto. Qed. @@ -476,6 +490,7 @@ Module Euf_Checker. TODO: show that there always exists a well-typed evaluation context. *) + (* Definition checker_ext t_atom t_form d used_roots (c:certif) := let (nclauses, t, confl) := c in Form.check_form t_form && Atom.check_atom t_atom && @@ -489,73 +504,10 @@ Module Euf_Checker. Proof. unfold checker_ext; intros t_atom t_form d used_roots (nclauses, t, confl); rewrite !andb_true_iff; intros [[H1 H2] H3]; intros t_i t_func H10 H; eelim euf_checker_correct; try eassumption; apply add_roots_correct; try eassumption; apply S.valid_make; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [_ H4]; auto. Qed. - - (* For debugging *) - (* - Fixpoint is__true (c:C.t) := - match c with - | cons l q => if (l == 0) then true else is__true q - | _ => false - end. - - Definition step_checker_debug t_atom t_form s (st:step) := - match st with - | Res pos res => - let s' := S.set_resolve s pos res in - if is__true (s'.[pos]) then None else Some s' - | ImmFlatten pos cid lf => - let c := check_flatten t_atom t_form s cid lf in - if is__true c then None else Some (S.set_clause s pos c) - | CTrue pos => Some (S.set_clause s pos Cnf.check_True) - | CFalse pos => Some (S.set_clause s pos Cnf.check_False) - | BuildDef pos l => - let c := check_BuildDef t_form l in - if is__true c then None else Some (S.set_clause s pos c) - | BuildDef2 pos l => - let c := check_BuildDef2 t_form l in - if is__true c then None else Some (S.set_clause s pos c) - | BuildProj pos l i => - let c := check_BuildProj t_form l i in - if is__true c then None else Some (S.set_clause s pos c) - | ImmBuildDef pos cid => - let c := check_ImmBuildDef t_form s cid in - if is__true c then None else Some (S.set_clause s pos c) - | ImmBuildDef2 pos cid => - let c := check_ImmBuildDef2 t_form s cid in - if is__true c then None else Some (S.set_clause s pos c) - | ImmBuildProj pos cid i => - let c := check_ImmBuildProj t_form s cid i in - if is__true c then None else Some (S.set_clause s pos c) - | EqTr pos l fl => - let c := check_trans t_form t_atom l fl in - if is__true c then None else Some (S.set_clause s pos c) - | EqCgr pos l fl => - let c := check_congr t_form t_atom l fl in - if is__true c then None else Some (S.set_clause s pos c) - | EqCgrP pos l1 l2 fl => - let c := check_congr_pred t_form t_atom l1 l2 fl in - if is__true c then None else Some (S.set_clause s pos c) - | LiaMicromega pos cl c => - let c := check_micromega t_form t_atom cl c in - if is__true c then None else Some (S.set_clause s pos c) - | LiaDiseq pos l => - let c := check_diseq t_form t_atom l in - if is__true c then None else Some (S.set_clause s pos c) - | SplArith pos orig res l => - let c := check_spl_arith t_form t_atom (S.get s orig) res l in - if is__true c then None else Some (S.set_clause s pos c) - | SplDistinctElim pos input res => - let c := check_distinct_elim t_form t_atom (S.get s input) res in - if is__true c then None else Some (S.set_clause s pos c) - end. - - Definition euf_checker_debug t_atom t_form s t := - _checker_debug_ (step_checker_debug t_atom t_form) s t. - - Definition euf_checker_partial t_atom t_form s t := - _checker_partial_ (step_checker t_atom t_form) s t. *) + End Checker. + End Euf_Checker. diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index d405894..f2c24b8 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -163,16 +163,21 @@ let cFite = gen_constant smt_modules "Fite" let cis_true = gen_constant smt_modules "is_true" -let make_certif_ops modules = - (gen_constant modules "step", - gen_constant modules "Res", gen_constant modules "ImmFlatten", - gen_constant modules "CTrue", gen_constant modules "CFalse", - gen_constant modules "BuildDef", gen_constant modules "BuildDef2", - gen_constant modules "BuildProj", - gen_constant modules "ImmBuildProj", gen_constant modules"ImmBuildDef", - gen_constant modules"ImmBuildDef2", - gen_constant modules "EqTr", gen_constant modules "EqCgr", gen_constant modules "EqCgrP", - gen_constant modules "LiaMicromega", gen_constant modules "LiaDiseq", gen_constant modules "SplArith", gen_constant modules "SplDistinctElim") +let make_certif_ops modules args = + let gen_constant c = + match args with + | Some args -> lazy (SmtMisc.mklApp (gen_constant modules c) args) + | None -> gen_constant modules c in + (gen_constant "step", + gen_constant "Res", gen_constant "ImmFlatten", + gen_constant "CTrue", gen_constant "CFalse", + gen_constant "BuildDef", gen_constant "BuildDef2", + gen_constant "BuildProj", + gen_constant "ImmBuildProj", gen_constant"ImmBuildDef", + gen_constant"ImmBuildDef2", + gen_constant "EqTr", gen_constant "EqCgr", gen_constant "EqCgrP", + gen_constant "LiaMicromega", gen_constant "LiaDiseq", gen_constant "SplArith", gen_constant "SplDistinctElim", + gen_constant "Hole") (** Useful construction *) diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml index 6a56c43..8ed87e4 100644 --- a/src/trace/smtCertif.ml +++ b/src/trace/smtCertif.ml @@ -108,6 +108,9 @@ type 'hform rule = (* Elimination of operators *) | SplDistinctElim of 'hform clause * 'hform + (* Possibility to introduce "holes" in proofs (that should be filled in Coq) *) + | Hole of 'hform + and 'hform clause = { id : clause_id; mutable kind : 'hform clause_kind; @@ -137,4 +140,5 @@ let used_clauses r = | ImmFlatten (c,_) | SplArith (c,_,_) | SplDistinctElim (c,_) -> [c] | True | False | BuildDef _ | BuildDef2 _ | BuildProj _ | EqTr _ | EqCgr _ | EqCgrP _ - | LiaMicromega _ | LiaDiseq _ -> [] + | LiaMicromega _ | LiaDiseq _ + | Hole _ -> [] diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index bace2d2..de6a8fb 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -27,7 +27,7 @@ open SmtCertif let euf_checker_modules = [ ["SMTCoq";"Trace";"Euf_Checker"] ] -let certif_ops = CoqTerms.make_certif_ops euf_checker_modules +let certif_ops args = CoqTerms.make_certif_ops euf_checker_modules args let cCertif = gen_constant euf_checker_modules "Certif" let ccertif = gen_constant euf_checker_modules "certif" let cchecker = gen_constant euf_checker_modules "checker" @@ -66,11 +66,13 @@ let compute_roots roots last_root = let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf, roots, max_id, confl) = - let (tres, last_root) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) certif_ops confl in - let certif = - mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in - let ce4 = Structures.mkConst certif in - let _ = declare_constant trace (DefinitionEntry ce4, IsDefinition Definition) in + + let t_i' = make_t_i rt in + let t_func' = make_t_func ro t_i' in + let t_atom' = Atom.interp_tbl ra in + let t_form' = snd (Form.interp_tbl rf) in + + let (tres, last_root, _) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) (Form.interp_to_coq (Atom.interp_to_coq (Hashtbl.create 17)) (Hashtbl.create 17)) (certif_ops (Some [|t_i'; t_func'; t_atom'; t_form'|])) confl false in let used_roots = compute_roots roots last_root in let roots = let res = Array.make (List.length roots + 1) (mkInt 0) in @@ -87,16 +89,18 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf, let _ = declare_constant root (DefinitionEntry ce3, IsDefinition Definition) in let ce3' = Structures.mkConst used_roots in let _ = declare_constant used_root (DefinitionEntry ce3', IsDefinition Definition) in - let t_i' = make_t_i rt in - let t_func' = make_t_func ro t_i' in let ce5 = Structures.mkConst t_i' in let _ = declare_constant t_i (DefinitionEntry ce5, IsDefinition Definition) in let ce6 = Structures.mkConst t_func' in let _ = declare_constant t_func (DefinitionEntry ce6, IsDefinition Definition) in - let ce1 = Structures.mkConst (Atom.interp_tbl ra) in + let ce1 = Structures.mkConst t_atom' in let _ = declare_constant t_atom (DefinitionEntry ce1, IsDefinition Definition) in - let ce2 = Structures.mkConst (snd (Form.interp_tbl rf)) in + let ce2 = Structures.mkConst t_form' in let _ = declare_constant t_form (DefinitionEntry ce2, IsDefinition Definition) in + let certif = + mklApp cCertif [|t_i'; t_func'; t_atom'; t_form'; mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in + let ce4 = Structures.mkConst certif in + let _ = declare_constant trace (DefinitionEntry ce4, IsDefinition Definition) in () @@ -109,9 +113,12 @@ let interp_roots roots = | f::roots -> List.fold_left (fun acc f -> mklApp candb [|acc; interp f|]) (interp f) roots let build_certif (rt, ro, ra, rf, roots, max_id, confl) = - let (tres,last_root) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) certif_ops confl in - let certif = - mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in + let t_atom = Atom.interp_tbl ra in + let t_form = snd (Form.interp_tbl rf) in + let t_i = make_t_i rt in + let t_func = make_t_func ro t_i in + + let (tres,last_root,_) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) (Form.interp_to_coq (Atom.interp_to_coq (Hashtbl.create 17)) (Hashtbl.create 17)) (certif_ops (Some [|t_i; t_func; t_atom; t_form|])) confl false in let used_roots = compute_roots roots last_root in let used_rootsCstr = let l = List.length used_roots in @@ -125,10 +132,8 @@ let build_certif (rt, ro, ra, rf, roots, max_id, confl) = List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots; Structures.mkArray (Lazy.force cint, res) in - let t_atom = Atom.interp_tbl ra in - let t_form = snd (Form.interp_tbl rf) in - let t_i = make_t_i rt in - let t_func = make_t_func ro t_i in + let certif = + mklApp cCertif [|t_i; t_func; t_atom; t_form; mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in (rootsCstr, used_rootsCstr, certif, t_atom, t_form, t_i, t_func) @@ -141,7 +146,7 @@ let theorem name ((rt, ro, ra, rf, roots, max_id, confl) as p) = Term.mkLetIn (mkName "t_atom", t_atom, mklApp carray [|Lazy.force catom|], (*6*) Term.mkLetIn (mkName "t_form", t_form, mklApp carray [|Lazy.force cform|], (*5*) Term.mkLetIn (mkName "d", rootsCstr, mklApp carray [|Lazy.force cint|], (*4*) - Term.mkLetIn (mkName "c", certif, Lazy.force ccertif, (*3*) + Term.mkLetIn (mkName "c", certif, mklApp ccertif [|t_i; t_func; t_atom; t_form|], (*3*) Term.mkLetIn (mkName "t_i", t_i, mklApp carray [|Lazy.force ctyp_eqb|], (*2*) Term.mkLetIn (mkName "t_func", t_func, mklApp carray [|mklApp ctval [|t_i|]|], (*1*) mklApp cchecker_correct @@ -169,67 +174,65 @@ let checker ((rt, ro, ra, rf, roots, max_id, confl) as p) = (* Tactic *) let build_body rt ro ra rf l b (max_id, confl) = - let (tres,_) = SmtTrace.to_coq Form.to_coq certif_ops confl in - let certif = - mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in - - let t_atom = Atom.interp_tbl ra in - let t_form = snd (Form.interp_tbl rf) in - let t_i = make_t_i rt in - let t_func = make_t_func ro t_i in - + let nti = mkName "t_i" in + let ntfunc = mkName "t_func" in let ntatom = mkName "t_atom" in let ntform = mkName "t_form" in let nc = mkName "c" in - let nti = mkName "t_i" in - let ntfunc = mkName "t_func" in - let vtatom = Term.mkRel 5 in - let vtform = Term.mkRel 4 in - let vc = Term.mkRel 3 in - let vti = Term.mkRel 2 in - let vtfunc = Term.mkRel 1 in + let v = Term.mkRel in - Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Term.mkLetIn (nc, certif, Lazy.force ccertif, - Term.mkLetIn (nti, Structures.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|], - Term.mkLetIn (ntfunc, Structures.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|], - mklApp cchecker_b_correct - [|vti;vtfunc;vtatom; vtform; l; b; vc; - vm_cast_true (mklApp cchecker_b [|vti;vtfunc;vtatom;vtform;l;b;vc|])|]))))) + let t_i = make_t_i rt in + let t_func = Term.lift 1 (make_t_func ro (v 0 (*t_i - 1*))) in + let t_atom = Atom.interp_tbl ra in + let t_form = snd (Form.interp_tbl rf) in + let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq (Form.interp_to_coq (Atom.interp_to_coq (Hashtbl.create 17)) (Hashtbl.create 17)) (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl true in + let certif = + mklApp cCertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*); mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in + let proof = + Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|], + Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1 (*t_i*)|]|], + Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], + mklApp cchecker_b_correct + [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l; b; v 1 (*certif*); + vm_cast_true (mklApp cchecker_b [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l; b; v 1 (*certif*)|])|]))))) + in -let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) = - let (tres,_) = SmtTrace.to_coq Form.to_coq certif_ops confl in - let certif = - mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in + (proof, cuts) - let t_atom = Atom.interp_tbl ra in - let t_form = snd (Form.interp_tbl rf) in - let t_i = make_t_i rt in - let t_func = make_t_func ro t_i in +let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) = + let nti = mkName "t_i" in + let ntfunc = mkName "t_func" in let ntatom = mkName "t_atom" in let ntform = mkName "t_form" in let nc = mkName "c" in - let nti = mkName "t_i" in - let ntfunc = mkName "t_func" in - let vtatom = Term.mkRel 5 in - let vtform = Term.mkRel 4 in - let vc = Term.mkRel 3 in - let vti = Term.mkRel 2 in - let vtfunc = Term.mkRel 1 in + let v = Term.mkRel in + + let t_i = make_t_i rt in + let t_func = Term.lift 1 (make_t_func ro (v 0 (*t_i*))) in + let t_atom = Atom.interp_tbl ra in + let t_form = snd (Form.interp_tbl rf) in + let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq (Form.interp_to_coq (Atom.interp_to_coq (Hashtbl.create 17)) (Hashtbl.create 17)) (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl true in + let certif = + mklApp cCertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*); mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in + + let proof = + Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|], + Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1 (*t_i*)|]|], + Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], + mklApp cchecker_eq_correct + [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l1; l2; l; v 1 (*certif*); + vm_cast_true (mklApp cchecker_eq [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l1; l2; l; v 1 (*certif*)|])|]))))) + in - Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Term.mkLetIn (nc, certif, Lazy.force ccertif, - Term.mkLetIn (nti, Structures.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|], - Term.mkLetIn (ntfunc, Structures.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|], - mklApp cchecker_eq_correct - [|vti;vtfunc;vtatom; vtform; l1; l2; l; vc; - vm_cast_true (mklApp cchecker_eq [|vti;vtfunc;vtatom;vtform;l1;l2;l;vc|])|]))))) + (proof, cuts) let get_arguments concl = @@ -250,7 +253,7 @@ let tactic call_solver rt ro ra rf env sigma t = let (forall_let, concl) = Term.decompose_prod_assum t in let env = Environ.push_rel_context forall_let env in let a, b = get_arguments concl in - let body = + let (body, cuts) = 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 env sigma) rf a in let l' = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in @@ -265,7 +268,7 @@ let tactic call_solver rt ro ra rf env sigma t = let compose_lam_assum forall_let body = List.fold_left (fun t rd -> Term.mkLambda_or_LetIn rd t) body forall_let in let res = compose_lam_assum forall_let body in - let cuts = Btype.get_cuts rt in + let cuts = (Btype.get_cuts rt)@cuts in List.fold_right (fun (eqn, eqt) tac -> Structures.tclTHENLAST (Structures.assert_before (Names.Name eqn) eqt) tac ) cuts (Structures.vm_cast_no_check res) diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml index e2a9b1d..83b8779 100644 --- a/src/trace/smtTrace.ml +++ b/src/trace/smtTrace.ml @@ -274,12 +274,18 @@ let build_certif first_root confl = alloc first_root -let to_coq to_lit (cstep, +(* [isCut]: true if we handle holes by adding cuts inside a tactic, + false otherwise (then, by adding a section variable) *) +let to_coq to_lit interp (cstep, cRes, cImmFlatten, cTrue, cFalse, cBuildDef, cBuildDef2, cBuildProj, cImmBuildProj,cImmBuildDef,cImmBuildDef2, cEqTr, cEqCgr, cEqCgrP, - cLiaMicromega, cLiaDiseq, cSplArith, cSplDistinctElim) confl = + cLiaMicromega, cLiaDiseq, cSplArith, cSplDistinctElim, + cHole) confl isCut = + + let cuts = ref [] in + let out_f f = to_lit f in let out_c c = mkInt (get_pos c) in let step_to_coq c = @@ -328,6 +334,20 @@ let to_coq to_lit (cstep, let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Coq_micromega.M.coq_proofTerm; Coq_micromega.dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Coq_micromega.M.coq_proofTerm|]) in mklApp cSplArith [|out_c c; out_c orig; res'; l'|] | SplDistinctElim (c',f) -> mklApp cSplDistinctElim [|out_c c;out_c c'; out_f f|] + | Hole res -> + let ass_name = Names.id_of_string ("ass"^(string_of_int ( + if isCut then List.length !cuts else Hashtbl.hash res + ))) in + let ass_ty = interp res in + let ass_var = + if isCut then ( + let ass_var = Term.mkVar ass_name in + cuts := (ass_name, ass_ty)::!cuts; + ass_var + ) else ( + declare_new_variable ass_name ass_ty + ) in + mklApp cHole [|out_c c; out_f res; ass_var|] end | _ -> assert false in let step = Lazy.force cstep in @@ -361,7 +381,7 @@ let to_coq to_lit (cstep, trace.(q) <- Structures.mkArray (step, traceq) end; - (Structures.mkArray (mklApp carray [|step|], trace), last_root) + (Structures.mkArray (mklApp carray [|step|], trace), last_root, !cuts) diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml index ab260ba..20b5463 100644 --- a/src/zchaff/zchaff.ml +++ b/src/zchaff/zchaff.ml @@ -193,7 +193,7 @@ let interp_roots first last = let sat_checker_modules = [ ["SMTCoq";"Trace";"Sat_Checker"] ] -let certif_ops = CoqTerms.make_certif_ops sat_checker_modules +let certif_ops = CoqTerms.make_certif_ops sat_checker_modules None let cCertif = gen_constant sat_checker_modules "Certif" let parse_certif dimacs trace fdimacs ftrace = @@ -204,7 +204,7 @@ let parse_certif dimacs trace fdimacs ftrace = let _ = declare_constant dimacs (DefinitionEntry ce1, IsDefinition Definition) in let max_id, confl = import_cnf_trace reloc ftrace first last in - let (tres,_) = SmtTrace.to_coq (fun _ -> assert false) certif_ops confl in + let (tres,_,_) = SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl false in let certif = mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in let ce2 = Structures.mkConst certif in @@ -222,8 +222,8 @@ let theorem name fdimacs ftrace = let d = make_roots first last in let max_id, confl = import_cnf_trace reloc ftrace first last in - let (tres,_) = - SmtTrace.to_coq (fun _ -> assert false) certif_ops confl in + let (tres,_,_) = + SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl false in let certif = mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in @@ -251,8 +251,8 @@ let checker fdimacs ftrace = let d = make_roots first last in let max_id, confl = import_cnf_trace reloc ftrace first last in - let (tres,_) = - SmtTrace.to_coq (fun _ -> assert false) certif_ops confl in + let (tres,_,_) = + SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl false in let certif = mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in @@ -334,7 +334,7 @@ let call_zchaff nvars root = let cnf_checker_modules = [ ["SMTCoq";"Trace";"Cnf_Checker"] ] -let certif_ops = CoqTerms.make_certif_ops cnf_checker_modules +let certif_ops = CoqTerms.make_certif_ops cnf_checker_modules None let ccertif = gen_constant cnf_checker_modules "certif" let cCertif = gen_constant cnf_checker_modules "Certif" let cchecker_b_correct = @@ -350,8 +350,8 @@ let build_body reify_atom reify_form l b (max_id, confl) = let nc = mkName "c" in let tvar = Atom.interp_tbl reify_atom in let _, tform = Form.interp_tbl reify_form in - let (tres,_) = - SmtTrace.to_coq Form.to_coq certif_ops confl in + let (tres,_,_) = + SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl false in let certif = mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in let vtvar = Term.mkRel 3 in @@ -371,8 +371,8 @@ let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) = let nc = mkName "c" in let tvar = Atom.interp_tbl reify_atom in let _, tform = Form.interp_tbl reify_form in - let (tres,_) = - SmtTrace.to_coq Form.to_coq certif_ops confl in + let (tres,_,_) = + SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl false in let certif = mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in let vtvar = Term.mkRel 3 in diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v index e63bbaf..b5edddd 100644 --- a/unit-tests/Tests_verit.v +++ b/unit-tests/Tests_verit.v @@ -135,153 +135,153 @@ End Checker_Let2. Section Sat0. Parse_certif_verit t_i0 t_func0 t_atom0 t_form0 root0 used_roots0 trace0 "sat0.smt2" "sat0.vtlog". - Compute Euf_Checker.checker t_i0 t_func0 t_atom0 t_form0 root0 used_roots0 trace0. + Compute @Euf_Checker.checker t_i0 t_func0 t_atom0 t_form0 root0 used_roots0 trace0. End Sat0. Section Sat1. Parse_certif_verit t_i1 t_func1 t_atom1 t_form1 root1 used_roots1 trace1 "sat1.smt2" "sat1.vtlog". - Compute Euf_Checker.checker t_i1 t_func1 t_atom1 t_form1 root1 used_roots1 trace1. + Compute @Euf_Checker.checker t_i1 t_func1 t_atom1 t_form1 root1 used_roots1 trace1. End Sat1. Section Sat2. Parse_certif_verit t_i2 t_func2 t_atom2 t_form2 root2 used_roots2 trace2 "sat2.smt2" "sat2.vtlog". - Compute Euf_Checker.checker t_i2 t_func2 t_atom2 t_form2 root2 used_roots2 trace2. + Compute @Euf_Checker.checker t_i2 t_func2 t_atom2 t_form2 root2 used_roots2 trace2. End Sat2. Section Sat3. Parse_certif_verit t_i3 t_func3 t_atom3 t_form3 root3 used_roots3 trace3 "sat3.smt2" "sat3.vtlog". - Compute Euf_Checker.checker t_i3 t_func3 t_atom3 t_form3 root3 used_roots3 trace3. + Compute @Euf_Checker.checker t_i3 t_func3 t_atom3 t_form3 root3 used_roots3 trace3. End Sat3. Section Sat4. Parse_certif_verit t_i4 t_func4 t_atom4 t_form4 root4 used_roots4 trace4 "sat4.smt2" "sat4.vtlog". - Compute Euf_Checker.checker t_i4 t_func4 t_atom4 t_form4 root4 used_roots4 trace4. + Compute @Euf_Checker.checker t_i4 t_func4 t_atom4 t_form4 root4 used_roots4 trace4. End Sat4. Section Sat5. Parse_certif_verit t_i5 t_func5 t_atom5 t_form5 root5 used_roots5 trace5 "sat5.smt2" "sat5.vtlog". - Compute Euf_Checker.checker t_i5 t_func5 t_atom5 t_form5 root5 used_roots5 trace5. + Compute @Euf_Checker.checker t_i5 t_func5 t_atom5 t_form5 root5 used_roots5 trace5. End Sat5. Section Sat6. Parse_certif_verit t_i6 t_func6 t_atom6 t_form6 root6 used_roots6 trace6 "sat6.smt2" "sat6.vtlog". - Compute Euf_Checker.checker t_i6 t_func6 t_atom6 t_form6 root6 used_roots6 trace6. + Compute @Euf_Checker.checker t_i6 t_func6 t_atom6 t_form6 root6 used_roots6 trace6. End Sat6. Section Sat7. Parse_certif_verit t_i7 t_func7 t_atom7 t_form7 root7 used_roots7 trace7 "sat7.smt2" "sat7.vtlog". - Compute Euf_Checker.checker t_i7 t_func7 t_atom7 t_form7 root7 used_roots7 trace7. + Compute @Euf_Checker.checker t_i7 t_func7 t_atom7 t_form7 root7 used_roots7 trace7. End Sat7. Section Sat8. Parse_certif_verit t_i8 t_func8 t_atom8 t_form8 root8 used_roots8 trace8 "sat8.smt2" "sat8.vtlog". - Compute Euf_Checker.checker t_i8 t_func8 t_atom8 t_form8 root8 used_roots8 trace8. + Compute @Euf_Checker.checker t_i8 t_func8 t_atom8 t_form8 root8 used_roots8 trace8. End Sat8. Section Sat9. Parse_certif_verit t_i9 t_func9 t_atom9 t_form9 root9 used_roots9 trace9 "sat9.smt2" "sat9.vtlog". - Compute Euf_Checker.checker t_i9 t_func9 t_atom9 t_form9 root9 used_roots9 trace9. + Compute @Euf_Checker.checker t_i9 t_func9 t_atom9 t_form9 root9 used_roots9 trace9. End Sat9. (* Section Sat10. Parse_certif_verit t_i10 t_func10 t_atom10 t_form10 root10 used_roots10 trace10 "sat10.smt2" "sat10.vtlog". - Compute Euf_Checker.checker t_i10 t_func10 t_atom10 t_form10 root10 used_roots10 trace10. + Compute @Euf_Checker.checker t_i10 t_func10 t_atom10 t_form10 root10 used_roots10 trace10. End Sat10. *) Section Sat11. Parse_certif_verit t_i11 t_func11 t_atom11 t_form11 root11 used_roots11 trace11 "sat11.smt2" "sat11.vtlog". - Compute Euf_Checker.checker t_i11 t_func11 t_atom11 t_form11 root11 used_roots11 trace11. + Compute @Euf_Checker.checker t_i11 t_func11 t_atom11 t_form11 root11 used_roots11 trace11. End Sat11. Section Sat12. Parse_certif_verit t_i12 t_func12 t_atom12 t_form12 root12 used_roots12 trace12 "sat12.smt2" "sat12.vtlog". - Compute Euf_Checker.checker t_i12 t_func12 t_atom12 t_form12 root12 used_roots12 trace12. + Compute @Euf_Checker.checker t_i12 t_func12 t_atom12 t_form12 root12 used_roots12 trace12. End Sat12. Section Hole4. Parse_certif_verit t_i_hole4 t_func_hole4 t_atom_hole4 t_form_hole4 root_hole4 used_roots_hole4 trace_hole4 "hole4.smt2" "hole4.vtlog". - Compute Euf_Checker.checker t_i_hole4 t_func_hole4 t_atom_hole4 t_form_hole4 root_hole4 used_roots_hole4 trace_hole4. + Compute @Euf_Checker.checker t_i_hole4 t_func_hole4 t_atom_hole4 t_form_hole4 root_hole4 used_roots_hole4 trace_hole4. End Hole4. Section Uf1. Parse_certif_verit t_i_uf1 t_func_uf1 t_atom_uf1 t_form_uf1 root_uf1 used_roots_uf1 trace_uf1 "uf1.smt2" "uf1.vtlog". - Compute Euf_Checker.checker t_i_uf1 t_func_uf1 t_atom_uf1 t_form_uf1 root_uf1 used_roots_uf1 trace_uf1. + Compute @Euf_Checker.checker t_i_uf1 t_func_uf1 t_atom_uf1 t_form_uf1 root_uf1 used_roots_uf1 trace_uf1. End Uf1. Section Uf2. Parse_certif_verit t_i_uf2 t_func_uf2 t_atom_uf2 t_form_uf2 root_uf2 used_roots_uf2 trace_uf2 "uf2.smt2" "uf2.vtlog". - Compute Euf_Checker.checker t_i_uf2 t_func_uf2 t_atom_uf2 t_form_uf2 root_uf2 used_roots_uf2 trace_uf2. + Compute @Euf_Checker.checker t_i_uf2 t_func_uf2 t_atom_uf2 t_form_uf2 root_uf2 used_roots_uf2 trace_uf2. End Uf2. Section Uf3. Parse_certif_verit t_i_uf3 t_func_uf3 t_atom_uf3 t_form_uf3 root_uf3 used_roots_uf3 trace_uf3 "uf3.smt2" "uf3.vtlog". - Compute Euf_Checker.checker t_i_uf3 t_func_uf3 t_atom_uf3 t_form_uf3 root_uf3 used_roots_uf3 trace_uf3. + Compute @Euf_Checker.checker t_i_uf3 t_func_uf3 t_atom_uf3 t_form_uf3 root_uf3 used_roots_uf3 trace_uf3. End Uf3. Section Uf4. Parse_certif_verit t_i_uf4 t_func_uf4 t_atom_uf4 t_form_uf4 root_uf4 used_roots_uf4 trace_uf4 "uf4.smt2" "uf4.vtlog". - Compute Euf_Checker.checker t_i_uf4 t_func_uf4 t_atom_uf4 t_form_uf4 root_uf4 used_roots_uf4 trace_uf4. + Compute @Euf_Checker.checker t_i_uf4 t_func_uf4 t_atom_uf4 t_form_uf4 root_uf4 used_roots_uf4 trace_uf4. End Uf4. Section Uf5. Parse_certif_verit t_i_uf5 t_func_uf5 t_atom_uf5 t_form_uf5 root_uf5 used_roots_uf5 trace_uf5 "uf5.smt2" "uf5.vtlog". - Compute Euf_Checker.checker t_i_uf5 t_func_uf5 t_atom_uf5 t_form_uf5 root_uf5 used_roots_uf5 trace_uf5. + Compute @Euf_Checker.checker t_i_uf5 t_func_uf5 t_atom_uf5 t_form_uf5 root_uf5 used_roots_uf5 trace_uf5. End Uf5. Section Uf6. Parse_certif_verit t_i_uf6 t_func_uf6 t_atom_uf6 t_form_uf6 root_uf6 used_roots_uf6 trace_uf6 "uf6.smt2" "uf6.vtlog". - Compute Euf_Checker.checker t_i_uf6 t_func_uf6 t_atom_uf6 t_form_uf6 root_uf6 used_roots_uf6 trace_uf6. + Compute @Euf_Checker.checker t_i_uf6 t_func_uf6 t_atom_uf6 t_form_uf6 root_uf6 used_roots_uf6 trace_uf6. End Uf6. Section Uf7. Parse_certif_verit t_i_uf7 t_func_uf7 t_atom_uf7 t_form_uf7 root_uf7 used_roots_uf7 trace_uf7 "uf7.smt2" "uf7.vtlog". - Compute Euf_Checker.checker t_i_uf7 t_func_uf7 t_atom_uf7 t_form_uf7 root_uf7 used_roots_uf7 trace_uf7. + Compute @Euf_Checker.checker t_i_uf7 t_func_uf7 t_atom_uf7 t_form_uf7 root_uf7 used_roots_uf7 trace_uf7. End Uf7. Section Lia1. Parse_certif_verit t_i_lia1 t_func_lia1 t_atom_lia1 t_form_lia1 root_lia1 used_roots_lia1 trace_lia1 "lia1.smt2" "lia1.vtlog". - Compute Euf_Checker.checker t_i_lia1 t_func_lia1 t_atom_lia1 t_form_lia1 root_lia1 used_roots_lia1 trace_lia1. + Compute @Euf_Checker.checker t_i_lia1 t_func_lia1 t_atom_lia1 t_form_lia1 root_lia1 used_roots_lia1 trace_lia1. End Lia1. Section Lia2. Parse_certif_verit t_i_lia2 t_func_lia2 t_atom_lia2 t_form_lia2 root_lia2 used_roots_lia2 trace_lia2 "lia2.smt2" "lia2.vtlog". - Compute Euf_Checker.checker t_i_lia2 t_func_lia2 t_atom_lia2 t_form_lia2 root_lia2 used_roots_lia2 trace_lia2. + Compute @Euf_Checker.checker t_i_lia2 t_func_lia2 t_atom_lia2 t_form_lia2 root_lia2 used_roots_lia2 trace_lia2. End Lia2. Section Lia3. Parse_certif_verit t_i_lia3 t_func_lia3 t_atom_lia3 t_form_lia3 root_lia3 used_roots_lia3 trace_lia3 "lia3.smt2" "lia3.vtlog". - Compute Euf_Checker.checker t_i_lia3 t_func_lia3 t_atom_lia3 t_form_lia3 root_lia3 used_roots_lia3 trace_lia3. + Compute @Euf_Checker.checker t_i_lia3 t_func_lia3 t_atom_lia3 t_form_lia3 root_lia3 used_roots_lia3 trace_lia3. End Lia3. Section Lia4. Parse_certif_verit t_i_lia4 t_func_lia4 t_atom_lia4 t_form_lia4 root_lia4 used_roots_lia4 trace_lia4 "lia4.smt2" "lia4.vtlog". - Compute Euf_Checker.checker t_i_lia4 t_func_lia4 t_atom_lia4 t_form_lia4 root_lia4 used_roots_lia4 trace_lia4. + Compute @Euf_Checker.checker t_i_lia4 t_func_lia4 t_atom_lia4 t_form_lia4 root_lia4 used_roots_lia4 trace_lia4. End Lia4. Section Lia5. Parse_certif_verit t_i_lia5 t_func_lia5 t_atom_lia5 t_form_lia5 root_lia5 used_roots_lia5 trace_lia5 "lia5.smt2" "lia5.vtlog". - Compute Euf_Checker.checker t_i_lia5 t_func_lia5 t_atom_lia5 t_form_lia5 root_lia5 used_roots_lia5 trace_lia5. + Compute @Euf_Checker.checker t_i_lia5 t_func_lia5 t_atom_lia5 t_form_lia5 root_lia5 used_roots_lia5 trace_lia5. End Lia5. Section Lia6. Parse_certif_verit t_i_lia6 t_func_lia6 t_atom_lia6 t_form_lia6 root_lia6 used_roots_lia6 trace_lia6 "lia6.smt2" "lia6.vtlog". - Compute Euf_Checker.checker t_i_lia6 t_func_lia6 t_atom_lia6 t_form_lia6 root_lia6 used_roots_lia6 trace_lia6. + Compute @Euf_Checker.checker t_i_lia6 t_func_lia6 t_atom_lia6 t_form_lia6 root_lia6 used_roots_lia6 trace_lia6. End Lia6. Section Lia7. Parse_certif_verit t_i_lia7 t_func_lia7 t_atom_lia7 t_form_lia7 root_lia7 used_roots_lia7 trace_lia7 "lia7.smt2" "lia7.vtlog". - Compute Euf_Checker.checker t_i_lia7 t_func_lia7 t_atom_lia7 t_form_lia7 root_lia7 used_roots_lia7 trace_lia7. + Compute @Euf_Checker.checker t_i_lia7 t_func_lia7 t_atom_lia7 t_form_lia7 root_lia7 used_roots_lia7 trace_lia7. End Lia7. (* Section Let1. Parse_certif_verit t_i_let1 t_func_let1 t_atom_let1 t_form_let1 root_let1 used_roots_let1 trace_let1 "let1.smt2" "let1.vtlog". - Compute Euf_Checker.checker t_i_let1 t_func_let1 t_atom_let1 t_form_let1 root_let1 used_roots_let1 trace_let1. + Compute @Euf_Checker.checker t_i_let1 t_func_let1 t_atom_let1 t_form_let1 root_let1 used_roots_let1 trace_let1. End Let1. Section Let2. Parse_certif_verit t_i_let2 t_func_let2 t_atom_let2 t_form_let2 root_let2 used_roots_let2 trace_let2 "let2.smt2" "let2.vtlog". - Compute Euf_Checker.checker t_i_let2 t_func_let2 t_atom_let2 t_form_let2 root_let2 used_roots_let2 trace_let2. + Compute @Euf_Checker.checker t_i_let2 t_func_let2 t_atom_let2 t_form_let2 root_let2 used_roots_let2 trace_let2. End Let2. *) |