diff options
Diffstat (limited to 'src/Trace.v')
| -rw-r--r-- | src/Trace.v | 401 |
1 files changed, 322 insertions, 79 deletions
diff --git a/src/Trace.v b/src/Trace.v index d01ccbe..4d832de 100644 --- a/src/Trace.v +++ b/src/Trace.v @@ -1,13 +1,9 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2016 *) +(* Copyright (C) 2011 - 2019 *) (* *) -(* Michaël Armand *) -(* Benjamin Grégoire *) -(* Chantal Keller *) -(* *) -(* Inria - École Polytechnique - Université Paris-Sud *) +(* See file "AUTHORS" for the list of authors *) (* *) (* This file is distributed under the terms of the CeCILL-C licence *) (* *) @@ -16,7 +12,9 @@ Require Import Bool Int63 PArray. Require Structures. -Require Import Misc State SMT_terms Cnf Euf Lia Syntactic Arithmetic Operators Assumptions. +Require Import Misc State SMT_terms. +Require Import Syntactic Arithmetic Operators Assumptions. +Require Import Cnf Euf Lia BVList Bva_checker Array_checker. Local Open Scope array_scope. Local Open Scope int63_scope. @@ -51,9 +49,7 @@ Section trace. (* For debugging *) (* - Variable check_step_debug : S.t -> step -> option S.t. - Definition _checker_debug_ (s: S.t) (t: _trace_) : sum S.t ((int*int)*S.t) := let s' := PArray.foldi_left (fun i s a => PArray.foldi_left (fun j s' a' => match s' with @@ -65,7 +61,6 @@ Section trace. | u => u end) s a) (inl s) t in s'. - Definition _checker_partial_ (s: S.t) (t: _trace_) (max:int) : S.t := PArray.fold_left (fun s a => PArray.foldi_left (fun i s' a' => if i < max then check_step s' a' else s') s a) s t. *) @@ -99,6 +94,12 @@ Module Sat_Checker. Inductive step := | Res (_:int) (_:resolution). +(* + Parameters (s s': (list _lit) -> bool) (t: (array (list _lit))) (i: int) (r: resolution). + Check (fun s (st:step) => let (pos, r) := st in S.set_resolve s pos r). + Check (_checker_ (fun s' (st:step) => let (pos, r) := st in S.set_resolve s' pos r) s t). +*) + Definition resolution_checker s t := _checker_ (fun s (st:step) => let (pos, r) := st in S.set_resolve s pos r) s t. @@ -180,16 +181,15 @@ Qed. Lemma theorem_checker : forall d c, checker d c = true -> - forall rho, negb (valid (interp_var rho) d). + forall rho, ~ (valid (interp_var rho) d). Proof. - intros d c H rho. - apply negb_true_iff. apply neg_eq_true_eq_false. - apply checker_correct with c;trivial. - split;compute;trivial;discriminate. + intros d c H rho;apply checker_correct with c;trivial. + split;compute;trivial;discriminate. Qed. End Sat_Checker. + Module Cnf_Checker. Inductive step := @@ -222,13 +222,13 @@ Module Cnf_Checker. | ImmBuildProj pos cid i => S.set_clause s pos (check_ImmBuildProj t_form s cid i) end. - Lemma step_checker_correct : forall rho t_form, + Lemma step_checker_correct : forall rho rhobv t_form, Form.check_form t_form -> - forall s, S.valid (Form.interp_state_var rho t_form) s -> - forall st : step, S.valid (Form.interp_state_var rho t_form) + forall s, S.valid (Form.interp_state_var rho rhobv t_form) s -> + forall st : step, S.valid (Form.interp_state_var rho rhobv t_form) (step_checker t_form s st). Proof. - intros rho t_form Ht s H; destruct (Form.check_form_correct rho _ Ht) as [[Ht1 Ht2] Ht3]; intros [pos res|pos cid lf|pos|pos|pos l|pos l|pos l i|pos cid|pos cid|pos cid i]; simpl; try apply S.valid_set_clause; auto. + intros rho rhobv t_form Ht s H; destruct (Form.check_form_correct rho rhobv _ Ht) as [[Ht1 Ht2] Ht3]; intros [pos res|pos cid lf|pos|pos|pos l|pos l|pos l i|pos cid|pos cid|pos cid i]; simpl; try apply S.valid_set_clause; auto. apply S.valid_set_resolve; auto. apply valid_check_flatten; auto; try discriminate; intros a1 a2; unfold is_true; rewrite Int63Properties.eqb_spec; intro; subst a1; auto. apply valid_check_True; auto. @@ -244,12 +244,12 @@ Module Cnf_Checker. Definition cnf_checker t_form s t := _checker_ (step_checker t_form) s t. - Lemma cnf_checker_correct : forall rho t_form, + Lemma cnf_checker_correct : forall rho rhobv t_form, Form.check_form t_form -> forall s t confl, cnf_checker t_form C.is_false s t confl -> - ~ (S.valid (Form.interp_state_var rho t_form) s). + ~ (S.valid (Form.interp_state_var rho rhobv t_form) s). Proof. - unfold cnf_checker; intros rho t_form Ht; apply _checker__correct. + unfold cnf_checker; intros rho rhobv t_form Ht; apply _checker__correct. intros c H; apply C.is_false_correct; auto. apply step_checker_correct; auto. Qed. @@ -265,9 +265,9 @@ Module Cnf_Checker. Lemma checker_correct : forall t_form l c, checker t_form l c = true -> - forall rho, ~ (Lit.interp (Form.interp_state_var rho t_form) l). + forall rho rhobv, ~ (Lit.interp (Form.interp_state_var rho rhobv t_form) l). Proof. - unfold checker; intros t_form l (nclauses, t, confl); unfold is_true; rewrite andb_true_iff; intros [H1 H2] rho H; apply (cnf_checker_correct (rho:=rho) H1 H2); destruct (Form.check_form_correct rho _ H1) as [[Ht1 Ht2] Ht3]; apply S.valid_set_clause; auto. + unfold checker; intros t_form l (nclauses, t, confl); unfold is_true; rewrite andb_true_iff; intros [H1 H2] rho rhobv H; apply (cnf_checker_correct (rho:=rho) (rhobv:=rhobv) H1 H2); destruct (Form.check_form_correct rho rhobv _ H1) as [[Ht1 Ht2] Ht3]; apply S.valid_set_clause; auto. apply S.valid_make; auto. unfold C.valid; simpl; rewrite H; auto. Qed. @@ -278,9 +278,9 @@ Module Cnf_Checker. Lemma checker_b_correct : forall t_var t_form l b c, checker_b t_form l b c = true -> - Lit.interp (Form.interp_state_var (PArray.get t_var) t_form) l = b. + Lit.interp (Form.interp_state_var (PArray.get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l = b. Proof. - unfold checker_b; intros t_var t_form l b c; case b; case_eq (Lit.interp (Form.interp_state_var (get t_var) t_form) l); auto; intros H1 H2; elim (checker_correct H2 (rho:=get t_var)); auto; rewrite Lit.interp_neg, H1; auto. + unfold checker_b; intros t_var t_form l b c; case b; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l); auto; intros H1 H2; elim (checker_correct H2 (rho:=get t_var) (rhobv:=fun _ s => BITVECTOR_LIST.zeros s)); auto; rewrite Lit.interp_neg, H1; auto. Qed. Definition checker_eq t_form l1 l2 l (c:certif) := @@ -293,12 +293,12 @@ Module Cnf_Checker. Lemma checker_eq_correct : forall t_var t_form l1 l2 l c, checker_eq t_form l1 l2 l c = true -> - Lit.interp (Form.interp_state_var (PArray.get t_var) t_form) l1 = - Lit.interp (Form.interp_state_var (PArray.get t_var) t_form) l2. + Lit.interp (Form.interp_state_var (PArray.get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l1 = + Lit.interp (Form.interp_state_var (PArray.get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l2. Proof. - unfold checker_eq; intros t_var t_form l1 l2 l c; 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; destruct c as (nclauses, t, confl); rewrite andb_true_iff in H3; destruct H3 as [H3 _]; destruct (Form.check_form_correct (get t_var) _ H3) as [[Ht1 Ht2] Ht3]; split; auto. - destruct H as [H1 H2]; case_eq (Lit.interp (Form.interp_state_var (get t_var) t_form) l1); intro Heq1; case_eq (Lit.interp (Form.interp_state_var (get t_var) t_form) l2); intro Heq2; auto; elim (checker_correct H3 (rho:=get t_var)); unfold Lit.interp; rewrite Heq'; unfold Var.interp; rewrite Form.wf_interp_form; auto; rewrite Heq; simpl; rewrite Heq1, Heq2; auto. + unfold checker_eq; intros t_var t_form l1 l2 l c; 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 a ls Heq]; 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; destruct c as (nclauses, t, confl); rewrite andb_true_iff in H3; destruct H3 as [H3 _]; destruct (Form.check_form_correct (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) _ H3) as [[Ht1 Ht2] Ht3]; split; auto. + destruct H as [H1 H2]; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l1); intro Heq1; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l2); intro Heq2; auto; elim (checker_correct H3 (rho:=get t_var) (rhobv:=fun _ s => BITVECTOR_LIST.zeros s)); unfold Lit.interp; rewrite Heq'; unfold Var.interp; rewrite Form.wf_interp_form; auto; rewrite Heq; simpl; rewrite Heq1, Heq2; auto. Qed. End Cnf_Checker. @@ -314,13 +314,14 @@ Module Euf_Checker. Section Checker. - Variable t_i : array typ_eqb. + Variable t_i : array SMT_classes.typ_compdec. 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) + | Weaken (pos:int) (cid:clause_id) (cl:list _lit) | ImmFlatten (pos:int) (cid:clause_id) (lf:_lit) | CTrue (pos:int) | CFalse (pos:int) @@ -337,12 +338,33 @@ Inductive step := | 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) + (* Bit-blasting *) + | BBVar (pos:int) (res:_lit) + | BBConst (pos:int) (res:_lit) + | BBOp (pos:int) (orig1 orig2:clause_id) (res:_lit) + | BBNot (pos:int) (orig:clause_id) (res:_lit) + | BBNeg (pos:int) (orig:clause_id) (res:_lit) + | BBAdd (pos:int) (orig1 orig2:clause_id) (res:_lit) + | BBConcat (pos:int) (orig1 orig2:clause_id) (res:_lit) + | BBMul (pos:int) (orig1 orig2:clause_id) (res:_lit) + | BBUlt (pos:int) (orig1 orig2:clause_id) (res:_lit) + | BBSlt (pos:int) (orig1 orig2:clause_id) (res:_lit) + | BBEq (pos:int) (orig1 orig2:clause_id) (res:_lit) + | BBDiseq (pos:int) (res:_lit) + | BBExtract (pos:int) (orig:clause_id) (res:_lit) + | BBZextend (pos:int) (orig:clause_id) (res:_lit) + | BBSextend (pos:int) (orig:clause_id) (res:_lit) + | BBShl (pos:int) (orig1 orig2:clause_id) (res:_lit) + | BBShr (pos:int) (orig1 orig2:clause_id) (res:_lit) + | RowEq (pos:int) (res: _lit) + | RowNeq (pos:int) (cl: C.t) + | Ext (pos:int) (res: _lit) (* Offer the possibility to discharge parts of the proof to (manual) Coq proofs. WARNING: this breaks extraction. *) | Hole (pos:int) (prem_id:list clause_id) (prem:list C.t) (concl:C.t) - (p:interp_conseq_uf (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) prem concl) + (p:interp_conseq_uf (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) prem concl) | ForallInst (pos:int) (lemma:Prop) (plemma:lemma) (concl:C.t) - (p: lemma -> interp_conseq_uf (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) nil concl) + (p: lemma -> interp_conseq_uf (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) nil concl) . Local Open Scope list_scope. @@ -352,6 +374,7 @@ Inductive step := Definition step_checker s (st:step) := match st with | Res pos res => S.set_resolve s pos res + | Weaken pos cid cl => S.set_weaken s pos cid cl | ImmFlatten pos cid lf => S.set_clause s pos (check_flatten t_atom t_form s cid lf) | CTrue pos => S.set_clause s pos Cnf.check_True | CFalse pos => S.set_clause s pos Cnf.check_False @@ -368,46 +391,98 @@ Inductive step := | 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) + | BBVar pos res => S.set_clause s pos (check_bbVar t_atom t_form res) + | BBConst pos res => S.set_clause s pos (check_bbConst t_atom t_form res) + | BBOp pos orig1 orig2 res => S.set_clause s pos (check_bbOp t_atom t_form s orig1 orig2 res) + | BBNot pos orig res => S.set_clause s pos (check_bbNot t_atom t_form s orig res) + | BBNeg pos orig res => S.set_clause s pos (check_bbNeg t_atom t_form s orig res) + | BBAdd pos orig1 orig2 res => S.set_clause s pos (check_bbAdd t_atom t_form s orig1 orig2 res) + | BBConcat pos orig1 orig2 res => S.set_clause s pos (check_bbConcat t_atom t_form s orig1 orig2 res) + | BBMul pos orig1 orig2 res => S.set_clause s pos (check_bbMult t_atom t_form s orig1 orig2 res) + | BBUlt pos orig1 orig2 res => S.set_clause s pos (check_bbUlt t_atom t_form s orig1 orig2 res) + | BBSlt pos orig1 orig2 res => S.set_clause s pos (check_bbSlt t_atom t_form s orig1 orig2 res) + | BBEq pos orig1 orig2 res => S.set_clause s pos (check_bbEq t_atom t_form s orig1 orig2 res) + | BBDiseq pos res => S.set_clause s pos (check_bbDiseq t_atom t_form res) + | BBExtract pos orig res => S.set_clause s pos (check_bbExtract t_atom t_form s orig res) + | BBZextend pos orig res => S.set_clause s pos (check_bbZextend t_atom t_form s orig res) + | BBSextend pos orig res => S.set_clause s pos (check_bbSextend t_atom t_form s orig res) + | BBShl pos orig1 orig2 res => S.set_clause s pos (check_bbShl t_atom t_form s orig1 orig2 res) + | BBShr pos orig1 orig2 res => S.set_clause s pos (check_bbShr t_atom t_form s orig1 orig2 res) + | RowEq pos res => S.set_clause s pos (check_roweq t_form t_atom res) + | RowNeq pos cl => S.set_clause s pos (check_rowneq t_form t_atom cl) + | Ext pos res => S.set_clause s pos (check_ext t_form t_atom res) | @Hole pos prem_id prem concl _ => S.set_clause s pos (check_hole s prem_id prem concl) | @ForallInst pos lemma _ concl _ => S.set_clause s pos concl end. + (* Opaque S.set_weaken. *) + Lemma step_checker_correct : - let rho := Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form in + let rho := Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv 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 s st). Proof. - 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 prem_id prem concl p | pos lemma plemma concl 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. - rewrite (Syntactic.check_neg_hatom_correct_bool _ _ _ H10 Ha1 Ha2 _ _ H); auto. - apply valid_check_True; auto. - apply valid_check_False; auto. - apply valid_check_BuildDef; auto. - apply valid_check_BuildDef2; auto. - apply valid_check_BuildProj; auto. - apply valid_check_ImmBuildDef; auto. - apply valid_check_ImmBuildDef2; auto. - apply valid_check_ImmBuildProj; auto. - apply valid_check_trans; auto. - apply valid_check_congr; auto. - apply valid_check_congr_pred; auto. - apply valid_check_micromega; auto. - apply valid_check_diseq; auto. - apply valid_check_spl_arith; auto. - apply valid_check_distinct_elim; auto. - apply valid_check_hole; auto. - apply valid_check_forall_inst with lemma; auto. + set (empty_bv := (fun (a:Atom.atom) s => BITVECTOR_LIST.zeros s)). + intros rho H1 H2 H10 s Hs. destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv 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 c|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|pos res|pos orig1 orig2 res|pos orig res|pos orig res + |pos orig1 orig2 res|pos orig1 orig2 res + |pos orig1 orig2 res|pos orig1 orig2 res|pos orig1 orig2 res|pos orig1 orig2 res + |pos cl |pos orig res |pos orig res |pos orig res | pos orig1 orig2 res | pos orig1 orig2 res |pos res|pos res + |pos res |pos prem_id prem concl p|pos lemma plemma concl p]; simpl; try apply S.valid_set_clause; auto. + - apply S.valid_set_resolve; auto. + - apply S.valid_set_weaken; auto. + - apply valid_check_flatten; auto; intros h1 h2 H. + + rewrite (Syntactic.check_hatom_correct_bool _ _ _ Ha1 Ha2 _ _ H); auto. + + rewrite (Syntactic.check_neg_hatom_correct_bool _ _ _ H10 Ha1 Ha2 _ _ H); auto. + - apply valid_check_True; auto. + - apply valid_check_False; auto. + - apply valid_check_BuildDef; auto. + - apply valid_check_BuildDef2; auto. + - apply valid_check_BuildProj; auto. + - apply valid_check_ImmBuildDef; auto. + - apply valid_check_ImmBuildDef2; auto. + - apply valid_check_ImmBuildProj; auto. + - apply valid_check_trans; auto. + - apply valid_check_congr; auto. + - apply valid_check_congr_pred; auto. + - apply valid_check_micromega; auto. + - apply valid_check_diseq; auto. + - apply valid_check_spl_arith; auto. + - apply valid_check_distinct_elim; auto. + - eapply valid_check_bbVar; eauto. + - apply valid_check_bbConst; auto. + - apply valid_check_bbOp; auto. + - apply valid_check_bbNot; auto. + - apply valid_check_bbNeg; auto. + - apply valid_check_bbAdd; auto. + - apply valid_check_bbConcat; auto. + - apply valid_check_bbMult; auto. + - apply valid_check_bbUlt; auto. + - apply valid_check_bbSlt; auto. + - apply valid_check_bbEq; auto. + - apply valid_check_bbDiseq; auto. + - apply valid_check_bbExtract; auto. + - apply valid_check_bbZextend; auto. + - apply valid_check_bbSextend; auto. + - apply valid_check_bbShl; auto. + - apply valid_check_bbShr; auto. + - apply valid_check_roweq; auto. + - apply valid_check_rowneq; auto. + - apply valid_check_ext; auto. + - apply valid_check_hole; auto. + - apply valid_check_forall_inst with lemma; auto. Qed. 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, *) - let rho := Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form in + let rho := Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv 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, @@ -431,17 +506,17 @@ Inductive step := end. Definition valid t_i t_func t_atom t_form d := - let rho := Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form in + let rho := Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv 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, *) - let rho := Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form in + let rho := Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv 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) (Atom.interp_form_hatom_bv 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. @@ -455,14 +530,188 @@ Inductive step := euf_checker (* t_atom t_form *) C.is_false (add_roots (S.make nclauses) d used_roots) t confl. Implicit Arguments checker []. + + Definition setup_checker_step_debug d used_roots (c:certif) := + let (nclauses, t, confl) := c in + let s := add_roots (S.make nclauses) d used_roots in + (s, Structures.trace_to_list t). + + + Definition position_of_step (st:step) := + match st with + | Res pos _ + | Weaken pos _ _ + | ImmFlatten pos _ _ + | CTrue pos + | CFalse pos + | BuildDef pos _ + | BuildDef2 pos _ + | BuildProj pos _ _ + | ImmBuildDef pos _ + | ImmBuildDef2 pos _ + | ImmBuildProj pos _ _ + | EqTr pos _ _ + | EqCgr pos _ _ + | EqCgrP pos _ _ _ + | LiaMicromega pos _ _ + | LiaDiseq pos _ + | SplArith pos _ _ _ + | SplDistinctElim pos _ _ + | BBVar pos _ + | BBConst pos _ + | BBOp pos _ _ _ + | BBNot pos _ _ + | BBNeg pos _ _ + | BBAdd pos _ _ _ + | BBConcat pos _ _ _ + | BBMul pos _ _ _ + | BBUlt pos _ _ _ + | BBSlt pos _ _ _ + | BBEq pos _ _ _ + | BBDiseq pos _ + | BBExtract pos _ _ + | BBZextend pos _ _ + | BBSextend pos _ _ + | BBShl pos _ _ _ + | BBShr pos _ _ _ + | RowEq pos _ + | RowNeq pos _ + | Ext pos _ + | @Hole pos _ _ _ _ + | @ForallInst pos _ _ _ _ => pos + end. + + + Definition checker_step_debug s step_t := + let s := step_checker s step_t in + (s, C.has_true (S.get s (position_of_step step_t))). + + + Definition ignore_true_step (st:step) := + match st with + | CTrue _ + (* | Res _ _ *) + | @Hole _ _ _ _ _ => true + | _ => false + end. + + Inductive name_step := + | Name_Res + | Name_Weaken + | Name_ImmFlatten + | Name_CTrue + | Name_CFalse + | Name_BuildDef + | Name_BuildDef2 + | Name_BuildProj + | Name_ImmBuildDef + | Name_ImmBuildDef2 + | Name_ImmBuildProj + | Name_EqTr + | Name_EqCgr + | Name_EqCgrP + | Name_LiaMicromega + | Name_LiaDiseq + | Name_SplArith + | Name_SplDistinctElim + | Name_BBVar + | Name_BBConst + | Name_BBOp + | Name_BBNot + | Name_BBNeg + | Name_BBAdd + | Name_BBConcat + | Name_BBMul + | Name_BBUlt + | Name_BBSlt + | Name_BBEq + | Name_BBDiseq + | Name_BBExtract + | Name_BBZextend + | Name_BBSextend + | Name_BBShl + | Name_BBShr + | Name_RowEq + | Name_RowNeq + | Name_Ext + | Name_Hole + | Name_ForallInst. + + Definition name_of_step (st:step) := + match st with + | Res _ _ => Name_Res + | Weaken _ _ _ => Name_Weaken + | ImmFlatten _ _ _ => Name_ImmFlatten + | CTrue _ => Name_CTrue + | CFalse _ => Name_CFalse + | BuildDef _ _ => Name_BuildDef + | BuildDef2 _ _ => Name_BuildDef2 + | BuildProj _ _ _ => Name_BuildProj + | ImmBuildDef _ _ => Name_ImmBuildDef + | ImmBuildDef2 _ _ => Name_ImmBuildDef2 + | ImmBuildProj _ _ _ => Name_ImmBuildProj + | EqTr _ _ _ => Name_EqTr + | EqCgr _ _ _ => Name_EqCgr + | EqCgrP _ _ _ _ => Name_EqCgrP + | LiaMicromega _ _ _ => Name_LiaMicromega + | LiaDiseq _ _ => Name_LiaDiseq + | SplArith _ _ _ _ => Name_SplArith + | SplDistinctElim _ _ _ => Name_SplDistinctElim + | BBVar _ _ => Name_BBVar + | BBConst _ _ => Name_BBConst + | BBOp _ _ _ _ => Name_BBOp + | BBNot _ _ _ => Name_BBNot + | BBNeg _ _ _ => Name_BBNeg + | BBAdd _ _ _ _ => Name_BBAdd + | BBConcat _ _ _ _ => Name_BBConcat + | BBMul _ _ _ _ => Name_BBMul + | BBUlt _ _ _ _ => Name_BBUlt + | BBSlt _ _ _ _ => Name_BBSlt + | BBEq _ _ _ _ => Name_BBEq + | BBDiseq _ _ => Name_BBDiseq + | BBExtract _ _ _ => Name_BBExtract + | BBZextend _ _ _ => Name_BBZextend + | BBSextend _ _ _ => Name_BBSextend + | BBShl _ _ _ _ => Name_BBShl + | BBShr _ _ _ _ => Name_BBShr + | RowEq _ _ => Name_RowEq + | RowNeq _ _ => Name_RowNeq + | Ext _ _ => Name_Ext + | @Hole _ _ _ _ _ => Name_Hole + | @ForallInst _ _ _ _ _ => Name_ForallInst + end. + + + Definition checker_debug d used_roots (c:certif) := + let (nclauses, t, confl) := c in + let s := add_roots (S.make nclauses) d used_roots in + let '(_, nb, failure) := + Structures.trace_fold + (fun acc step => + match acc with + | (s, nb, None) => + let nb := S nb in + let s := step_checker s step in + if negb (ignore_true_step step) && + C.has_true (S.get s (position_of_step step)) then + (s, nb, Some step) + else (s, nb, None) + | _ => acc + end + ) (s, O, None) t + in + match failure with + | Some st => Some (nb, name_of_step st) + | None => None + end + . + + 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 -> - negb (valid t_func t_atom t_form d). + ~ (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]. - apply Is_true_eq_true. apply negb_prop_intro. intro H. - apply Is_true_eq_true in 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) (Atom.interp_form_hatom_bv 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) := @@ -472,12 +721,9 @@ Inductive step := 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. + Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv 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; - assert (G:= checker_correct H2); - apply negb_true_iff in G; apply neg_eq_true_eq_false in G; - elim G; 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) (Atom.interp_form_hatom_bv 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) := @@ -491,15 +737,12 @@ Inductive step := 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. + Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv 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) (Atom.interp_form_hatom_bv 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 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; - assert (G:= checker_correct H3); - apply negb_true_iff in G; apply neg_eq_true_eq_false in G; - elim G; 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. + 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 a ls Heq]; 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) (Atom.interp_form_hatom_bv 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) (Atom.interp_form_hatom_bv 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) (Atom.interp_form_hatom_bv 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. |