diff options
Diffstat (limited to 'src/hls/Sat.v')
-rw-r--r-- | src/hls/Sat.v | 104 |
1 files changed, 0 insertions, 104 deletions
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 #<i>#quite#</i># 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). |