add isFinished() to type enumerators (so we don't rely on exception-throwing after...

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 59f66521c1ccf2646cb78e9f883e8327cf133e42..52a2e0c27f2d2012e94bef8c4d0d94ec66b7d91b 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -555,12 +555,9 @@ public:
    * Used as a predicate for options preprocessor.
    */
   static void beforeSearch(std::string option, bool value, SmtEngine* smt) throw(ModalException) {
-    // FIXME: should be the following test...
-    // if(smt != NULL && (smt->d_queryMade || smt->d_problemExtended)) {
-    // ...but addToModelType() etc. make a stronger assumption:
     if(smt != NULL && smt->d_fullyInited) {
       std::stringstream ss;
-      ss << "cannot change option `" << option << "' after assertions have been made";
+      ss << "cannot change option `" << option << "' after final initialization (i.e., after logic has been set)";
       throw ModalException(ss.str());
     }
   }

diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h
index e62baa2f679a3f593ec1b230a17b0a4d20758a30..4dd139be7a88f5d869db264d17f008bff9a37a59 100644 (file)
--- a/src/theory/arith/type_enumerator.h
+++ b/src/theory/arith/type_enumerator.h
@@ -72,6 +72,10 @@ public:
     return *this;
   }
 
+  bool isFinished() throw() {
+    return false;
+  }
+
 };/* class RationalEnumerator */
 
 class IntegerEnumerator : public TypeEnumeratorBase<IntegerEnumerator> {
@@ -100,6 +104,10 @@ public:
     return *this;
   }
 
+  bool isFinished() throw() {
+    return false;
+  }
+
 };/* class IntegerEnumerator */
 
 }/* CVC4::theory::arith namespace */

diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h
index e613fc6678f9b9fb73554cc6caa31577e33da2bc..f6d871c48f9f9834dcc232a210a19e469c1456fe 100644 (file)
--- a/src/theory/arrays/type_enumerator.h
+++ b/src/theory/arrays/type_enumerator.h
@@ -50,6 +50,10 @@ public:
     return *this;
   }
 
+  bool isFinished() throw() {
+    Unimplemented();
+  }
+
 };/* class ArrayEnumerator */
 
 }/* CVC4::theory::arrays namespace */

diff --git a/src/theory/booleans/type_enumerator.h b/src/theory/booleans/type_enumerator.h
index c83e79d75f940fe7cef9988815e8bdedb6b0fc80..66f76780552197f188d9b247c7583d9cfec04584 100644 (file)
--- a/src/theory/booleans/type_enumerator.h
+++ b/src/theory/booleans/type_enumerator.h
@@ -62,6 +62,10 @@ public:
     return *this;
   }
 
+  bool isFinished() throw() {
+    return d_value == DONE;
+  }
+
 };/* class BooleanEnumerator */
 
 }/* CVC4::theory::booleans namespace */

diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h
index c94ec73222aa8e7725ff2b7676cc5720ee47dd4c..4375cc50170e0a51e1f9626392a034f87f1ee129 100644 (file)
--- a/src/theory/builtin/type_enumerator.h
+++ b/src/theory/builtin/type_enumerator.h
@@ -51,6 +51,10 @@ public:
     return *this;
   }
 
+  bool isFinished() throw() {
+    return false;
+  }
+
 };/* class UninterpretedSortEnumerator */
 
 }/* CVC4::theory::builtin namespace */

diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h
index 746e77a0019f1ff22eb2a07e27830d199a3f3692..2f8f713f8e1432d5a375395c80e94b87b7265fb0 100644 (file)
--- a/src/theory/bv/type_enumerator.h
+++ b/src/theory/bv/type_enumerator.h
@@ -55,6 +55,10 @@ public:
     return *this;
   }
 
+  bool isFinished() throw() {
+    return d_bits != d_bits.modByPow2(d_size);
+  }
+
 };/* BitVectorEnumerator */
 
 }/* CVC4::theory::bv namespace */

diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 1776bf4cea72597d216e1df70e91d508a83c14ce..47691dd19c94ef77ba82a2009020a9fa0e5a230e 100644 (file)
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -143,6 +143,10 @@ public:
     return *this;
   }
 
+  bool isFinished() throw() {
+    return d_ctor >= d_datatype.getNumConstructors();
+  }
+
 };/* DatatypesEnumerator */
 
 }/* CVC4::theory::datatypes namespace */

diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h
index a03f1f35a2c5c89eece142b844f60c4bd99e2c3e..7b097ac77a783a954acfdabae0652c6182188cdd 100644 (file)
--- a/src/theory/type_enumerator.h
+++ b/src/theory/type_enumerator.h
@@ -47,12 +47,19 @@ public:
 
   virtual ~TypeEnumeratorInterface() {}
 
+  /** Is this enumerator out of constants to enumerate? */
+  virtual bool isFinished() throw() = 0;
+
+  /** Get the current constant of this type (throws if no such constant exists) */
   virtual Node operator*() throw(NoMoreValuesException) = 0;
 
+  /** Increment the pointer to the next available constant */
   virtual TypeEnumeratorInterface& operator++() throw() = 0;
 
+  /** Clone this enumerator */
   virtual TypeEnumeratorInterface* clone() const = 0;
 
+  /** Get the type from which we're enumerating constants */
   TypeNode getType() const throw() { return d_type; }
 
 };/* class TypeEnumeratorInterface */
@@ -92,6 +99,7 @@ public:
 
   ~TypeEnumerator() { delete d_te; }
 
+  bool isFinished() throw() { return d_te->isFinished(); }
   Node operator*() throw(NoMoreValuesException) { return **d_te; }
   TypeEnumerator& operator++() throw() { ++*d_te; return *this; }
   TypeEnumerator operator++(int) throw() { TypeEnumerator te = *this; ++*d_te; return te; }