portfolio merge

12 files changed, 35 insertions, 26 deletions

diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp
index 3b1f5f395..e74a250a3 100644
--- a/src/theory/arith/arith_priority_queue.cpp
+++ b/src/theory/arith/arith_priority_queue.cpp
@@ -191,12 +191,15 @@ void ArithPriorityQueue::transitionToDifferenceMode() {
 
   switch(d_pivotRule){
   case MINIMUM:
+    Debug("arith::pivotRule") << "Making the minimum heap." << endl;
     make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::minimumRule);
     break;
   case BREAK_TIES:
+    Debug("arith::pivotRule") << "Making the break ties heap." << endl;
     make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::breakTiesRules);
     break;
   case MAXIMUM:
+    Debug("arith::pivotRule") << "Making the maximum heap." << endl;
     make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::maximumRule);
     break;
   }
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 27fb0bb02..26cdb2cdb 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -619,9 +619,9 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){
   if(d_queue.empty()){
     return Node::null();
   }
-  static unsigned int instance = 0;
-  ++instance;
 
+  static CVC4_THREADLOCAL(unsigned int) instance = 0;
+  ++instance;
   Debug("arith::updateInconsistentVars") << "begin updateInconsistentVars() "
                                          << instance << endl;
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 64e713b0a..268829105 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1223,7 +1223,7 @@ void TheoryArith::presolve(){
 
   if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); }
 
-  static int callCount = 0;
+  static CVC4_THREADLOCAL(unsigned) callCount = 0;
   Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl;
 
   d_learner.clear();
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 9c69ec684..511982d48 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -29,7 +29,7 @@ namespace arith {
 class ArithConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType();
     return nodeManager->integerType();
   }
@@ -38,7 +38,7 @@ public:
 class ArithOperatorTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     TypeNode integerType = nodeManager->integerType();
     TypeNode realType = nodeManager->realType();
     TNode::iterator child_it = n.begin();
@@ -65,7 +65,7 @@ public:
 class ArithPredicateTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
       TypeNode integerType = nodeManager->integerType();
       TypeNode realType = nodeManager->realType();
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index bd3c8ad67..fd9e7cb2f 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -27,7 +27,7 @@ namespace arrays {
 
 struct ArraySelectTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate) {
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
     Assert(n.getKind() == kind::SELECT);
     TypeNode arrayType = n[0].getType(check);
     if( check ) {
@@ -45,7 +45,7 @@ struct ArraySelectTypeRule {
 
 struct ArrayStoreTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate) {
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
     Assert(n.getKind() == kind::STORE);
     TypeNode arrayType = n[0].getType(check);
     if( check ) {
diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
index e6c3e0f54..3b30b9f59 100644
--- a/src/theory/booleans/theory_bool_type_rules.h
+++ b/src/theory/booleans/theory_bool_type_rules.h
@@ -28,7 +28,7 @@ namespace boolean {
 class BooleanTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     TypeNode booleanType = nodeManager->booleanType();
     if( check ) {
       TNode::iterator child_it = n.begin();
@@ -49,7 +49,7 @@ public:
 class IteTypeRule {
   public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     TypeNode iteType = n[1].getType(check);
     if( check ) {
       TypeNode booleanType = nodeManager->booleanType();
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 86603f004..cd3e1437f 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -34,7 +34,7 @@ namespace builtin {
 class ApplyTypeRule {
   public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate) {
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
     TNode f = n.getOperator();
     TypeNode fType = f.getType(check);
     if( !fType.isFunction() && n.getNumChildren() > 0 ) {
@@ -72,7 +72,7 @@ class ApplyTypeRule {
 
 class EqualityTypeRule {
   public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) {
     TypeNode booleanType = nodeManager->booleanType();
 
     if( check ) {
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index a232ad33b..566bf3a68 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -84,7 +84,7 @@ RewriteResponse TheoryBVRewriter::postRewrite(TNode node) {
   return RewriteResponse(REWRITE_DONE, result);
 }
 
-AllRewriteRules* TheoryBVRewriter::s_allRules = NULL;
+CVC4_THREADLOCAL(AllRewriteRules*) TheoryBVRewriter::s_allRules = NULL;
 
 void TheoryBVRewriter::init() {
   s_allRules = new AllRewriteRules;
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 11a55ca61..f0eb621ca 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -32,7 +32,7 @@ struct AllRewriteRules;
 
 class TheoryBVRewriter {
 
-  static AllRewriteRules* s_allRules;
+  static CVC4_THREADLOCAL(AllRewriteRules*) s_allRules;
 
 public:
 
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 926ceb767..192295bc0 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -30,7 +30,7 @@ namespace bv {
 class BitVectorConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize());
   }
 };
@@ -38,7 +38,7 @@ public:
 class BitVectorCompRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
       TypeNode lhs = n[0].getType(check);
       TypeNode rhs = n[1].getType(check);
@@ -53,7 +53,7 @@ public:
 class BitVectorArithRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     unsigned maxWidth = 0;
     TNode::iterator it = n.begin();
     TNode::iterator it_end = n.end();
@@ -72,7 +72,7 @@ public:
 class BitVectorFixedWidthTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     TNode::iterator it = n.begin();
     TypeNode t = (*it).getType(check);
     if( check ) {
@@ -93,7 +93,7 @@ public:
 class BitVectorPredicateTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
       TypeNode lhsType = n[0].getType(check);
       if (!lhsType.isBitVector()) {
@@ -111,7 +111,7 @@ public:
 class BitVectorExtractTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     BitVectorExtract extractInfo = n.getOperator().getConst<BitVectorExtract>();
 
     // NOTE: We're throwing a type-checking exception here even
@@ -137,7 +137,7 @@ public:
 class BitVectorConcatRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     unsigned size = 0;
     TNode::iterator it = n.begin();
     TNode::iterator it_end = n.end();
@@ -158,7 +158,7 @@ public:
 class BitVectorRepeatTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     TypeNode t = n[0].getType(check);
     // NOTE: We're throwing a type-checking exception here even
     // when check is false, bc if the argument isn't a bit-vector
@@ -174,7 +174,7 @@ public:
 class BitVectorExtendTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     TypeNode t = n[0].getType(check);
     // NOTE: We're throwing a type-checking exception here even
     // when check is false, bc if the argument isn't a bit-vector
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 147fb868e..6385d1467 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -364,6 +364,12 @@ class TheoryEngine {
                        << std::endl
                        << QueryCommand(node.toExpr()) << std::endl;
     }
+
+    // Share with other portfolio threads
+    if(Options::current()->lemmaOutputChannel != NULL) {
+      Options::current()->lemmaOutputChannel->notifyNewLemma(node.toExpr());
+    }
+
     // Remove the ITEs and assert to prop engine
     std::vector<Node> additionalLemmas;
     additionalLemmas.push_back(node);
@@ -514,13 +520,13 @@ public:
   void staticLearning(TNode in, NodeBuilder<>& learned);
 
   /**
-   * Calls presolve() on all active theories and returns true
+   * Calls presolve() on all theories and returns true
    * if one of the theories discovers a conflict.
    */
   bool presolve();
 
    /**
-   * Calls postsolve() on all active theories.
+   * Calls postsolve() on all theories.
    */
   void postsolve();
 
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 927a31e01..9b622bc15 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -28,7 +28,7 @@ namespace uf {
 class UfTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     TNode f = n.getOperator();
     TypeNode fType = f.getType(check);
     if( !fType.isFunction() ) {