check last result in (get-assignment); some context cleanup

diff --git a/src/context/cdo.h b/src/context/cdo.h
index ba4b368a83a646b40c7f2fd118bd4ab4e46a0752..f4c4a7e2901e8a8f58d9cc8c7dab684c54e543ec 100644 (file)
--- a/src/context/cdo.h
+++ b/src/context/cdo.h
@@ -143,10 +143,15 @@ public:
   const T& get() const { return d_data; }
 
   /**
-   * For convenience, define operator T to be the same as get().
+   * For convenience, define operator T() to be the same as get().
    */
   operator T() { return get(); }
 
+  /**
+   * For convenience, define operator const T() to be the same as get().
+   */
+  operator const T() const { return get(); }
+
   /**
    * For convenience, define operator= that takes an object of type T.
    */

diff --git a/src/context/context.h b/src/context/context.h
index 9a561abb67cf307116d815ef90da82d94d828499..053d5cb1a6abe9b0cd21ed1ea9697fb22c2f8b86 100644 (file)
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -246,6 +246,7 @@ public:
    * creation of new Scope objects in the current memory region.
    */
   static void* operator new(size_t size, ContextMemoryManager* pCMM) {
+    Trace("context_mm") << "Scope::new " << size << " in " << pCMM << std::endl;
     return pCMM->newData(size);
   }
 
@@ -329,12 +330,12 @@ public:
  *    memory, privately declare (but don't define) an operator
  *    new(size_t) and destructor (as currently in the Link class, in
  *    src/theory/uf/ecdata.h).
- * 
+ *
  * 2. For data structures that may or may not be allocated in context
  *    memory, and are designed to be that way (esp. if they contain
  *    ContextObj instances), they should be heavily documented --
  *    especially the destructor, since it _may_or_may_not_be_called_.
- * 
+ *
  * 3. There's also an issue for generic code -- some class Foo<T>
  *    might be allocated in context memory, and that might normally be
  *    fine, but if T is a ContextObj this requires certain care.
@@ -352,7 +353,7 @@ class ContextObj {
   /**
    * Pointer to Scope in which this object was last modified.
    */
-  Scope* d_pScope; 
+  Scope* d_pScope;
 
   /**
    * Pointer to most recent version of same ContextObj in a previous Scope
@@ -504,6 +505,7 @@ public:
    * to be done using the restore method.
    */
   static void* operator new(size_t size, ContextMemoryManager* pCMM) {
+    Trace("context_mm") << "Context::new " << size << " in " << pCMM << std::endl;
     return pCMM->newData(size);
   }
 

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3d6f304b55d2460f3a369b3db0047b8efe63ab17..594efcc35a7343731192fc7a9b1d1795c44ad9e1 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -88,8 +88,7 @@ public:
   /**
    * Pre-process an Node.  This is expected to be highly-variable,
    * with a lot of "source-level configurability" to add multiple
-   * passes over the Node.  TODO: may need to specify a LEVEL of
-   * preprocessing (certain contexts need more/less ?).
+   * passes over the Node.
    */
   static Node preprocess(SmtEngine& smt, TNode n)
     throw(NoSuchFunctionException, AssertionException);
@@ -488,7 +487,8 @@ Expr SmtEngine::getValue(const Expr& e)
       "Cannot get value when produce-models options is off.";
     throw ModalException(msg);
   }
-  if(d_status.asSatisfiabilityResult() != Result::SAT ||
+  if(d_status.isNull() ||
+     d_status.asSatisfiabilityResult() != Result::SAT ||
      d_haveAdditions) {
     const char* msg =
       "Cannot get value unless immediately proceded by SAT/INVALID response.";
@@ -548,8 +548,13 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
       "produce-assignments option is off.";
     throw ModalException(msg);
   }
-  // TODO also check that the last query was sat/unknown, without intervening
-  // assertions
+  if(d_status.isNull() ||
+     d_status.asSatisfiabilityResult() != Result::SAT ||
+     d_haveAdditions) {
+    const char* msg =
+      "Cannot get value unless immediately proceded by SAT/INVALID response.";
+    throw ModalException(msg);
+  }
 
   NodeManagerScope nms(d_nodeManager);
   vector<SExpr> sexprs;

diff --git a/src/util/result.h b/src/util/result.h
index fc2fa4522940aff61d2b3336509947e4d56bb20a..62ddc74d00a47bed14ea152e098a782850442ede 100644 (file)
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -122,6 +122,9 @@ public:
   bool isUnknown() const {
     return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN;
   }
+  bool isNull() const {
+    return d_which == TYPE_NONE;
+  }
   enum UnknownExplanation whyUnknown() const {
     AlwaysAssert( isUnknown(),
                   "This result is not unknown, so the reason for "