Add work towards decidability of SAT solver

7 files changed, 377 insertions, 279 deletions

diff --git a/docs b/docs
-Subproject 20ed00b92c1a5bf2806a27e9c85d90c6d265e5b
+Subproject 36abd86820f7521fcebb3b173acbcb6409b148b
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} :=