diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-10-21 14:03:32 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-10-21 14:03:32 +0100 |
commit | 7bbedef94189dc9ab094619ee00bc9aaf0fd110a (patch) | |
tree | 203053b236c507fa3f0c5d6f8445af625d1bbb14 /src/hls/Abstr.v | |
parent | 1d86b1c178deb97f3d499f461a417a4fe6846cf8 (diff) | |
download | vericert-7bbedef94189dc9ab094619ee00bc9aaf0fd110a.tar.gz vericert-7bbedef94189dc9ab094619ee00bc9aaf0fd110a.zip |
Add work towards decidability of SAT solver
Diffstat (limited to 'src/hls/Abstr.v')
-rw-r--r-- | src/hls/Abstr.v | 127 |
1 files changed, 98 insertions, 29 deletions
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index dc883b2..54fda33 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -34,6 +34,7 @@ Require Import vericert.hls.RTLBlock. Require Import vericert.hls.RTLPar. Require Import vericert.hls.RTLBlockInstr. Require Import vericert.hls.HashTree. +Require Import vericert.hls.Predicate. #[local] Open Scope positive. #[local] Open Scope pred_op. @@ -573,7 +574,7 @@ Fixpoint norm_expression (max: predicate) (pe: pred_expr) (h: hash_tree) end end. -Definition mk_pred_stmnt' pr_op e p_e := (¬ p_e ∨ Pvar e) ∧ pr_op. +Definition mk_pred_stmnt' pr_op e p_e := (¬ p_e ∨ Pvar (true, e)) ∧ pr_op. Definition mk_pred_stmnt t := PTree.fold mk_pred_stmnt' t T. @@ -597,12 +598,11 @@ Definition encode_expression max pe h := Fixpoint max_predicate (p: pred_op) : positive := match p with - | Pvar p => p + | Pvar (b, p) => p | Ptrue => 1 | Pfalse => 1 | Pand a b => Pos.max (max_predicate a) (max_predicate b) | Por a b => Pos.max (max_predicate a) (max_predicate b) - | Pnot a => max_predicate a end. Fixpoint max_pred_expr (pe: pred_expr) : positive := @@ -653,15 +653,20 @@ Proof. apply andb_false_iff in H. inv H. auto. rewrite H0 in H1. discriminate. Qed. -Lemma unsat_not a: unsat (Pand a (Pnot a)). -Proof. unfold unsat; simplify; auto with bool. Qed. +Lemma unsat_not a: unsat (a ∧ (¬ a)). +Proof. + unfold unsat; simplify. + rewrite negate_correct. + auto with bool. +Qed. -Lemma unsat_commut a b: unsat (Pand a b) -> unsat (Pand b a). +Lemma unsat_commut a b: unsat (a ∧ b) -> unsat (b ∧ a). Proof. unfold unsat; simplify; eauto with bool. Qed. -Lemma sat_dec a n b: sat_pred n a = Some b -> {sat a} + {unsat a}. +Lemma sat_dec a: {sat a} + {unsat a}. Proof. - unfold sat, unsat. destruct b. + unfold sat, unsat. + destruct (sat_pred a). intros. left. destruct s. exists (Sat.interp_alist x). auto. intros. tauto. @@ -686,39 +691,86 @@ Instance Equivalence_SAT : Equivalence equiv := Lemma sat_equiv : forall a b, - unsat (Por (Pand a (Pnot b)) (Pand (Pnot a) b)) -> equiv a b. + unsat (a ∧ ¬ b ∨ ¬ a ∧ b) -> equiv a b. Proof. unfold unsat, equiv. intros. specialize (H c); simplify. + rewrite negate_correct in *. destruct (sat_predicate b c) eqn:X; destruct (sat_predicate a c) eqn:X2; crush. Qed. +Lemma sat_predicate_and : + forall a b c, + sat_predicate (a ∧ b) c = sat_predicate a c && sat_predicate b c. +Proof. crush. Qed. + +Lemma sat_predicate_or : + forall a b c, + sat_predicate (a ∨ b) c = sat_predicate a c || sat_predicate b c. +Proof. crush. Qed. + Lemma sat_equiv2 : forall a b, - unsat (Por (Pand a (Pnot b)) (Pand b (Pnot a))) -> equiv a b. + equiv a b -> unsat (a ∧ ¬ b ∨ ¬ a ∧ b). +Proof. + unfold unsat, equiv; simplify. + repeat rewrite negate_correct. + repeat rewrite H. + rewrite andb_negb_r. + rewrite andb_negb_l. auto. +Qed. + +Lemma sat_equiv3 : + forall a b, + unsat (a ∧ ¬ b ∨ b ∧ ¬ a) -> equiv a b. Proof. unfold unsat, equiv. intros. specialize (H c); simplify. + rewrite negate_correct in *. destruct (sat_predicate b c) eqn:X; destruct (sat_predicate a c) eqn:X2; crush. Qed. -Definition equiv_check n p1 p2 := - match sat_pred_simple n (p1 ∧ ¬ p2 ∨ p2 ∧ ¬ p1) with - | Some None => true +Lemma sat_equiv4 : + forall a b, + equiv a b -> unsat (a ∧ ¬ b ∨ b ∧ ¬ a). +Proof. + unfold unsat, equiv; simplify. + repeat rewrite negate_correct. + repeat rewrite H. + rewrite andb_negb_r. auto. +Qed. + +Definition equiv_check p1 p2 := + match sat_pred_simple (p1 ∧ ¬ p2 ∨ p2 ∧ ¬ p1) with + | None => true | _ => false end. Lemma equiv_check_correct : - forall n p1 p2, equiv_check n p1 p2 = true -> equiv p1 p2. + forall p1 p2, equiv_check p1 p2 = true -> equiv p1 p2. Proof. unfold equiv_check. unfold sat_pred_simple. intros. - destruct_match; [|discriminate]. - destruct_match; [discriminate|]. - destruct_match; [|discriminate]. - destruct_match. destruct_match; discriminate. - eapply sat_equiv2; eauto. + destruct_match; try discriminate; []. + destruct_match. destruct_match. discriminate. + eapply sat_equiv3; eauto. +Qed. + +Lemma equiv_check_correct2 : + forall p1 p2, equiv p1 p2 -> equiv_check p1 p2 = true. +Proof. + unfold equiv_check, equiv, sat_pred_simple. intros. + destruct_match; auto. destruct_match; try discriminate. destruct_match. + simplify. + apply sat_equiv4 in H. unfold unsat in H. simplify. + clear Heqs. rewrite H in e. discriminate. +Qed. + +Lemma equiv_check_dec : + forall p1 p2, equiv_check p1 p2 = true <-> equiv p1 p2. +Proof. + intros; split; eauto using equiv_check_correct, equiv_check_correct2. Qed. Definition beq_pred_expr (bound: nat) (pe1 pe2: pred_expr) : bool := @@ -743,25 +795,23 @@ Definition beq_pred_expr (bound: nat) (pe1 pe2: pred_expr) : bool := let max := Pos.max (max_pred_expr pe1) (max_pred_expr pe2) in let (p1, h) := encode_expression max pe1 (PTree.empty _) in let (p2, h') := encode_expression max pe2 h in - equiv_check bound p1 p2 + equiv_check p1 p2 end. Definition check := Rtree.beq (beq_pred_expr 10000). Compute (check (empty # (Reg 2) <- - ((((Pand (Pvar 4) (Pnot (Pvar 4)))), (Ebase (Reg 9))) ::| - (NE.singleton (((Pvar 2)), (Ebase (Reg 3)))))) - (empty # (Reg 2) <- (NE.singleton (((Por (Pvar 2) (Pand (Pvar 3) (Pnot (Pvar 3))))), + ((((Pand (Pvar (true, 4)) (¬ (Pvar (true, 4))))), (Ebase (Reg 9))) ::| + (NE.singleton (((Pvar (true, 2))), (Ebase (Reg 3)))))) + (empty # (Reg 2) <- (NE.singleton (((Por (Pvar (true, 2)) (Pand (Pvar (true, 3)) (¬ (Pvar (true, 3)))))), (Ebase (Reg 3)))))). -Definition inj_asgn_f a b := if (a =? b)%nat then true else false. - Lemma inj_asgn_eg : forall a b, - inj_asgn_f a b = inj_asgn_f a a -> a = b. + (a =? b)%nat = (a =? a)%nat -> a = b. Proof. intros. destruct (Nat.eq_dec a b); subst. - auto. unfold inj_asgn_f in H. apply Nat.eqb_neq in n. + auto. apply Nat.eqb_neq in n. rewrite n in H. rewrite Nat.eqb_refl in H. discriminate. Qed. @@ -769,10 +819,30 @@ Lemma inj_asgn : forall a b, (forall (f: nat -> bool), f a = f b) -> a = b. Proof. intros. apply inj_asgn_eg. eauto. Qed. +Lemma inj_asgn_false: + forall n1 n2 , ~ (forall c: nat -> bool, c n1 = negb (c n2)). +Proof. + unfold not; intros. specialize (H (fun x => true)). + simplify. discriminate. +Qed. + +Lemma negb_inj: + forall a b, + negb a = negb b -> a = b. +Proof. destruct a, b; crush. Qed. + Lemma sat_predicate_Pvar_inj : forall p1 p2, equiv (Pvar p1) (Pvar p2) -> p1 = p2. -Proof. unfold equiv. simplify. apply Pos2Nat.inj. eapply inj_asgn. eauto. Qed. +Proof. + unfold equiv. simplify. destruct p1, p2. + destruct b, b0. + assert (p = p0). + apply Pos2Nat.inj. eapply inj_asgn. eauto. rewrite H0; auto. + admit. + assert (p = p0). apply Pos2Nat.inj. eapply inj_asgn. intros. specialize (H f). + apply negb_inj in H. auto. rewrite H0; auto. +Qed. Definition ind_preds t := forall e1 e2 p1 p2 c, @@ -799,7 +869,6 @@ Lemma pred_equivalence_Some : Proof. intros * SMEA SMEB EQ. - Lemma pred_equivalence_None : forall (ta tb: PTree.t pred_op) e pe, equiv (mk_pred_stmnt ta) (mk_pred_stmnt tb) -> |