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

7 files changed, 36 insertions, 0 deletions

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; }