From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 12 Oct 2010 14:09:54 +0000 (+0000)
Subject: check last result in (get-assignment); some context cleanup
X-Git-Tag: cvc5-1.0.0~8810
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ec320b78deaaf31bdae1b8b048f66cfb1b3a4197;p=cvc5.git

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

diff --git a/src/context/cdo.h b/src/context/cdo.h
index ba4b368a8..f4c4a7e29 100644
--- 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 9a561abb6..053d5cb1a 100644
--- 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 3d6f304b5..594efcc35 100644
--- 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 fc2fa4522..62ddc74d0 100644
--- 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 "