From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 31 Jul 2012 21:44:22 +0000 (+0000)
Subject: fixes for portfolio
X-Git-Tag: cvc5-1.0.0~7903
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c90b1b66e6c8e3b77f2b73b73208f120445e5f91;p=cvc5.git

fixes for portfolio
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0acc53693..272bfe04e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -345,7 +345,6 @@ void SmtEngine::finishInit() {
 
   d_theoryEngine->setPropEngine(d_propEngine);
   d_theoryEngine->setDecisionEngine(d_decisionEngine);
-
 }
 
 void SmtEngine::finalOptionsAreSet() {
@@ -353,8 +352,8 @@ void SmtEngine::finalOptionsAreSet() {
     return;
   }
 
-  finishInit();                 // finish initalization, creating prop
-                                // engine etc.
+  // finish initalization, creat the prop engine, etc.
+  finishInit();
 
   AlwaysAssert( d_propEngine->getAssertionLevel() == 0,
                 "The PropEngine has pushed but the SmtEngine "
@@ -1992,6 +1991,9 @@ void SmtEngine::internalPop() {
 }
 
 void SmtEngine::interrupt() throw(ModalException) {
+  if(!d_fullyInited) {
+    return;
+  }
   d_propEngine->interrupt();
 }
 
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index a91243343..988b2b327 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -30,7 +30,9 @@ static TheoryId theoryOf(TNode node) {
   return Theory::theoryOf(THEORY_OF_TYPE_BASED, node);
 }
 
-std::hash_set<Node, NodeHashFunction> d_rewriteStack;
+#ifdef CVC4_ASSERTIONS
+static CVC4_THREADLOCAL(std::hash_set<Node, NodeHashFunction>*) s_rewriteStack = NULL;
+#endif /* CVC4_ASSERTIONS */
 
 /**
  * TheoryEngine::rewrite() keeps a stack of things that are being pre-
@@ -72,6 +74,10 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
 
 #ifdef CVC4_ASSERTIONS
   bool isEquality = node.getKind() == kind::EQUAL;
+
+  if(s_rewriteStack == NULL) {
+    s_rewriteStack = new std::hash_set<Node, NodeHashFunction>();
+  }
 #endif
 
   Trace("rewriter") << "Rewriter::rewriteTo(" << theoryId << "," << node << ")"<< std::endl;
@@ -171,12 +177,12 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
           Assert(response.node != rewriteStackTop.node);
           //TODO: this is not thread-safe - should make this assertion dependent on sequential build
 #ifdef CVC4_ASSERTIONS
-          Assert(d_rewriteStack.find(response.node) == d_rewriteStack.end());
-          d_rewriteStack.insert(response.node);
+          Assert(s_rewriteStack->find(response.node) == s_rewriteStack->end());
+          s_rewriteStack->insert(response.node);
 #endif
           rewriteStackTop.node = rewriteTo(newTheoryId, response.node);
 #ifdef CVC4_ASSERTIONS
-          d_rewriteStack.erase(response.node);
+          s_rewriteStack->erase(response.node);
 #endif
           break;
         } else if (response.status == REWRITE_DONE) {