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 | |
parent | 1d86b1c178deb97f3d499f461a417a4fe6846cf8 (diff) | |
download | vericert-7bbedef94189dc9ab094619ee00bc9aaf0fd110a.tar.gz vericert-7bbedef94189dc9ab094619ee00bc9aaf0fd110a.zip |
Add work towards decidability of SAT solver
Diffstat (limited to 'src')
-rw-r--r-- | src/hls/Abstr.v | 127 | ||||
-rw-r--r-- | src/hls/HTLPargen.v | 11 | ||||
-rw-r--r-- | src/hls/IfConversion.v | 7 | ||||
-rw-r--r-- | src/hls/Predicate.v | 201 | ||||
-rw-r--r-- | src/hls/RTLBlockInstr.v | 225 | ||||
-rw-r--r-- | src/hls/Sat.v | 85 |
6 files changed, 377 insertions, 279 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) -> diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 64996c6..e8b18dc 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -28,6 +28,7 @@ Require Import vericert.common.Statemonad. Require Import vericert.common.Vericertlib. Require Import vericert.hls.AssocMap. Require Import vericert.hls.HTL. +Require Import vericert.hls.Predicate. Require Import vericert.hls.RTLBlockInstr. Require Import vericert.hls.RTLPar. Require Import vericert.hls.ValueInt. @@ -657,12 +658,12 @@ Definition add_control_instr_force (n : node) (st : stmnt) : mon unit := Fixpoint pred_expr (preg: reg) (p: pred_op) := match p with - | Pvar pred => - Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)) + | Pvar (b, pred) => + if b + then Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)) + else Vunop Vnot (Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred))) | Ptrue => Vlit (ZToValue 1) | Pfalse => Vlit (ZToValue 0) - | Pnot pred => - Vunop Vnot (pred_expr preg pred) | Pand p1 p2 => Vbinop Vand (pred_expr preg p1) (pred_expr preg p2) | Por p1 p2 => @@ -695,7 +696,7 @@ Definition translate_inst a (fin rtrn stack preg : reg) (n : node) (i : instr) translate_predicate a preg p dst (Vvar src) | RBsetpred c args p => do cond <- translate_condition c args; - ret (a (pred_expr preg (Pvar p)) cond) + ret (a (pred_expr preg (Pvar (true, p))) cond) end. Lemma create_new_state_state_incr: diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index f8d404c..205506c 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -25,6 +25,7 @@ Require Import compcert.lib.Maps. Require Import vericert.common.Vericertlib. Require Import vericert.hls.RTLBlockInstr. Require Import vericert.hls.RTLBlock. +Require Import vericert.hls.Predicate. (*| ============= @@ -57,10 +58,10 @@ Definition if_convert_block (c: code) (p: predicate) (bb: bblock) : bblock := | RBcond cond args n1 n2 => match PTree.get n1 c, PTree.get n2 c with | Some bb1, Some bb2 => - let bb1' := List.map (map_if_convert (Pvar p)) bb1.(bb_body) in - let bb2' := List.map (map_if_convert (Pnot (Pvar p))) bb2.(bb_body) in + let bb1' := List.map (map_if_convert (Pvar (true, p))) bb1.(bb_body) in + let bb2' := List.map (map_if_convert (Pvar (false, p))) bb2.(bb_body) in mk_bblock (List.concat (bb.(bb_body) :: ((RBsetpred cond args p) :: bb1') :: bb2' :: nil)) - (RBpred_cf (Pvar p) bb1.(bb_exit) bb2.(bb_exit)) + (RBpred_cf (Pvar (true, p)) bb1.(bb_exit) bb2.(bb_exit)) | _, _ => bb end | _ => bb diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v new file mode 100644 index 0000000..d07ee28 --- /dev/null +++ b/src/hls/Predicate.v @@ -0,0 +1,201 @@ +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.Sat. + +Definition predicate : Type := positive. + +Inductive pred_op : Type := +| Pvar: (bool * predicate) -> pred_op +| Ptrue: pred_op +| Pfalse: pred_op +| Pand: pred_op -> pred_op -> pred_op +| Por: pred_op -> pred_op -> pred_op. + +Declare Scope pred_op. + +Notation "A ∧ B" := (Pand A B) (at level 20) : pred_op. +Notation "A ∨ B" := (Por A B) (at level 25) : pred_op. +Notation "⟂" := (Pfalse) : pred_op. +Notation "'T'" := (Ptrue) : pred_op. + +Fixpoint sat_predicate (p: pred_op) (a: asgn) : bool := + match p with + | Pvar (b, p') => if b then a (Pos.to_nat p') else negb (a (Pos.to_nat p')) + | Ptrue => true + | Pfalse => false + | Pand p1 p2 => sat_predicate p1 a && sat_predicate p2 a + | Por p1 p2 => sat_predicate p1 a || sat_predicate p2 a + end. + +Fixpoint mult {A: Type} (a b: list (list A)) : list (list A) := + match a with + | nil => nil + | l :: ls => mult ls b ++ (List.map (fun x => l ++ x) b) + end. + +Lemma satFormula_concat: + forall a b agn, + satFormula a agn -> + satFormula b agn -> + satFormula (a ++ b) agn. +Proof. induction a; crush. Qed. + +Lemma satFormula_concat2: + forall a b agn, + satFormula (a ++ b) agn -> + satFormula a agn /\ satFormula b agn. +Proof. + induction a; simplify; + try apply IHa in H1; crush. +Qed. + +Lemma satClause_concat: + forall a a1 a0, + satClause a a1 -> + satClause (a0 ++ a) a1. +Proof. induction a0; crush. Qed. + +Lemma satClause_concat2: + forall a a1 a0, + satClause a0 a1 -> + satClause (a0 ++ a) a1. +Proof. + induction a0; crush. + inv H; crush. +Qed. + +Lemma satClause_concat3: + forall a b c, + satClause (a ++ b) c -> + satClause a c \/ satClause b c. +Proof. + induction a; crush. + inv H; crush. + apply IHa in H0; crush. + inv H0; crush. +Qed. + +Lemma satFormula_mult': + forall p2 a a0, + satFormula p2 a0 \/ satClause a a0 -> + satFormula (map (fun x : list lit => a ++ x) p2) a0. +Proof. + induction p2; crush. + - inv H. inv H0. apply satClause_concat. auto. + apply satClause_concat2; auto. + - apply IHp2. + inv H; crush; inv H0; crush. +Qed. + +Lemma satFormula_mult2': + forall p2 a a0, + satFormula (map (fun x : list lit => a ++ x) p2) a0 -> + satClause a a0 \/ satFormula p2 a0. +Proof. + induction p2; crush. + apply IHp2 in H1. inv H1; crush. + apply satClause_concat3 in H0. + inv H0; crush. +Qed. + +Lemma satFormula_mult: + forall p1 p2 a, + satFormula p1 a \/ satFormula p2 a -> + satFormula (mult p1 p2) a. +Proof. + induction p1; crush. + apply satFormula_concat; crush. + inv H. inv H0. + apply IHp1. auto. + apply IHp1. auto. + apply satFormula_mult'; + inv H; crush. +Qed. + +Lemma satFormula_mult2: + forall p1 p2 a, + satFormula (mult p1 p2) a -> + satFormula p1 a \/ satFormula p2 a. +Proof. + induction p1; crush. + apply satFormula_concat2 in H; crush. + apply IHp1 in H0. + inv H0; crush. + apply satFormula_mult2' in H1. inv H1; crush. +Qed. + +Fixpoint trans_pred (p: pred_op) : + {fm: formula | forall a, + sat_predicate p a = true <-> satFormula fm a}. + refine + (match p with + | Pvar (b, p') => exist _ (((b, Pos.to_nat p') :: nil) :: nil) _ + | Ptrue => exist _ nil _ + | Pfalse => exist _ (nil::nil) _ + | Pand p1 p2 => + match trans_pred p1, trans_pred p2 with + | exist _ p1' _, exist _ p2' _ => exist _ (p1' ++ p2') _ + end + | Por p1 p2 => + match trans_pred p1, trans_pred p2 with + | exist _ p1' _, exist _ p2' _ => exist _ (mult p1' p2') _ + end + end); split; intros; simpl in *; auto; try solve [crush]. + - destruct b; auto. apply negb_true_iff in H. auto. + - destruct b. inv H. inv H0; auto. apply negb_true_iff. inv H. inv H0; eauto. contradiction. + - apply satFormula_concat. + apply andb_prop in H. inv H. apply i in H0. auto. + apply andb_prop in H. inv H. apply i0 in H1. auto. + - apply satFormula_concat2 in H. simplify. apply andb_true_intro. + split. apply i in H0. auto. + apply i0 in H1. auto. + - apply orb_prop in H. inv H; apply satFormula_mult. apply i in H0. auto. + apply i0 in H0. auto. + - apply orb_true_intro. + apply satFormula_mult2 in H. inv H. apply i in H0. auto. + apply i0 in H0. auto. +Defined. + +Definition sat_pred (p: pred_op) : + ({al : alist | sat_predicate p (interp_alist al) = true} + + {forall a : asgn, sat_predicate p a = false}). + refine + ( match trans_pred p with + | exist _ fm _ => + match satSolve fm with + | inleft (exist _ a _) => inleft (exist _ a _) + | inright _ => inright _ + end + end ). + - apply i in s0. auto. + - intros. specialize (n a). specialize (i a). + destruct (sat_predicate p a). exfalso. + apply n. apply i. auto. auto. +Defined. + +Definition sat_pred_simple (p: pred_op) := + match sat_pred p with + | inleft (exist _ al _) => Some al + | inright _ => None + end. + +#[local] Open Scope pred_op. + +Fixpoint negate (p: pred_op) := + match p with + | Pvar (b, pr) => Pvar (negb b, pr) + | T => ⟂ + | ⟂ => T + | A ∧ B => negate A ∨ negate B + | A ∨ B => negate A ∧ negate B + end. + +Notation "¬ A" := (negate A) (at level 15) : pred_op. + +Lemma negate_correct : + forall h a, sat_predicate (negate h) a = negb (sat_predicate h a). +Proof. + induction h; crush. + - repeat destruct_match; subst; crush; symmetry; apply negb_involutive. + - rewrite negb_andb; crush. + - rewrite negb_orb; crush. +Qed. diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 8353452..51beedc 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -28,228 +28,10 @@ Require Import compcert.lib.Integers. Require Import compcert.lib.Maps. Require Import compcert.verilog.Op. -Require Import vericert.common.Vericertlib. -Require Import vericert.hls.Sat. - -Local Open Scope rtl. +Require Import Predicate. +Require Import Vericertlib. Definition node := positive. -Definition predicate := positive. - -Inductive pred_op : Type := -| Pvar: predicate -> pred_op -| Ptrue: pred_op -| Pfalse: pred_op -| Pnot: pred_op -> pred_op -| Pand: pred_op -> pred_op -> pred_op -| Por: pred_op -> pred_op -> pred_op. - -Declare Scope pred_op. - -Notation "A ∧ B" := (Pand A B) (at level 20) : pred_op. -Notation "A ∨ B" := (Por A B) (at level 25) : pred_op. -Notation "⟂" := (Pfalse) : pred_op. -Notation "'T'" := (Ptrue) : pred_op. -Notation "¬ A" := (Pnot A) (at level 15) : pred_op. - -Fixpoint sat_predicate (p: pred_op) (a: asgn) : bool := - match p with - | Pvar p' => a (Pos.to_nat p') - | Ptrue => true - | Pfalse => false - | Pnot p' => negb (sat_predicate p' a) - | Pand p1 p2 => sat_predicate p1 a && sat_predicate p2 a - | Por p1 p2 => sat_predicate p1 a || sat_predicate p2 a - end. - -Fixpoint mult {A: Type} (a b: list (list A)) : list (list A) := - match a with - | nil => nil - | l :: ls => mult ls b ++ (List.map (fun x => l ++ x) b) - end. - -Lemma satFormula_concat: - forall a b agn, - satFormula a agn -> - satFormula b agn -> - satFormula (a ++ b) agn. -Proof. induction a; crush. Qed. - -Lemma satFormula_concat2: - forall a b agn, - satFormula (a ++ b) agn -> - satFormula a agn /\ satFormula b agn. -Proof. - induction a; simplify; - try apply IHa in H1; crush. -Qed. - -Lemma satClause_concat: - forall a a1 a0, - satClause a a1 -> - satClause (a0 ++ a) a1. -Proof. induction a0; crush. Qed. - -Lemma satClause_concat2: - forall a a1 a0, - satClause a0 a1 -> - satClause (a0 ++ a) a1. -Proof. - induction a0; crush. - inv H; crush. -Qed. - -Lemma satClause_concat3: - forall a b c, - satClause (a ++ b) c -> - satClause a c \/ satClause b c. -Proof. - induction a; crush. - inv H; crush. - apply IHa in H0; crush. - inv H0; crush. -Qed. - -Lemma satFormula_mult': - forall p2 a a0, - satFormula p2 a0 \/ satClause a a0 -> - satFormula (map (fun x : list lit => a ++ x) p2) a0. -Proof. - induction p2; crush. - - inv H. inv H0. apply satClause_concat. auto. - apply satClause_concat2; auto. - - apply IHp2. - inv H; crush; inv H0; crush. -Qed. - -Lemma satFormula_mult2': - forall p2 a a0, - satFormula (map (fun x : list lit => a ++ x) p2) a0 -> - satClause a a0 \/ satFormula p2 a0. -Proof. - induction p2; crush. - apply IHp2 in H1. inv H1; crush. - apply satClause_concat3 in H0. - inv H0; crush. -Qed. - -Lemma satFormula_mult: - forall p1 p2 a, - satFormula p1 a \/ satFormula p2 a -> - satFormula (mult p1 p2) a. -Proof. - induction p1; crush. - apply satFormula_concat; crush. - inv H. inv H0. - apply IHp1. auto. - apply IHp1. auto. - apply satFormula_mult'; - inv H; crush. -Qed. - -Lemma satFormula_mult2: - forall p1 p2 a, - satFormula (mult p1 p2) a -> - satFormula p1 a \/ satFormula p2 a. -Proof. - induction p1; crush. - apply satFormula_concat2 in H; crush. - apply IHp1 in H0. - inv H0; crush. - apply satFormula_mult2' in H1. inv H1; crush. -Qed. - -Fixpoint trans_pred (bound: nat) (p: pred_op) : - option {fm: formula | forall a, - sat_predicate p a = true <-> satFormula fm a}. - refine - (match bound with - | O => None - | S n => - match p with - | Pvar p' => Some (exist _ (((true, Pos.to_nat p') :: nil) :: nil) _) - | Ptrue => Some (exist _ nil _) - | Pfalse => Some (exist _ (nil::nil) _) - | Pand p1 p2 => - match trans_pred n p1, trans_pred n p2 with - | Some (exist _ p1' _), Some (exist _ p2' _) => - Some (exist _ (p1' ++ p2') _) - | _, _ => None - end - | Por p1 p2 => - match trans_pred n p1, trans_pred n p2 with - | Some (exist _ p1' _), Some (exist _ p2' _) => - Some (exist _ (mult p1' p2') _) - | _, _ => None - end - | Pnot (Pvar p') => Some (exist _ (((false, Pos.to_nat p') :: nil) :: nil) _) - | Pnot Ptrue => Some (exist _ (nil::nil) _) - | Pnot Pfalse => Some (exist _ nil _) - | Pnot (Pnot p') => - match trans_pred n p' with - | Some (exist _ p1' _) => Some (exist _ p1' _) - | None => None - end - | Pnot (Pand p1 p2) => - match trans_pred n (Por (Pnot p1) (Pnot p2)) with - | Some (exist _ p1' _) => Some (exist _ p1' _) - | None => None - end - | Pnot (Por p1 p2) => - match trans_pred n (Pand (Pnot p1) (Pnot p2)) with - | Some (exist _ p1' _) => Some (exist _ p1' _) - | None => None - end - end - end); split; intros; simpl in *; auto; try solve [crush]. - - inv H. inv H0; auto. - - split; auto. destruct (a (Pos.to_nat p')) eqn:?; crush. - - inv H. inv H0. unfold satLit in H. simplify. rewrite H. auto. - crush. - - rewrite negb_involutive in H. apply i in H. auto. - - rewrite negb_involutive. apply i; auto. - - rewrite negb_andb in H. apply i. auto. - - rewrite negb_andb. apply i. auto. - - rewrite negb_orb in H. apply i. auto. - - rewrite negb_orb. apply i. auto. - - apply satFormula_concat. - apply andb_prop in H. inv H. apply i in H0. auto. - apply andb_prop in H. inv H. apply i0 in H1. auto. - - apply satFormula_concat2 in H. simplify. apply andb_true_intro. - split. apply i in H0. auto. - apply i0 in H1. auto. - - apply orb_prop in H. inv H; apply satFormula_mult. apply i in H0. auto. - apply i0 in H0. auto. - - apply orb_true_intro. - apply satFormula_mult2 in H. inv H. apply i in H0. auto. - apply i0 in H0. auto. -Defined. - -Definition sat_pred (bound: nat) (p: pred_op) : - option ({al : alist | sat_predicate p (interp_alist al) = true} - + {forall a : asgn, sat_predicate p a = false}). - refine - ( match trans_pred bound p with - | Some (exist _ fm _) => - match boundedSat bound fm with - | Some (inleft (exist _ a _)) => Some (inleft (exist _ a _)) - | Some (inright _) => Some (inright _) - | None => None - end - | None => None - end ). - - apply i in s2. auto. - - intros. specialize (n a). specialize (i a). - destruct (sat_predicate p a). exfalso. - apply n. apply i. auto. auto. -Defined. - -Definition sat_pred_simple (bound: nat) (p: pred_op) := - match sat_pred bound p with - | Some (inleft (exist _ al _)) => Some (Some al) - | Some (inright _) => Some None - | None => None - end. Inductive instr : Type := | RBnop : instr @@ -320,10 +102,9 @@ Definition predset := PMap.t bool. Fixpoint eval_predf (pr: predset) (p: pred_op) {struct p} := match p with - | Pvar p' => PMap.get p' pr + | Pvar (b, p') => if b then PMap.get p' pr else negb (PMap.get p' pr) | Ptrue => true | Pfalse => false - | Pnot p' => negb (eval_predf pr p') | Pand p' p'' => (eval_predf pr p') && (eval_predf pr p'') | Por p' p'' => (eval_predf pr p') || (eval_predf pr p'') end. diff --git a/src/hls/Sat.v b/src/hls/Sat.v index e2bb5dc..b7596f6 100644 --- a/src/hls/Sat.v +++ b/src/hls/Sat.v @@ -10,10 +10,12 @@ Require Coq.MSets.MSetList. Require Import Coq.Structures.OrderedTypeEx. Require Import Coq.Structures.OrdersAlt. Require Import Coq.Program.Wf. +Require Import Vericertlib. Module Nat_OT := Update_OT Nat_as_OT. Module NSet := MSetList.Make Nat_OT. +#[local] Open Scope nat. (** * Problem Definition *) @@ -481,7 +483,7 @@ Definition lit_set_cl (cl: clause) := Definition lit_set (fm: formula) := fold_right NSet.union NSet.empty (map lit_set_cl fm). -Compute lit_set (((true, 1)::(true, 2)::(true, 1)::nil)::nil). +Compute NSet.cardinal (lit_set (((true, 1)::(true, 1)::(true, 1)::nil)::nil)). Definition sat_measure (fm: formula) := NSet.cardinal (lit_set fm). @@ -497,28 +499,71 @@ Proof. inversion H0. rewrite H1 in Heqs. discriminate. Qed. +Lemma sat_measure_setClause' : + forall cl cl' l A, + setClause cl l = inleft (exist _ cl' A) -> + ~ In (snd l) (map snd cl'). +Proof. + induction cl; intros. + { simpl in *. inv H. unfold not in *. intros. inv H. } + { simpl in H. + repeat (destruct_match; crush; []). destruct_match. + repeat (destruct_match; crush; []). inv H. eapply IHcl; eauto. + inv H. unfold not. intros. inv H. contradiction. eapply IHcl; eauto. + } +Qed. + +Lemma sat_measure_setClause'' : + forall cl cl' l A, + setClause cl l = inleft (exist _ cl' A) -> + forall l', + l' <> snd l -> + In l' (map snd cl) -> + In l' (map snd cl'). +Proof. + induction cl; intros. + { inversion H1. } + { inversion H1. subst. simpl in H. + repeat (destruct_match; crush; []). inv H. simpl. + inv H1. eauto. right. eapply IHcl; eauto. + simpl in H. repeat (destruct_match; crush; []). destruct_match. + repeat (destruct_match; crush; []). inv H. eapply IHcl; eauto. + inv H1; crush. inv H. simplify. auto. + inv H. simpl. right. eapply IHcl; eauto. + } +Qed. + +Lemma sat_measure_setClause : + forall cl cl' l A, + In (snd l) (map snd cl) -> + setClause cl l = inleft (exist _ cl' A) -> + NSet.cardinal (lit_set_cl cl') < NSet.cardinal (lit_set_cl cl). +Proof. + intros. pose proof H0. apply sat_measure_setClause' in H0. + pose proof (sat_measure_setClause'' _ _ _ _ H1). admit. +Admitted. + +Definition InFm l (fm: formula) := exists cl, In cl fm /\ In l cl. + +Lemma sat_measure_setFormula : + forall fm fm' l A, + InFm l fm -> + setFormula fm l = inleft (exist _ fm' A) -> + sat_measure fm' < sat_measure fm. +Proof. Admitted. + Lemma sat_measure_propagate_unit : - forall fm' fm l - (i: forall a : asgn, satFormula fm (upd a l) <-> satFormula fm' a) - (s: forall a : asgn, satFormula fm a -> satLit l a), - Some - (inleft - (existT - (fun fm' : formula => - {l : lit - | (forall a : asgn, satFormula fm a -> satLit l a) /\ - (forall a : asgn, satFormula fm (upd a l) <-> satFormula fm' a)}) fm' - (exist - (fun l : lit => - (forall a : asgn, satFormula fm a -> satLit l a) /\ - (forall a : asgn, satFormula fm (upd a l) <-> satFormula fm' a)) l - (conj s i)))) = unitPropagate fm -> + forall fm' fm H, + unitPropagate fm = Some (inleft (existT _ fm' H)) -> sat_measure fm' < sat_measure fm. Proof. - induction fm. - - intros. simpl in *. discriminate. - - intros. - Admitted. + induction fm; crush. + repeat (destruct_match; crush; []). + destruct_match. + repeat (destruct_match; crush; []). + inv Heqs1. + unfold sat_measure. + Admitted. Program Fixpoint satSolve (fm: formula) { measure (sat_measure fm) }: {al : alist | satFormula fm (interp_alist al)} + {forall a, ~satFormula fm a} := |