From 376a0a4916ace4924103fb8fff4757ace5eac327 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 28 Apr 2023 18:08:04 +0100 Subject: Update Sat.v names --- src/hls/Predicate.v | 126 +++++++-------- src/hls/Sat.v | 454 +++++++++++++++++++++++++--------------------------- 2 files changed, 280 insertions(+), 300 deletions(-) (limited to 'src') diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index 99f0ce5..d8de758 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -413,41 +413,41 @@ Fixpoint mult {A: Type} (a b: list (list A)) : list (list A) := | l :: ls => mult ls b ++ (List.map (fun x => l ++ x) b) end. -Lemma satFormula_concat: +Lemma sat_formula_concat: forall a b agn, - satFormula a agn -> - satFormula b agn -> - satFormula (a ++ b) agn. + sat_formula a agn -> + sat_formula b agn -> + sat_formula (a ++ b) agn. Proof. induction a; crush. Qed. -Lemma satFormula_concat2: +Lemma sat_formula_concat2: forall a b agn, - satFormula (a ++ b) agn -> - satFormula a agn /\ satFormula b agn. + sat_formula (a ++ b) agn -> + sat_formula a agn /\ sat_formula b agn. Proof. induction a; simplify; try apply IHa in H1; crush. Qed. -Lemma satClause_concat: +Lemma sat_clause_concat: forall a a1 a0, - satClause a a1 -> - satClause (a0 ++ a) a1. + sat_clause a a1 -> + sat_clause (a0 ++ a) a1. Proof. induction a0; crush. Qed. -Lemma satClause_concat2: +Lemma sat_clause_concat2: forall a a1 a0, - satClause a0 a1 -> - satClause (a0 ++ a) a1. + sat_clause a0 a1 -> + sat_clause (a0 ++ a) a1. Proof. induction a0; crush. inv H; crush. Qed. -Lemma satClause_concat3: +Lemma sat_clause_concat3: forall a b c, - satClause (a ++ b) c -> - satClause a c \/ satClause b c. + sat_clause (a ++ b) c -> + sat_clause a c \/ sat_clause b c. Proof. induction a; crush. inv H; crush. @@ -455,58 +455,58 @@ Proof. inv H0; crush. Qed. -Lemma satFormula_mult': +Lemma sat_formula_mult': forall p2 a a0, - satFormula p2 a0 \/ satClause a a0 -> - satFormula (map (fun x : list lit => a ++ x) p2) a0. + sat_formula p2 a0 \/ sat_clause a a0 -> + sat_formula (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. + - inv H. inv H0. apply sat_clause_concat. auto. + apply sat_clause_concat2; auto. - apply IHp2. inv H; crush; inv H0; crush. Qed. -Lemma satFormula_mult2': +Lemma sat_formula_mult2': forall p2 a a0, - satFormula (map (fun x : list lit => a ++ x) p2) a0 -> - satClause a a0 \/ satFormula p2 a0. + sat_formula (map (fun x : list lit => a ++ x) p2) a0 -> + sat_clause a a0 \/ sat_formula p2 a0. Proof. induction p2; crush. apply IHp2 in H1. inv H1; crush. - apply satClause_concat3 in H0. + apply sat_clause_concat3 in H0. inv H0; crush. Qed. -Lemma satFormula_mult: +Lemma sat_formula_mult: forall p1 p2 a, - satFormula p1 a \/ satFormula p2 a -> - satFormula (mult p1 p2) a. + sat_formula p1 a \/ sat_formula p2 a -> + sat_formula (mult p1 p2) a. Proof. induction p1; crush. - apply satFormula_concat; crush. + apply sat_formula_concat; crush. inv H. inv H0. apply IHp1. auto. apply IHp1. auto. - apply satFormula_mult'; + apply sat_formula_mult'; inv H; crush. Qed. -Lemma satFormula_mult2: +Lemma sat_formula_mult2: forall p1 p2 a, - satFormula (mult p1 p2) a -> - satFormula p1 a \/ satFormula p2 a. + sat_formula (mult p1 p2) a -> + sat_formula p1 a \/ sat_formula p2 a. Proof. induction p1; crush. - apply satFormula_concat2 in H; crush. + apply sat_formula_concat2 in H; crush. apply IHp1 in H0. inv H0; crush. - apply satFormula_mult2' in H1. inv H1; crush. + apply sat_formula_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}. + sat_predicate p a = true <-> sat_formula fm a}. refine (match p with | Plit (b, p') => exist _ (((b, p') :: nil) :: nil) _ @@ -523,16 +523,16 @@ Fixpoint trans_pred (p: pred_op) : 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 sat_formula_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. + - apply sat_formula_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 orb_prop in H. inv H; apply sat_formula_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 sat_formula_mult2 in H. inv H. apply i in H0. auto. apply i0 in H0. auto. Defined. @@ -568,21 +568,21 @@ Fixpoint xtseytin (next: positive) (p: pred_op) {struct p} : (positive * lit * f Lemma stseytin_and_correct : forall cur p1 p2 fm c, stseytin_and cur p1 p2 = fm -> - satLit cur c -> - satLit p1 c /\ satLit p2 c -> - satFormula fm c. + sat_lit cur c -> + sat_lit p1 c /\ sat_lit p2 c -> + sat_formula fm c. Proof. intros. unfold stseytin_and in *. rewrite <- H. - unfold satLit in *. destruct p1. destruct p2. destruct cur. - simpl in *|-. cbn. unfold satLit. cbn. crush. + unfold sat_lit in *. destruct p1. destruct p2. destruct cur. + simpl in *|-. cbn. unfold sat_lit. cbn. crush. Qed. Lemma stseytin_and_correct2 : forall cur p1 p2 fm c, stseytin_and cur p1 p2 = fm -> - satFormula fm c -> - satLit cur c <-> satLit p1 c /\ satLit p2 c. + sat_formula fm c -> + sat_lit cur c <-> sat_lit p1 c /\ sat_lit p2 c. Proof. intros. split. intros. inv H1. unfold stseytin_and in *. inv H0; try contradiction. Admitted. @@ -590,29 +590,29 @@ Proof. Lemma stseytin_or_correct : forall cur p1 p2 fm c, stseytin_or cur p1 p2 = fm -> - satLit cur c -> - satLit p1 c \/ satLit p2 c -> - satFormula fm c. + sat_lit cur c -> + sat_lit p1 c \/ sat_lit p2 c -> + sat_formula fm c. Proof. intros. unfold stseytin_or in *. rewrite <- H. inv H1. - unfold satLit in *. destruct p1. destruct p2. destruct cur. - simpl in *|-. cbn. unfold satLit. cbn. crush. - unfold satLit in *. destruct p1. destruct p2. destruct cur. - simpl in *|-. cbn. unfold satLit. cbn. crush. + unfold sat_lit in *. destruct p1. destruct p2. destruct cur. + simpl in *|-. cbn. unfold sat_lit. cbn. crush. + unfold sat_lit in *. destruct p1. destruct p2. destruct cur. + simpl in *|-. cbn. unfold sat_lit. cbn. crush. Qed. Lemma stseytin_or_correct2 : forall cur p1 p2 fm c, stseytin_or cur p1 p2 = fm -> - satFormula fm c -> - satLit cur c <-> satLit p1 c \/ satLit p2 c. + sat_formula fm c -> + sat_lit cur c <-> sat_lit p1 c \/ sat_lit p2 c. Proof. Admitted. Lemma xtseytin_correct : forall p next l n fm c, xtseytin next p = (n, l, fm) -> - sat_predicate p c = true <-> satFormula ((l::nil)::fm) c. + sat_predicate p c = true <-> sat_formula ((l::nil)::fm) c. Proof. induction p. - intros. simplify. destruct p. @@ -634,12 +634,12 @@ Proof. (* eapply IHp2 in Heqp1. apply Heqp1 in H2. apply Heqp in H1. inv H1. inv H2. assert - (satFormula + (sat_formula (((true, n1) :: bar l0 :: bar l1 :: nil) :: (bar (true, n1) :: l0 :: nil) :: (bar (true, n1) :: l1 :: nil) :: nil) c). eapply stseytin_and_correct. unfold stseytin_and. eauto. - unfold satLit. simpl. admit. + unfold sat_lit. simpl. admit. inv H; try contradiction. inv H1; try contradiction. eauto.*) Admitted. @@ -654,11 +654,11 @@ Fixpoint max_predicate (p: pred_op) : positive := Definition tseytin (p: pred_op) : {fm: formula | forall a, - sat_predicate p a = true <-> satFormula fm a}. + sat_predicate p a = true <-> sat_formula fm a}. refine ( (match xtseytin (max_predicate p + 1) p as X return xtseytin (max_predicate p + 1) p = X -> - {fm: formula | forall a, sat_predicate p a = true <-> satFormula fm a} + {fm: formula | forall a, sat_predicate p a = true <-> sat_formula fm a} with (m, n, fm) => fun H => exist _ ((n::nil) :: fm) _ end) (eq_refl (xtseytin (max_predicate p + 1) p))). intros. eapply xtseytin_correct; eauto. Defined. @@ -674,7 +674,7 @@ Definition sat_pred_tseytin (p: pred_op) : refine ( match tseytin p with | exist _ fm _ => - match satSolve fm with + match sat_solve fm with | inleft (exist _ a _) => inleft (exist _ a _) | inright _ => inright _ end @@ -697,7 +697,7 @@ Definition sat_pred (p: pred_op) : refine ( match trans_pred p with | exist _ fm _ => - match satSolve fm with + match sat_solve fm with | inleft (exist _ a _) => inleft (exist _ a _) | inright _ => inright _ end diff --git a/src/hls/Sat.v b/src/hls/Sat.v index ad3d325..1cc2d2c 100644 --- a/src/hls/Sat.v +++ b/src/hls/Sat.v @@ -1,9 +1,3 @@ -(** -##Interactive Computer Theorem -Proving#
# -CS294-9, Fall 2006#
# -UC Berkeley *) - Require Import Arith Bool List. Require Import Coq.funind.Recdef. Require Coq.MSets.MSetPositive. @@ -18,42 +12,40 @@ Module PSetProp := MSetProperties.OrdProperties(PSet). #[local] Open Scope positive. -(** * Problem Definition *) +(** * Verified SAT Solver -Definition var := positive. -(** We identify propositional variables with natural numbers. *) +This development was heavily inspired by the example of a Sat solver given in: +http://www.cs.berkeley.edu/~adamc/itp/. -Definition lit := (bool * var)%type. -(** A literal is a combination of a truth value and a variable. *) +First, some basic definitions, such as variables, literals, clauses and +formulas. In this development [positive] is used instead of [nat] because it +integrates better into CompCert itself. *) +Definition var := positive. +Definition lit := (bool * var)%type. Definition clause := list lit. -(** A clause is a list (disjunction) of literals. *) - Definition formula := list clause. -(** A formula is a list (conjunction) of clauses. *) + +(** The most general version of an assignment is a function mapping variables to +booleans. This provides a possible value for all variables that could exist. *) Definition asgn := var -> bool. -(** An assignment is a function from variables to their truth values. *) -Definition satLit (l : lit) (a : asgn) := +Definition sat_lit (l : lit) (a : asgn) := a (snd l) = fst l. -(** An assignment satisfies a literal if it maps it to true. *) -Fixpoint satClause (cl : clause) (a : asgn) {struct cl} : Prop := +Fixpoint sat_clause (cl : clause) (a : asgn) {struct cl} : Prop := match cl with | nil => False - | l :: cl' => satLit l a \/ satClause cl' a + | l :: cl' => sat_lit l a \/ sat_clause cl' a end. -(** An assignment satisfies a clause if it satisfies at least one of its - literals. - *) -Fixpoint satFormula (fm: formula) (a: asgn) {struct fm} : Prop := +(** An assignment satisfies a formula if it satisfies all of its clauses. *) +Fixpoint sat_formula (fm: formula) (a: asgn) {struct fm} : Prop := match fm with | nil => True - | cl :: fm' => satClause cl a /\ satFormula fm' a + | cl :: fm' => sat_clause cl a /\ sat_formula fm' a end. -(** An assignment satisfies a formula if it satisfies all of its clauses. *) (** * Subroutines *) @@ -62,7 +54,6 @@ Definition bool_eq_dec : forall (x y : bool), {x = y} + {x <> y}. decide equality. Defined. -(** You'll probably want to compare booleans for equality at some point. *) Definition boolpositive_eq_dec : forall (x y : (bool * positive)), {x = y} + {x <> y}. pose proof bool_eq_dec. pose proof peq. @@ -72,9 +63,10 @@ Defined. (** A literal and its negation can't be true simultaneously. *) Lemma contradictory_assignment : forall s l cl a, s <> fst l - -> satLit l a - -> satLit (s, snd l) a - -> satClause cl a. + -> sat_lit l a + -> sat_lit (s, snd l) a + -> sat_clause cl a. +Proof. intros. red in H0, H1. simpl in H1. @@ -93,61 +85,61 @@ Definition upd (a : asgn) (l : lit) : asgn := (** Some lemmas about [upd] *) -Lemma satLit_upd_eq : forall l a, - satLit l (upd a l). - unfold satLit, upd; simpl; intros. +Lemma sat_lit_upd_eq : forall l a, + sat_lit l (upd a l). + unfold sat_lit, upd; simpl; intros. destruct (peq (snd l) (snd l)); tauto. Qed. -#[local] Hint Resolve satLit_upd_eq : core. +#[local] Hint Resolve sat_lit_upd_eq : core. -Lemma satLit_upd_neq : forall v l s a, +Lemma sat_lit_upd_neq : forall v l s a, v <> snd l - -> satLit (s, v) (upd a l) - -> satLit (s, v) a. - unfold satLit, upd; simpl; intros. + -> sat_lit (s, v) (upd a l) + -> sat_lit (s, v) a. + unfold sat_lit, upd; simpl; intros. destruct (peq v (snd l)); tauto. Qed. -#[local] Hint Resolve satLit_upd_neq : core. +#[local] Hint Resolve sat_lit_upd_neq : core. -Lemma satLit_upd_neq2 : forall v l s a, +Lemma sat_lit_upd_neq2 : forall v l s a, v <> snd l - -> satLit (s, v) a - -> satLit (s, v) (upd a l). - unfold satLit, upd; simpl; intros. + -> sat_lit (s, v) a + -> sat_lit (s, v) (upd a l). + unfold sat_lit, upd; simpl; intros. destruct (peq v (snd l)); tauto. Qed. -#[local] Hint Resolve satLit_upd_neq2 : core. +#[local] Hint Resolve sat_lit_upd_neq2 : core. -Lemma satLit_contra : forall s l a cl, +Lemma sat_lit_contra : forall s l a cl, s <> fst l - -> satLit (s, snd l) (upd a l) - -> satClause cl a. - unfold satLit, upd; simpl; intros. + -> sat_lit (s, snd l) (upd a l) + -> sat_clause cl a. + unfold sat_lit, upd; simpl; intros. destruct (peq (snd l) (snd l)); intuition auto with *. Qed. -#[local] Hint Resolve satLit_contra : core. +#[local] Hint Resolve sat_lit_contra : core. Ltac magic_solver := simpl; intros; subst; intuition eauto; firstorder; match goal with - | [ H1 : satLit ?l ?a, H2 : satClause ?cl ?a |- _ ] => - assert (satClause cl (upd a l)); firstorder + | [ H1 : sat_lit ?l ?a, H2 : sat_clause ?cl ?a |- _ ] => + assert (sat_clause cl (upd a l)); firstorder end. -(** Strongly-specified function to update a clause to reflect the effect of making a particular - literal true. *) -Definition setClause : forall (cl : clause) (l : lit), +(** Strongly-specified function to update a clause to reflect the effect of + making a particular literal true. *) +Definition set_clause : forall (cl : clause) (l : lit), {cl' : clause | - forall a, satClause cl (upd a l) <-> satClause cl' a} - + {forall a, satLit l a -> satClause cl a}. - refine (fix setClause (cl: clause) (l: lit) {struct cl} := + forall a, sat_clause cl (upd a l) <-> sat_clause cl' a} + + {forall a, sat_lit l a -> sat_clause cl a}. + refine (fix set_clause (cl: clause) (l: lit) {struct cl} := match cl with | nil => inleft (exist _ nil _) | x :: xs => - match setClause xs l with + match set_clause xs l with | inright p => inright _ | inleft (exist _ cl' H) => match peq (snd x) (snd l), bool_eq_dec (fst x) (fst l) with @@ -156,38 +148,38 @@ Definition setClause : forall (cl : clause) (l : lit), | right neq, _ => inleft (exist _ (x :: cl') _) end end - end); clear setClause; try magic_solver. + end); clear set_clause; try magic_solver. - intros; simpl; left; apply injective_projections in bool_eq; subst; auto. - - split; intros. simpl in H0. inversion H0. eapply satLit_contra; eauto. + - split; intros. simpl in H0. inversion H0. eapply sat_lit_contra; eauto. destruct x; simpl in *; subst. auto. apply H. eauto. simpl. right. apply H; eauto. - split; intros; simpl in *. inversion H0. destruct x; simpl in *; subst. left. eauto. right. apply H. eauto. - inversion H0. left. apply satLit_upd_neq2. auto. auto. + inversion H0. left. apply sat_lit_upd_neq2. auto. auto. right. apply H. auto. Defined. (** For testing purposes, we define a weakly-specified function as a thin - wrapper around [setClause]. + wrapper around [set_clause]. *) -Definition setClauseSimple (cl : clause) (l : lit) := - match setClause cl l with +Definition set_clause_simple (cl : clause) (l : lit) := + match set_clause cl l with | inleft (exist _ cl' _) => Some cl' | inright _ => None end. -(*Eval compute in setClauseSimple ((false, 1%nat) :: nil) (true, 1%nat).*) -(*Eval compute in setClauseSimple nil (true, 0). -Eval compute in setClauseSimple ((true, 0) :: nil) (true, 0). -Eval compute in setClauseSimple ((true, 0) :: nil) (false, 0). -Eval compute in setClauseSimple ((true, 0) :: nil) (true, 1). -Eval compute in setClauseSimple ((true, 0) :: nil) (false, 1). -Eval compute in setClauseSimple ((true, 0) :: (true, 1) :: nil) (true, 1). -Eval compute in setClauseSimple ((true, 0) :: (true, 1) :: nil) (false, 1). -Eval compute in setClauseSimple ((true, 0) :: (false, 1) :: nil) (true, 1). -Eval compute in setClauseSimple ((true, 0) :: (false, 1) :: nil) (false, 1).*) +(*Eval compute in set_clause_simple ((false, 1%nat) :: nil) (true, 1%nat).*) +(*Eval compute in set_clause_simple nil (true, 0). +Eval compute in set_clause_simple ((true, 0) :: nil) (true, 0). +Eval compute in set_clause_simple ((true, 0) :: nil) (false, 0). +Eval compute in set_clause_simple ((true, 0) :: nil) (true, 1). +Eval compute in set_clause_simple ((true, 0) :: nil) (false, 1). +Eval compute in set_clause_simple ((true, 0) :: (true, 1) :: nil) (true, 1). +Eval compute in set_clause_simple ((true, 0) :: (true, 1) :: nil) (false, 1). +Eval compute in set_clause_simple ((true, 0) :: (false, 1) :: nil) (true, 1). +Eval compute in set_clause_simple ((true, 0) :: (false, 1) :: nil) (false, 1).*) (** It's useful to have this strongly-specified nilness check. *) Definition isNil : forall (A : Set) (ls : list A), {ls = nil} + {ls <> nil}. @@ -197,47 +189,47 @@ Arguments isNil [A]. (** Some more lemmas that I found helpful.... *) -Lemma satLit_idem_lit : forall l a l', - satLit l a - -> satLit l' a - -> satLit l' (upd a l). - unfold satLit, upd; simpl; intros. +Lemma sat_lit_idem_lit : forall l a l', + sat_lit l a + -> sat_lit l' a + -> sat_lit l' (upd a l). + unfold sat_lit, upd; simpl; intros. destruct (peq (snd l') (snd l)); congruence. Qed. -#[local] Hint Resolve satLit_idem_lit : core. +#[local] Hint Resolve sat_lit_idem_lit : core. -Lemma satLit_idem_clause : forall l a cl, - satLit l a - -> satClause cl a - -> satClause cl (upd a l). +Lemma sat_lit_idem_clause : forall l a cl, + sat_lit l a + -> sat_clause cl a + -> sat_clause cl (upd a l). induction cl; simpl; intuition. Qed. -#[local] Hint Resolve satLit_idem_clause : core. +#[local] Hint Resolve sat_lit_idem_clause : core. -Lemma satLit_idem_formula : forall l a fm, - satLit l a - -> satFormula fm a - -> satFormula fm (upd a l). +Lemma sat_lit_idem_formula : forall l a fm, + sat_lit l a + -> sat_formula fm a + -> sat_formula fm (upd a l). induction fm; simpl; intuition. Qed. -#[local] Hint Resolve satLit_idem_formula : core. +#[local] Hint Resolve sat_lit_idem_formula : core. (** Function that updates an entire formula to reflect setting a literal to true. *) -Definition setFormula : forall (fm : formula) (l : lit), +Definition set_formula : forall (fm : formula) (l : lit), {fm' : formula | - forall a, satFormula fm (upd a l) <-> satFormula fm' a} - + {forall a, satLit l a -> ~satFormula fm a}. - refine (fix setFormula (fm: formula) (l: lit) {struct fm} := + forall a, sat_formula fm (upd a l) <-> sat_formula fm' a} + + {forall a, sat_lit l a -> ~sat_formula fm a}. + refine (fix set_formula (fm: formula) (l: lit) {struct fm} := match fm with | nil => inleft (exist _ nil _) | cl' :: fm' => - match setFormula fm' l with + match set_formula fm' l with | inright p => inright _ | inleft (exist _ fm'' H) => - match setClause cl' l with + match set_clause cl' l with | inright H' => inleft (exist _ fm'' _) | inleft (exist _ cl'' _) => if isNil cl'' @@ -245,22 +237,22 @@ Definition setFormula : forall (fm : formula) (l : lit), else inleft (exist _ (cl'' :: fm'') _) end end - end); clear setFormula; magic_solver. + end); clear set_formula; magic_solver. Defined. -Definition setFormulaSimple (fm : formula) (l : lit) := - match setFormula fm l with +Definition set_formula_simple (fm : formula) (l : lit) := + match set_formula fm l with | inleft (exist _ fm' _) => Some fm' | inright _ => None end. -(* Eval compute in setFormulaSimple (((true, 1%nat) :: nil) :: ((false, 1%nat) :: nil) :: nil) (true, 1%nat). *) -(* Eval compute in setFormulaSimple nil (true, 0). *) -(* Eval compute in setFormulaSimple (((true, 0) :: nil) :: nil) (true, 0). *) -(* Eval compute in setFormulaSimple (((false, 0) :: nil) :: nil) (true, 0). *) -(* Eval compute in setFormulaSimple (((false, 1) :: nil) :: nil) (true, 0). *) -(* Eval compute in setFormulaSimple (((false, 1) :: (true, 0) :: nil) :: nil) (true, 0). *) -(* Eval compute in setFormulaSimple (((false, 1) :: (false, 0) :: nil) :: nil) (true, 0). *) +(* Eval compute in set_formula_simple (((true, 1%nat) :: nil) :: ((false, 1%nat) :: nil) :: nil) (true, 1%nat). *) +(* Eval compute in set_formula_simple nil (true, 0). *) +(* Eval compute in set_formula_simple (((true, 0) :: nil) :: nil) (true, 0). *) +(* Eval compute in set_formula_simple (((false, 0) :: nil) :: nil) (true, 0). *) +(* Eval compute in set_formula_simple (((false, 1) :: nil) :: nil) (true, 0). *) +(* Eval compute in set_formula_simple (((false, 1) :: (true, 0) :: nil) :: nil) (true, 0). *) +(* Eval compute in set_formula_simple (((false, 1) :: (false, 0) :: nil) :: nil) (true, 0). *) #[local] Hint Extern 1 False => discriminate : core. @@ -270,75 +262,78 @@ match goal with end : core. (** Code that either finds a unit clause in a formula or declares that there are none. *) -Definition findUnitClause : forall (fm: formula), +Definition find_unit_clause : forall (fm: formula), {l : lit | In (l :: nil) fm} + {forall l, ~In (l :: nil) fm}. - refine (fix findUnitClause (fm: formula) {struct fm} := + refine (fix find_unit_clause (fm: formula) {struct fm} := match fm with | nil => inright _ | (l :: nil) :: fm' => inleft (exist _ l _) | _ :: fm' => - match findUnitClause fm' with + match find_unit_clause fm' with | inleft (exist _ l _) => inleft (exist _ l _) | inright H => inright _ end end - ); clear findUnitClause; magic_solver. + ); clear find_unit_clause; magic_solver. Defined. (** The literal in a unit clause must always be true in a satisfying assignment. *) -Lemma unitClauseTrue : forall l a fm, +Lemma unit_clause_true : forall l a fm, In (l :: nil) fm - -> satFormula fm a - -> satLit l a. + -> sat_formula fm a + -> sat_lit l a. induction fm; intuition auto with *. inversion H. inversion H; subst; simpl in H0; intuition. apply IHfm; eauto. inv H0. eauto. Qed. -#[local] Hint Resolve unitClauseTrue : core. +#[local] Hint Resolve unit_clause_true : core. + +(** Unit propagation. The return type of [unit_propagate] signifies that three +results are possible: -(** Unit propagation. The return type of [unitPropagate] signifies that three results are possible: - [None]: There are no unit clauses. - [Some (inleft _)]: There is a unit clause, and here is a formula reflecting setting its literal to true. - [Some (inright _)]: There is a unit clause, and propagating it reveals that the formula is unsatisfiable. *) -Definition unitPropagate : forall (fm : formula), option (sigT (fun fm' : formula => - {l : lit | - (forall a, satFormula fm a -> satLit l a) - /\ forall a, satFormula fm (upd a l) <-> satFormula fm' a}) - + {forall a, ~satFormula fm a}). - refine (fix unitPropagate (fm: formula) {struct fm} := - match findUnitClause fm with +Definition unit_propagate : + forall (fm : formula), option (sigT (fun fm' : formula => + {l : lit | + (forall a, sat_formula fm a -> sat_lit l a) + /\ forall a, sat_formula fm (upd a l) <-> sat_formula fm' a}) + + {forall a, ~sat_formula fm a}). + refine (fix unit_propagate (fm: formula) {struct fm} := + match find_unit_clause fm with | inright H => None | inleft (exist _ l _) => - match setFormula fm l with + match set_formula fm l with | inright _ => Some (inright _) | inleft (exist _ fm' _) => Some (inleft (existT _ fm' (exist _ l _))) end end - ); clear unitPropagate; magic_solver. + ); clear unit_propagate; magic_solver. Defined. -Definition unitPropagateSimple (fm : formula) := - match unitPropagate fm with +Definition unit_propagate_simple (fm : formula) := + match unit_propagate fm with | None => None | Some (inleft (existT _ fm' (exist _ l _))) => Some (Some (fm', l)) | Some (inright _) => Some None end. -(*Eval compute in unitPropagateSimple (((true, 1%nat) :: nil) :: ((false, 1%nat) :: nil) :: nil). -Eval compute in unitPropagateSimple nil. -Eval compute in unitPropagateSimple (((true, 0) :: nil) :: nil). -Eval compute in unitPropagateSimple (((true, 0) :: nil) :: ((false, 0) :: nil) :: nil). -Eval compute in unitPropagateSimple (((true, 0) :: nil) :: ((false, 1) :: nil) :: nil). -Eval compute in unitPropagateSimple (((true, 0) :: nil) :: ((false, 0) :: (false, 1) :: nil) :: nil). -Eval compute in unitPropagateSimple (((false, 0) :: (false, 1) :: nil) :: ((true, 0) :: nil) :: nil).*) +(*Eval compute in unit_propagate_simple (((true, 1%nat) :: nil) :: ((false, 1%nat) :: nil) :: nil). +Eval compute in unit_propagate_simple nil. +Eval compute in unit_propagate_simple (((true, 0) :: nil) :: nil). +Eval compute in unit_propagate_simple (((true, 0) :: nil) :: ((false, 0) :: nil) :: nil). +Eval compute in unit_propagate_simple (((true, 0) :: nil) :: ((false, 1) :: nil) :: nil). +Eval compute in unit_propagate_simple (((true, 0) :: nil) :: ((false, 0) :: (false, 1) :: nil) :: nil). +Eval compute in unit_propagate_simple (((false, 0) :: (false, 1) :: nil) :: ((true, 0) :: nil) :: nil).*) (** * The SAT Solver *) @@ -346,7 +341,7 @@ Eval compute in unitPropagateSimple (((false, 0) :: (false, 1) :: nil) :: ((true (** This section defines a DPLL SAT solver in terms of the subroutines. *) (** An arbitrary heuristic to choose the next variable to split on *) -Definition chooseSplit (fm : formula) := +Definition choose_split (fm : formula) := match fm with | ((l :: _) :: _) => l | _ => (true, 1) @@ -354,12 +349,12 @@ Definition chooseSplit (fm : formula) := Definition negate (l : lit) := (negb (fst l), snd l). -#[local] Hint Unfold satFormula : core. +#[local] Hint Unfold sat_formula : core. -Lemma satLit_dec : forall l a, - {satLit l a} + {satLit (negate l) a}. +Lemma sat_lit_dec : forall l a, + {sat_lit l a} + {sat_lit (negate l) a}. destruct l. - unfold satLit; simpl; intro. + unfold sat_lit; simpl; intro. destruct b; destruct (a v); simpl; auto. Qed. @@ -372,14 +367,14 @@ Fixpoint interp_alist (al : alist) : asgn := | l :: al' => upd (interp_alist al') l end. -(*Eval compute in boundedSatSimple 100 nil. -Eval compute in boundedSatSimple 100 (((true, 1%nat) :: nil) :: ((false, 1%nat) :: nil) :: nil). -Eval compute in boundedSatSimple 100 (((true, 0) :: nil) :: nil). -Eval compute in boundedSatSimple 100 (((true, 0) :: nil) :: ((false, 0) :: nil) :: nil). -Eval compute in boundedSatSimple 100 (((true, 0) :: (false, 1) :: nil) :: ((true, 1) :: nil) :: nil). -Eval compute in boundedSatSimple 100 (((true, 0) :: (false, 1) :: nil) :: ((true, 1) :: (false, 0) :: nil) :: nil). -Eval compute in boundedSatSimple 100 (((true, 0) :: (false, 1) :: nil) :: ((false, 0) :: (false, 0) :: nil) :: ((true, 1) :: nil) :: nil). -Eval compute in boundedSatSimple 100 (((false, 0) :: (true, 1) :: nil) :: ((false, 1) :: (true, 0) :: nil) :: nil).*) +(*Eval compute in boundedSat_simple 100 nil. +Eval compute in boundedSat_simple 100 (((true, 1%nat) :: nil) :: ((false, 1%nat) :: nil) :: nil). +Eval compute in boundedSat_simple 100 (((true, 0) :: nil) :: nil). +Eval compute in boundedSat_simple 100 (((true, 0) :: nil) :: ((false, 0) :: nil) :: nil). +Eval compute in boundedSat_simple 100 (((true, 0) :: (false, 1) :: nil) :: ((true, 1) :: nil) :: nil). +Eval compute in boundedSat_simple 100 (((true, 0) :: (false, 1) :: nil) :: ((true, 1) :: (false, 0) :: nil) :: nil). +Eval compute in boundedSat_simple 100 (((true, 0) :: (false, 1) :: nil) :: ((false, 0) :: (false, 0) :: nil) :: ((true, 1) :: nil) :: nil). +Eval compute in boundedSat_simple 100 (((false, 0) :: (true, 1) :: nil) :: ((false, 1) :: (true, 0) :: nil) :: nil).*) Definition lit_set_cl (cl: clause) := fold_right PSet.add PSet.empty (map snd cl). @@ -430,10 +425,10 @@ Definition sat_measure_cl (cl: clause) := PSet.cardinal (lit_set_cl cl). Definition sat_measure (fm: formula) := PSet.cardinal (lit_set fm). Lemma elim_clause : - forall (cl: clause) l, In l cl -> exists H, setClause cl l = inright H. + forall (cl: clause) l, In l cl -> exists H, set_clause cl l = inright H. Proof. induction cl; intros; simpl in *; try contradiction. - destruct (setClause cl l) eqn:?; [|econstructor; eauto]. + destruct (set_clause cl l) eqn:?; [|econstructor; eauto]. destruct s. inversion H; subst. clear H. destruct (peq (snd l) (snd l)); [| contradiction]. destruct (bool_eq_dec (fst l) (fst l)); [| contradiction]. @@ -441,9 +436,9 @@ Proof. inversion H0. rewrite H1 in Heqs. discriminate. Qed. -Lemma sat_measure_setClause' : +Lemma sat_measure_set_clause' : forall cl cl' l A, - setClause cl l = inleft (exist _ cl' A) -> + set_clause cl l = inleft (exist _ cl' A) -> ~ In (snd l) (map snd cl'). Proof. induction cl; intros. @@ -454,9 +449,9 @@ Proof. inv H. unfold not. intros. inv H. contradiction. eapply IHcl; eauto. Qed. -Lemma sat_measure_setClause'' : +Lemma sat_measure_set_clause'' : forall cl cl' l A, - setClause cl l = inleft (exist _ cl' A) -> + set_clause cl l = inleft (exist _ cl' A) -> forall l', l' <> snd l -> In l' (map snd cl) -> @@ -476,28 +471,28 @@ Qed. Definition InFm l (fm: formula) := exists cl b, In cl fm /\ In (b, l) cl. -Lemma satFormulaHasEmpty : +Lemma sat_formulaHasEmpty : forall fm, In nil fm -> - forall a, ~ satFormula fm a. + forall a, ~ sat_formula fm a. Proof. induction fm; crush. unfold not; intros. inv H0. inv H; auto. eapply IHfm; eauto. Qed. -Lemma InFm_chooseSplit : +Lemma InFm_choose_split : forall l b c, - InFm (snd (chooseSplit ((l :: b) :: c))) ((l :: b) :: c). + InFm (snd (choose_split ((l :: b) :: c))) ((l :: b) :: c). Proof. simpl; intros. destruct l; cbn. exists ((b0, v) :: b). exists b0. split; constructor; auto. Qed. -Lemma InFm_negated_chooseSplit : +Lemma InFm_negated_choose_split : forall l b c, - InFm (snd (negate (chooseSplit ((l :: b) :: c)))) ((l :: b) :: c). + InFm (snd (negate (choose_split ((l :: b) :: c)))) ((l :: b) :: c). Proof. simpl; intros. destruct l; cbn. exists ((b0, v) :: b). exists b0. @@ -523,10 +518,10 @@ Definition hasNoNil : forall fm: formula, {In nil fm} + {~ In nil fm}. - apply in_cons; assumption. Defined. -Lemma sat_measure_setClause : +Lemma sat_measure_set_clause : forall cl cl' l b A, (forall b', ~ In (b', l) cl) -> - setClause cl (b, l) = inleft (exist _ cl' A) -> + set_clause cl (b, l) = inleft (exist _ cl' A) -> lit_set_cl cl = lit_set_cl cl'. Proof. induction cl; intros. @@ -559,10 +554,10 @@ Proof. now apply in_map. Qed. -Lemma sat_measure_setClause_In_neq : +Lemma sat_measure_set_clause_In_neq : forall cl cl' l v b A, In v (map snd cl) -> - setClause cl (b, l) = inleft (exist _ cl' A) -> + set_clause cl (b, l) = inleft (exist _ cl' A) -> v <> l -> In v (map snd cl'). Proof. @@ -581,10 +576,10 @@ Proof. contradiction. Qed. -Lemma sat_measure_setClause_In_rev : +Lemma sat_measure_set_clause_In_rev : forall cl cl' l v b A, In v (map snd cl') -> - setClause cl (b, l) = inleft (exist _ cl' A) -> + set_clause cl (b, l) = inleft (exist _ cl' A) -> In v (map snd cl). Proof. induction cl; intros. @@ -602,9 +597,9 @@ Proof. inv H; auto. contradiction. Qed. -Lemma sat_measure_setClause_In_neq2 : +Lemma sat_measure_set_clause_In_neq2 : forall cl cl' l b A, - setClause cl (b, l) = inleft (exist _ cl' A) -> + set_clause cl (b, l) = inleft (exist _ cl' A) -> ~ In l (map snd cl'). Proof. induction cl; intros. @@ -619,10 +614,10 @@ Proof. eapply IHcl; eauto. Qed. -Lemma sat_measure_setClause_In : +Lemma sat_measure_set_clause_In : forall cl cl' l b A, In l (map snd cl) -> - setClause cl (b, l) = inleft (exist _ cl' A) -> + set_clause cl (b, l) = inleft (exist _ cl' A) -> (sat_measure_cl cl' < sat_measure_cl cl)%nat. Proof. induction cl; intros. @@ -636,7 +631,7 @@ Proof. -- exploit IHcl; eauto; intros. unfold sat_measure_cl in *. cbn -[PSet.cardinal]. apply lit_set_cl_in_set in i0. rewrite PSetProp.P.add_cardinal_1; auto. - -- apply sat_measure_setClause in Heqs; [|now apply in_map_snd_forall]. + -- apply sat_measure_set_clause in Heqs; [|now apply in_map_snd_forall]. unfold sat_measure_cl in *. cbn -[PSet.cardinal]. setoid_rewrite Heqs. apply lit_set_cl_not_in_set in n0. @@ -652,7 +647,7 @@ Proof. destruct (in_dec peq v (map snd cl)); destruct (in_dec peq v (map snd x)). * apply lit_set_cl_in_set in i0. apply lit_set_cl_in_set in i1. repeat rewrite PSetProp.P.add_cardinal_1 by auto. auto. - * exploit sat_measure_setClause_In_neq. eapply i0. eauto. auto. intros. + * exploit sat_measure_set_clause_In_neq. eapply i0. eauto. auto. intros. contradiction. * apply lit_set_cl_in_set in i0. apply lit_set_cl_not_in_set in n0. rewrite PSetProp.P.add_cardinal_1 by auto. @@ -662,19 +657,6 @@ Proof. unfold lit_set_cl in *; lia. Qed. -(* Lemma sat_measure_setFormula : - forall cl cl' l b b' A, - In (b', l) cl -> - setClause cl (b, l) = inleft (exist _ cl' A) -> - (sat_measure_cl cl' < sat_measure_cl cl)%nat. -Proof. - induction cl; intros. - - crush. - - cbn in H0. repeat (destruct_match; try discriminate; []). - destruct_match. - + repeat (destruct_match; try discriminate; []). - inv H0. cbn [snd fst] in *.*) - Lemma InFm_dec: forall l fm, { InFm l fm } + { ~ InFm l fm }. Proof. @@ -741,7 +723,7 @@ Qed. Lemma lit_set_cl_eq : forall cl v b cl' A, In v (map snd cl) -> - setClause cl (b, v) = inleft (exist _ cl' A) -> + set_clause cl (b, v) = inleft (exist _ cl' A) -> PSet.Equal (lit_set_cl cl) (PSet.add v (lit_set_cl cl')). Proof. constructor; intros. @@ -749,31 +731,31 @@ Proof. + apply PSetProp.P.FM.add_1; auto. + apply PSetProp.P.FM.add_2. apply lit_set_cl_in_set2 in H1. apply lit_set_cl_in_set. - eapply sat_measure_setClause_In_neq; eauto. + eapply sat_measure_set_clause_In_neq; eauto. - apply PSet.add_spec in H1. inv H1. + apply lit_set_cl_in_set; auto. + apply lit_set_cl_in_set. apply lit_set_cl_in_set2 in H2. - eapply sat_measure_setClause_In_rev; eauto. + eapply sat_measure_set_clause_In_rev; eauto. Qed. Lemma lit_set_cl_neq : forall cl v b cl' A, ~ In v (map snd cl) -> - setClause cl (b, v) = inleft (exist _ cl' A) -> + set_clause cl (b, v) = inleft (exist _ cl' A) -> PSet.Equal (lit_set_cl cl) (lit_set_cl cl'). Proof. constructor; intros. - - erewrite <- sat_measure_setClause; eauto. + - erewrite <- sat_measure_set_clause; eauto. intros. unfold not; intros. apply H. replace v with (snd (b', v)) by auto; apply in_map; auto. - - erewrite sat_measure_setClause; eauto. + - erewrite sat_measure_set_clause; eauto. intros. unfold not; intros. apply H. replace v with (snd (b', v)) by auto; apply in_map; auto. Qed. -Lemma sat_measure_setFormula1 : +Lemma sat_measure_set_formula1 : forall fm fm' l b A, - setFormula fm (b, l) = inleft (exist _ fm' A) -> + set_formula fm (b, l) = inleft (exist _ fm' A) -> ~ InFm l fm'. Proof. induction fm. @@ -783,17 +765,17 @@ Proof. destruct_match; repeat (destruct_match; try discriminate; []); inv H. + eapply IHfm in Heqs. assert (~ In l (map snd x0)) - by (eapply sat_measure_setClause_In_neq2; eauto). + by (eapply sat_measure_set_clause_In_neq2; eauto). unfold not; intros. apply InFm_cons in H0. inv H0; auto. inv H1. apply H. replace l with (snd (x1, l)) by auto. apply in_map; auto. + eapply IHfm in Heqs. auto. Qed. -Lemma sat_measure_setFormula2 : +Lemma sat_measure_set_formula2 : forall fm fm' l v b A, InFm v fm' -> - setFormula fm (b, l) = inleft (exist _ fm' A) -> + set_formula fm (b, l) = inleft (exist _ fm' A) -> InFm v fm. Proof. induction fm. @@ -804,7 +786,7 @@ Proof. + apply InFm_cons in H. inv H. * destruct H0 as (b0 & H0). apply in_map with (f := snd) in H0. cbn in H0. - exploit sat_measure_setClause_In_rev; eauto; intros. + exploit sat_measure_set_clause_In_rev; eauto; intros. apply list_in_map_inv in H. destruct H as (c & H1 & H2). destruct c. inv H1. cbn. exists a. exists b1. intuition auto with *. * exploit IHfm; eauto; intros. eapply InFm_cons2; tauto. @@ -813,73 +795,73 @@ Proof. all: exact true. Qed. -Lemma sat_measure_setFormula3 : +Lemma sat_measure_set_formula3 : forall fm fm' l b A, - setFormula fm (b, l) = inleft (exist _ fm' A) -> + set_formula fm (b, l) = inleft (exist _ fm' A) -> PSet.Subset (lit_set fm') (lit_set fm). Proof. unfold PSet.Subset; intros. apply lit_set_in_set. apply lit_set_in_set2 in H0. - eapply sat_measure_setFormula2; eauto. + eapply sat_measure_set_formula2; eauto. Qed. -Lemma sat_measure_setFormula : +Lemma sat_measure_set_formula : forall fm fm' l b A, InFm l fm -> - setFormula fm (b, l) = inleft (exist _ fm' A) -> + set_formula fm (b, l) = inleft (exist _ fm' A) -> (sat_measure fm' < sat_measure fm)%nat. Proof. intros. unfold sat_measure. apply PSetProp.P.subset_cardinal_lt with (x:=l). - eapply sat_measure_setFormula3; eauto. + eapply sat_measure_set_formula3; eauto. now apply lit_set_in_set. unfold not; intros. - eapply sat_measure_setFormula1. eauto. + eapply sat_measure_set_formula1. eauto. now apply lit_set_in_set2 in H1. Qed. Lemma sat_measure_propagate_unit : forall fm' fm H, - unitPropagate fm = Some (inleft (existT _ fm' H)) -> + unit_propagate fm = Some (inleft (existT _ fm' H)) -> (sat_measure fm' < sat_measure fm)%nat. Proof. - unfold unitPropagate; intros. cbn in *. + unfold unit_propagate; intros. cbn in *. destruct fm; intros. crush. repeat (destruct_match; try discriminate; []). inv H0. destruct x. - eapply sat_measure_setFormula; eauto. + eapply sat_measure_set_formula; eauto. cbn in i. clear Heqs. clear H3. inv i. eexists. exists b. split. constructor. auto. now constructor. exists ((b, v) :: nil). exists b. split. apply in_cons. auto. now constructor. Qed. -Program Fixpoint satSolve (fm: formula) { measure (sat_measure fm) }: - {al : alist | satFormula fm (interp_alist al)} + {forall a, ~satFormula fm a} := +Program Fixpoint sat_solve (fm: formula) { measure (sat_measure fm) }: + {al : alist | sat_formula fm (interp_alist al)} + {forall a, ~sat_formula fm a} := match isNil fm with | left fmIsNil => inleft _ (exist _ nil _) | right fmIsNotNil => match hasNoNil fm with | left hasNilfm => inright _ _ | right hasNoNilfm => - match unitPropagate fm with + match unit_propagate fm with | Some (inleft (existT _ fm' (exist _ l _))) => - match satSolve fm' with + match sat_solve fm' with | inleft (exist _ al _) => inleft _ (exist _ (l :: al) _) | inright _ => inright _ _ end | Some (inright _) => inright _ _ | None => - let l := chooseSplit fm in - match setFormula fm l with + let l := choose_split fm in + match set_formula fm l with | inleft (exist _ fm' _) => - match satSolve fm' with + match sat_solve fm' with | inleft (exist _ al _) => inleft _ (exist _ (l :: al) _) | inright _ => - match setFormula fm (negate l) with + match set_formula fm (negate l) with | inleft (exist _ fm' _) => - match satSolve fm' with + match sat_solve fm' with | inleft (exist _ al _) => inleft _ (exist _ (negate l :: al) _) | inright _ => inright _ _ end @@ -887,9 +869,9 @@ Program Fixpoint satSolve (fm: formula) { measure (sat_measure fm) }: end end | inright _ => - match setFormula fm (negate l) with + match set_formula fm (negate l) with | inleft (exist _ fm' _) => - match satSolve fm' with + match sat_solve fm' with | inleft (exist _ al _) => inleft _ (exist _ (negate l :: al) _) | inright _ => inright _ _ end @@ -900,7 +882,7 @@ Program Fixpoint satSolve (fm: formula) { measure (sat_measure fm) }: end end. Next Obligation. - apply satFormulaHasEmpty; assumption. Defined. + apply sat_formulaHasEmpty; assumption. Defined. Next Obligation. eapply sat_measure_propagate_unit; eauto. Defined. Next Obligation. @@ -909,63 +891,61 @@ Next Obligation. unfold not; intros; eapply wildcard'; apply i; eauto. Defined. Next Obligation. intros. symmetry in Heq_anonymous. - destruct (chooseSplit fm) eqn:?. - apply sat_measure_setFormula in Heq_anonymous; auto. unfold isNil in *. + destruct (choose_split fm) eqn:?. + apply sat_measure_set_formula in Heq_anonymous; auto. unfold isNil in *. destruct fm; try discriminate. assert (c <> nil). { unfold not; intros. apply hasNoNilfm. constructor; auto. } destruct c; try discriminate. replace p with (snd (b, p)) by auto. rewrite <- Heqp. - apply InFm_chooseSplit. Defined. + apply InFm_choose_split. Defined. Next Obligation. apply wildcard'0; auto. Defined. Next Obligation. - eapply sat_measure_setFormula; eauto. + eapply sat_measure_set_formula; eauto. destruct fm; try discriminate. destruct c; try discriminate. - apply InFm_chooseSplit. Defined. + apply InFm_choose_split. Defined. Next Obligation. apply wildcard'2; auto. Defined. Next Obligation. unfold not in *; intros. - destruct (satLit_dec (chooseSplit fm) a); - [assert (satFormula fm (upd a (chooseSplit fm))) - | assert (satFormula fm (upd a (negate (chooseSplit fm))))]; auto. + destruct (sat_lit_dec (choose_split fm) a); + [assert (sat_formula fm (upd a (choose_split fm))) + | assert (sat_formula fm (upd a (negate (choose_split fm))))]; auto. { eapply wildcard'1. apply wildcard'0; eauto. } { eapply wildcard'. apply wildcard'2; eauto. } Defined. Next Obligation. unfold not in *; intros. - destruct (satLit_dec (chooseSplit fm) a); - [assert (satFormula fm (upd a (chooseSplit fm))) - | assert (satFormula fm (upd a (negate (chooseSplit fm))))]; auto. + destruct (sat_lit_dec (choose_split fm) a); + [assert (sat_formula fm (upd a (choose_split fm))) + | assert (sat_formula fm (upd a (negate (choose_split fm))))]; auto. { eapply wildcard'1. eapply wildcard'0. eauto. } { eapply wildcard'; eauto. } Defined. Next Obligation. - eapply sat_measure_setFormula; eauto. + eapply sat_measure_set_formula; eauto. destruct fm; try discriminate. destruct c; try discriminate. - apply InFm_chooseSplit. Defined. + apply InFm_choose_split. Defined. Next Obligation. apply wildcard'1; auto. Defined. Next Obligation. unfold not in *; intros. - destruct (satLit_dec (chooseSplit fm) a); - [assert (satFormula fm (upd a (chooseSplit fm))) - | assert (satFormula fm (upd a (negate (chooseSplit fm))))]; auto. + destruct (sat_lit_dec (choose_split fm) a); + [assert (sat_formula fm (upd a (choose_split fm))) + | assert (sat_formula fm (upd a (negate (choose_split fm))))]; auto. { eapply wildcard'0; eauto. } { eapply wildcard'; apply wildcard'1; eauto. } Defined. Next Obligation. unfold not in *; intros. - destruct (satLit_dec (chooseSplit fm) a). + destruct (sat_lit_dec (choose_split fm) a). { eapply wildcard'0; eauto. } { eapply wildcard'; eauto. } Defined. -Definition satSolveSimple (fm : formula) := - match satSolve fm with +Definition sat_solve_simple (fm : formula) := + match sat_solve fm with | inleft (exist _ a _) => Some a | inright _ => None end. - -(* Eval compute in satSolveSimple nil. *) -- cgit