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).