From e2d7bba73f52285475da813433c703d7df7ae44a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 27 Apr 2023 16:33:57 +0100 Subject: Update to Coq 8.17 and CompCert 3.12 --- src/hls/Sat.v | 104 ---------------------------------------------------------- 1 file changed, 104 deletions(-) (limited to 'src/hls/Sat.v') diff --git a/src/hls/Sat.v b/src/hls/Sat.v index 3924ce7..b5970da 100644 --- a/src/hls/Sat.v +++ b/src/hls/Sat.v @@ -372,110 +372,6 @@ Fixpoint interp_alist (al : alist) : asgn := | l :: al' => upd (interp_alist al') l end. -(** Here's the final definition! - - This implementation isn't ##quite## what you would expect, since it - takes an extra parameter expressing a search tree depth. Writing the function - without that parameter would be trickier when it came to proving termination. - In practice, you can just seed the bound with one plus the number of variables - in the input, but the function's return type still indicates a possibility for - a "time-out" by returning [None]. - *) -Definition boundedSat: forall (bound : nat) (fm : formula), - option ({al : alist | satFormula fm (interp_alist al)} - + {forall a, ~satFormula fm a}). - refine (fix boundedSat (bound : nat) (fm : formula) {struct bound} - : option ({al : alist | satFormula fm (interp_alist al)} - + {forall a, ~satFormula fm a}) := - match bound with - | O => None - | S bound' => - if isNil fm - then Some (inleft _ (exist _ nil _)) - else match unitPropagate fm with - | Some (inleft (existT _ fm' (exist _ l _))) => - match boundedSat bound' fm' with - | None => None - | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (l :: al) _)) - | Some (inright _) => Some (inright _ _) - end - | Some (inright _) => Some (inright _ _) - | None => - let l := chooseSplit fm in - match setFormula fm l with - | inleft (exist _ fm' _) => - match boundedSat bound' fm' with - | None => None - | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (l :: al) _)) - | Some (inright _) => - match setFormula fm (negate l) with - | inleft (exist _ fm' _) => - match boundedSat bound' fm' with - | None => None - | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (negate l :: al) _)) - | Some (inright _) => Some (inright _ _) - end - | inright _ => Some (inright _ _) - end - end - | inright _ => - match setFormula fm (negate l) with - | inleft (exist _ fm' _) => - match boundedSat bound' fm' with - | None => None - | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (negate l :: al) _)) - | Some (inright _) => Some (inright _ _) - end - | inright _ => Some (inright _ _) - end - end - end - end); simpl; intros; subst; intuition; try generalize dependent (interp_alist al). - firstorder. - firstorder. - firstorder. - firstorder. - assert (satFormula fm (upd a0 l)); firstorder. - assert (satFormula fm (upd a0 l)); firstorder. - firstorder. - firstorder. - firstorder. - firstorder. - firstorder. - firstorder. - firstorder. - firstorder. - firstorder. - firstorder. - destruct (satLit_dec l a); - [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder. - destruct (satLit_dec l a); - [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder. - destruct (satLit_dec l a); - [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder. - destruct (satLit_dec l a); - [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder. - destruct (satLit_dec l a); intuition eauto; - assert (satFormula fm (upd a l)); firstorder. - destruct (satLit_dec l a); intuition eauto; - assert (satFormula fm (upd a l)); firstorder. - firstorder. - firstorder. - destruct (satLit_dec l a); intuition eauto; - assert (satFormula fm (upd a (negate l))); firstorder. - destruct (satLit_dec l a); intuition eauto; - assert (satFormula fm (upd a (negate l))); firstorder. - destruct (satLit_dec l a); - [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder. -Defined. - -Definition boundedSatSimple (bound : nat) (fm : formula) := - match boundedSat bound fm with - | None => None - | Some (inleft (exist _ a _)) => Some (Some a) - | Some (inright _) => Some None - 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). -- cgit