diff options
author | Paul Meng <baolmeng@gmail.com> | 2016-10-11 13:54:20 -0500 |
---|---|---|
committer | Paul Meng <baolmeng@gmail.com> | 2016-10-11 13:54:20 -0500 |
commit | 3395c5c13cd61d98aec0d9806e3b9bc3d707968a (patch) | |
tree | 0eadad9799862ec77d29f7abe03a46c300d80de8 /src/theory/bv | |
parent | 773e7d27d606b71ff0f78e84efe1deef2653f016 (diff) | |
parent | 5f415d4585134612bc24e9a823289fee35541a01 (diff) |
Merge branch 'origin' of https://github.com/CVC4/CVC4.git
Conflicts:
src/options/quantifiers_options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bv_inequality_graph.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_type_rules.h | 204 |
3 files changed, 109 insertions, 101 deletions
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 452172586..923e1d8c5 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -242,7 +242,7 @@ public: */ bool addDisequality(TNode a, TNode b, TNode reason); void getConflict(std::vector<TNode>& conflict); - virtual ~InequalityGraph() throw(AssertionException) {} + virtual ~InequalityGraph() {} /** * Check that the currently asserted disequalities that have not been split on * are still true in the current model. diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index f0981044b..de596e3d5 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -100,8 +100,10 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, d_subtheoryMap[SUB_BITBLAST] = bb_solver; } - TheoryBV::~TheoryBV() { + if (d_eagerSolver) { + delete d_eagerSolver; + } for (unsigned i = 0; i < d_subtheories.size(); ++i) { delete d_subtheories[i]; } diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index b531129f7..cafa7044a 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -26,9 +26,9 @@ namespace theory { namespace bv { class BitVectorConstantTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { if (check) { if (n.getConst<BitVector>().getSize() == 0) { throw TypeCheckingExceptionPrivate(n, "constant of size 0"); @@ -36,14 +36,13 @@ public: } return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize()); } -};/* class BitVectorConstantTypeRule */ +}; /* class BitVectorConstantTypeRule */ class BitVectorBitOfTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { - - if(check) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { + if (check) { BitVectorBitOf info = n.getOperator().getConst<BitVectorBitOf>(); TypeNode t = n[0].getType(check); @@ -51,72 +50,76 @@ public: throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } if (info.bitIndex >= t.getBitVectorSize()) { - throw TypeCheckingExceptionPrivate(n, "extract index is larger than the bitvector size"); + throw TypeCheckingExceptionPrivate( + n, "extract index is larger than the bitvector size"); } } return nodeManager->booleanType(); } -};/* class BitVectorBitOfTypeRule */ +}; /* class BitVectorBitOfTypeRule */ class BitVectorCompTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - if( check ) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { + if (check) { TypeNode lhs = n[0].getType(check); TypeNode rhs = n[1].getType(check); if (!lhs.isBitVector() || lhs != rhs) { - throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width"); + throw TypeCheckingExceptionPrivate( + n, "expecting bit-vector terms of the same width"); } } return nodeManager->mkBitVectorType(1); } -};/* class BitVectorCompTypeRule */ +}; /* class BitVectorCompTypeRule */ class BitVectorFixedWidthTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { TNode::iterator it = n.begin(); TypeNode t = (*it).getType(check); - if( check ) { + if (check) { if (!t.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); } TNode::iterator it_end = n.end(); - for (++ it; it != it_end; ++ it) { + for (++it; it != it_end; ++it) { if ((*it).getType(check) != t) { - throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width"); + throw TypeCheckingExceptionPrivate( + n, "expecting bit-vector terms of the same width"); } } } return t; } -};/* class BitVectorFixedWidthTypeRule */ +}; /* class BitVectorFixedWidthTypeRule */ class BitVectorPredicateTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - if( check ) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { + if (check) { TypeNode lhsType = n[0].getType(check); if (!lhsType.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); } TypeNode rhsType = n[1].getType(check); if (lhsType != rhsType) { - throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width"); + throw TypeCheckingExceptionPrivate( + n, "expecting bit-vector terms of the same width"); } } return nodeManager->booleanType(); } -};/* class BitVectorPredicateTypeRule */ +}; /* class BitVectorPredicateTypeRule */ class BitVectorUnaryPredicateTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - if( check ) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { + if (check) { TypeNode type = n[0].getType(check); if (!type.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); @@ -124,13 +127,13 @@ public: } return nodeManager->booleanType(); } -};/* class BitVectorUnaryPredicateTypeRule */ +}; /* class BitVectorUnaryPredicateTypeRule */ class BitVectorEagerAtomTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - if( check ) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { + if (check) { TypeNode lhsType = n[0].getType(check); if (!lhsType.isBoolean()) { throw TypeCheckingExceptionPrivate(n, "expecting boolean term"); @@ -138,96 +141,98 @@ public: } return nodeManager->booleanType(); } -};/* class BitVectorEagerAtomTypeRule */ +}; /* class BitVectorEagerAtomTypeRule */ class BitVectorAckermanizationUdivTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { TypeNode lhsType = n[0].getType(check); - if( check ) { + if (check) { if (!lhsType.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } } return lhsType; } -};/* class BitVectorAckermanizationUdivTypeRule */ +}; /* class BitVectorAckermanizationUdivTypeRule */ class BitVectorAckermanizationUremTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { TypeNode lhsType = n[0].getType(check); - if( check ) { + if (check) { if (!lhsType.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } } return lhsType; } -};/* class BitVectorAckermanizationUremTypeRule */ +}; /* class BitVectorAckermanizationUremTypeRule */ class BitVectorExtractTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { BitVectorExtract extractInfo = n.getOperator().getConst<BitVectorExtract>(); // NOTE: We're throwing a type-checking exception here even // if check is false, bc if we allow high < low the resulting // type will be illegal if (extractInfo.high < extractInfo.low) { - throw TypeCheckingExceptionPrivate(n, "high extract index is smaller than the low extract index"); + throw TypeCheckingExceptionPrivate( + n, "high extract index is smaller than the low extract index"); } - if( check ) { + if (check) { TypeNode t = n[0].getType(check); if (!t.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } if (extractInfo.high >= t.getBitVectorSize()) { - throw TypeCheckingExceptionPrivate(n, "high extract index is bigger than the size of the bit-vector"); + throw TypeCheckingExceptionPrivate( + n, "high extract index is bigger than the size of the bit-vector"); } } return nodeManager->mkBitVectorType(extractInfo.high - extractInfo.low + 1); } -};/* class BitVectorExtractTypeRule */ +}; /* class BitVectorExtractTypeRule */ class BitVectorExtractOpTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { Assert(n.getKind() == kind::BITVECTOR_EXTRACT_OP); return nodeManager->builtinOperatorType(); } -};/* class BitVectorExtractOpTypeRule */ +}; /* class BitVectorExtractOpTypeRule */ class BitVectorConcatTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { unsigned size = 0; TNode::iterator it = n.begin(); TNode::iterator it_end = n.end(); - for (; it != it_end; ++ it) { - TypeNode t = (*it).getType(check); - // NOTE: We're throwing a type-checking exception here even - // when check is false, bc if we don't check that the arguments - // are bit-vectors the result type will be inaccurate - if (!t.isBitVector()) { - throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); - } - size += t.getBitVectorSize(); + for (; it != it_end; ++it) { + TypeNode t = (*it).getType(check); + // NOTE: We're throwing a type-checking exception here even + // when check is false, bc if we don't check that the arguments + // are bit-vectors the result type will be inaccurate + if (!t.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); + } + size += t.getBitVectorSize(); } return nodeManager->mkBitVectorType(size); } -};/* class BitVectorConcatTypeRule */ +}; /* class BitVectorConcatTypeRule */ class BitVectorRepeatTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { 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 @@ -238,12 +243,12 @@ public: unsigned repeatAmount = n.getOperator().getConst<BitVectorRepeat>(); return nodeManager->mkBitVectorType(repeatAmount * t.getBitVectorSize()); } -};/* class BitVectorRepeatTypeRule */ +}; /* class BitVectorRepeatTypeRule */ class BitVectorExtendTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { 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 @@ -251,27 +256,28 @@ public: if (!t.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } - unsigned extendAmount = n.getKind() == kind::BITVECTOR_SIGN_EXTEND ? - (unsigned) n.getOperator().getConst<BitVectorSignExtend>() : - (unsigned) n.getOperator().getConst<BitVectorZeroExtend>(); + unsigned extendAmount = + n.getKind() == kind::BITVECTOR_SIGN_EXTEND + ? (unsigned)n.getOperator().getConst<BitVectorSignExtend>() + : (unsigned)n.getOperator().getConst<BitVectorZeroExtend>(); return nodeManager->mkBitVectorType(extendAmount + t.getBitVectorSize()); } -};/* class BitVectorExtendTypeRule */ +}; /* class BitVectorExtendTypeRule */ class BitVectorConversionTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - if(n.getKind() == kind::BITVECTOR_TO_NAT) { - if(check && !n[0].getType(check).isBitVector()) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { + if (n.getKind() == kind::BITVECTOR_TO_NAT) { + if (check && !n[0].getType(check).isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } return nodeManager->integerType(); } - if(n.getKind() == kind::INT_TO_BITVECTOR) { + if (n.getKind() == kind::INT_TO_BITVECTOR) { size_t bvSize = n.getOperator().getConst<IntToBitVector>(); - if(check && !n[0].getType(check).isInteger()) { + if (check && !n[0].getType(check).isInteger()) { throw TypeCheckingExceptionPrivate(n, "expecting integer term"); } return nodeManager->mkBitVectorType(bvSize); @@ -279,24 +285,24 @@ public: InternalError("bv-conversion typerule invoked for non-bv-conversion kind"); } -};/* class BitVectorConversionTypeRule */ +}; /* class BitVectorConversionTypeRule */ class CardinalityComputer { -public: + public: inline static Cardinality computeCardinality(TypeNode type) { Assert(type.getKind() == kind::BITVECTOR_TYPE); unsigned size = type.getConst<BitVectorSize>(); - if(size == 0) { + if (size == 0) { return 0; } Integer i = Integer(2).pow(size); return i; } -};/* class CardinalityComputer */ +}; /* class CardinalityComputer */ -}/* CVC4::theory::bv namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} /* CVC4::theory::bv namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ #endif /* __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H */ |