From 410688d57a92d5ff3505ad70c4573955e4075475 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 1 Aug 2012 22:33:13 +0000
Subject: add isFinished() to type enumerators (so we don't rely on
 exception-throwing after exhaustively enumerating finite types), also fix a
 standards-related FIXME in SmtEngine by clarifying the text of an error
 message

---
 src/smt/smt_engine.h                   | 5 +----
 src/theory/arith/type_enumerator.h     | 8 ++++++++
 src/theory/arrays/type_enumerator.h    | 4 ++++
 src/theory/booleans/type_enumerator.h  | 4 ++++
 src/theory/builtin/type_enumerator.h   | 4 ++++
 src/theory/bv/type_enumerator.h        | 4 ++++
 src/theory/datatypes/type_enumerator.h | 4 ++++
 src/theory/type_enumerator.h           | 8 ++++++++
 8 files changed, 37 insertions(+), 4 deletions(-)

(limited to 'src')

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 59f66521c..52a2e0c27 100644
--- 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 e62baa2f6..4dd139be7 100644
--- 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 e613fc667..f6d871c48 100644
--- 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 c83e79d75..66f767805 100644
--- 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 c94ec7322..4375cc501 100644
--- 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 746e77a00..2f8f713f8 100644
--- 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 1776bf4ce..47691dd19 100644
--- 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 a03f1f35a..7b097ac77 100644
--- 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; }
-- 
cgit v1.2.3