diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/arith_priority_queue.cpp | 3 | ||||
-rw-r--r-- | src/theory/arith/simplex.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_type_rules.h | 6 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_type_rules.h | 4 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool_type_rules.h | 4 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_type_rules.h | 18 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 10 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_type_rules.h | 2 |
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() ) { |