diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-02-20 17:59:33 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-02-20 17:59:33 +0000 |
commit | 3d2b33d66998261f9369cccc098140f64bc8b417 (patch) | |
tree | 9176ad2684415f8fb95f75a5655e8b17dcdf9793 /src/theory/bv | |
parent | 92155f5e40ed2cf452dc5e2f618e7be6542293e8 (diff) |
portfolio merge
Diffstat (limited to 'src/theory/bv')
-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 |
3 files changed, 11 insertions, 11 deletions
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 |