summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/bv/bitblast_strategies.cpp102
-rw-r--r--src/theory/bv/bitblaster.cpp10
-rw-r--r--src/theory/bv/bv_subtheory_bitblast.cpp4
-rw-r--r--src/theory/bv/bv_subtheory_eq.cpp4
-rw-r--r--src/theory/bv/cd_set_collection.h8
-rw-r--r--src/theory/bv/theory_bv.cpp20
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules.h6
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h46
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_core.h26
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_normalization.h36
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h38
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_simplification.h76
-rw-r--r--src/theory/bv/theory_bv_utils.h6
13 files changed, 188 insertions, 194 deletions
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index c25c40c22..a952b2929 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -191,13 +191,13 @@ Node inline sLessThanBB(const Bits&a, const Bits& b, bool orEqual) {
Node UndefinedAtomBBStrategy(TNode node, Bitblaster* bb) {
- BVDebug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: "
+ Debug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: "
<< node.getKind() << "\n";
Unreachable();
}
Node DefaultEqBB(TNode node, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
Assert(node.getKind() == kind::EQUAL);
Bits lhs, rhs;
@@ -219,7 +219,7 @@ Node DefaultEqBB(TNode node, Bitblaster* bb) {
Node AdderUltBB(TNode node, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
Assert(node.getKind() == kind::BITVECTOR_ULT);
Bits a, b;
bb->bbTerm(node[0], a);
@@ -241,7 +241,7 @@ Node AdderUltBB(TNode node, Bitblaster* bb) {
Node DefaultUltBB(TNode node, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
Assert(node.getKind() == kind::BITVECTOR_ULT);
Bits a, b;
bb->bbTerm(node[0], a);
@@ -254,7 +254,7 @@ Node DefaultUltBB(TNode node, Bitblaster* bb) {
}
Node DefaultUleBB(TNode node, Bitblaster* bb){
- BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
Assert(node.getKind() == kind::BITVECTOR_ULE);
Bits a, b;
@@ -267,31 +267,31 @@ Node DefaultUleBB(TNode node, Bitblaster* bb){
}
Node DefaultUgtBB(TNode node, Bitblaster* bb){
- BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
// should be rewritten
Unimplemented();
}
Node DefaultUgeBB(TNode node, Bitblaster* bb){
- BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
// should be rewritten
Unimplemented();
}
// Node DefaultSltBB(TNode node, Bitblaster* bb){
-// BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n";
+// Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
// // shoudl be rewritten in terms of ult
// Unimplemented();
// }
// Node DefaultSleBB(TNode node, Bitblaster* bb){
-// BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n";
+// Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
// // shoudl be rewritten in terms of ule
// Unimplemented();
// }
Node DefaultSltBB(TNode node, Bitblaster* bb){
- BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
Bits a, b;
bb->bbTerm(node[0], a);
@@ -303,7 +303,7 @@ Node DefaultSltBB(TNode node, Bitblaster* bb){
}
Node DefaultSleBB(TNode node, Bitblaster* bb){
- BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
Bits a, b;
bb->bbTerm(node[0], a);
@@ -315,13 +315,13 @@ Node DefaultSleBB(TNode node, Bitblaster* bb){
}
Node DefaultSgtBB(TNode node, Bitblaster* bb){
- BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
// should be rewritten
Unimplemented();
}
Node DefaultSgeBB(TNode node, Bitblaster* bb){
- BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
// should be rewritten
Unimplemented();
}
@@ -330,7 +330,7 @@ Node DefaultSgeBB(TNode node, Bitblaster* bb){
/// Term bitblasting strategies
void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: "
+ Debug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: "
<< node.getKind() << "\n";
Unreachable();
}
@@ -342,15 +342,15 @@ void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) {
}
if(Debug.isOn("bitvector-bb")) {
- BVDebug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting " << node << "\n";
- BVDebug("bitvector-bb") << " with bits " << toString(bits);
+ Debug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << " with bits " << toString(bits);
}
bb->storeVariable(node);
}
void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n";
Assert(node.getKind() == kind::CONST_BITVECTOR);
Assert(bits.size() == 0);
@@ -364,13 +364,13 @@ void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {
}
}
if(Debug.isOn("bitvector-bb")) {
- BVDebug("bitvector-bb") << "with bits: " << toString(bits) << "\n";
+ Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n";
}
}
void DefaultNotBB (TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n";
Assert(node.getKind() == kind::BITVECTOR_NOT);
Assert(bits.size() == 0);
Bits bv;
@@ -379,7 +379,7 @@ void DefaultNotBB (TNode node, Bits& bits, Bitblaster* bb) {
}
void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n";
Assert(bits.size() == 0);
Assert (node.getKind() == kind::BITVECTOR_CONCAT);
@@ -394,12 +394,12 @@ void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb) {
}
Assert (bits.size() == utils::getSize(node));
if(Debug.isOn("bitvector-bb")) {
- BVDebug("bitvector-bb") << "with bits: " << toString(bits) << "\n";
+ Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n";
}
}
void DefaultAndBB (TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n";
Assert(node.getKind() == kind::BITVECTOR_AND &&
bits.size() == 0);
@@ -417,7 +417,7 @@ void DefaultAndBB (TNode node, Bits& bits, Bitblaster* bb) {
}
void DefaultOrBB (TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n";
Assert(node.getKind() == kind::BITVECTOR_OR &&
bits.size() == 0);
@@ -435,7 +435,7 @@ void DefaultOrBB (TNode node, Bits& bits, Bitblaster* bb) {
}
void DefaultXorBB (TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n";
Assert(node.getKind() == kind::BITVECTOR_XOR &&
bits.size() == 0);
@@ -456,7 +456,7 @@ void DefaultXorBB (TNode node, Bits& bits, Bitblaster* bb) {
}
void DefaultXnorBB (TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n";
Assert(node.getNumChildren() == 2 &&
node.getKind() == kind::BITVECTOR_XNOR &&
@@ -473,17 +473,17 @@ void DefaultXnorBB (TNode node, Bits& bits, Bitblaster* bb) {
void DefaultNandBB (TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+ Debug("bitvector") << "theory::bv:: Unimplemented kind "
<< node.getKind() << "\n";
Unimplemented();
}
void DefaultNorBB (TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+ Debug("bitvector") << "theory::bv:: Unimplemented kind "
<< node.getKind() << "\n";
Unimplemented();
}
void DefaultCompBB (TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n";
+ Debug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n";
Assert(getSize(node) == 1 && bits.size() == 0 && node.getKind() == kind::BITVECTOR_COMP);
Bits a, b;
@@ -501,7 +501,7 @@ void DefaultCompBB (TNode node, Bits& bits, Bitblaster* bb) {
}
void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) {
- BVDebug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n";
+ Debug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n";
Assert(res.size() == 0 &&
node.getKind() == kind::BITVECTOR_MULT);
@@ -517,12 +517,12 @@ void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) {
res = newres;
}
if(Debug.isOn("bitvector-bb")) {
- BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n";
+ Debug("bitvector-bb") << "with bits: " << toString(res) << "\n";
}
}
void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n";
Assert(node.getKind() == kind::BITVECTOR_PLUS &&
res.size() == 0);
@@ -543,7 +543,7 @@ void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) {
void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n";
Assert(node.getKind() == kind::BITVECTOR_SUB &&
node.getNumChildren() == 2 &&
bits.size() == 0);
@@ -561,7 +561,7 @@ void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) {
}
void DefaultNegBB (TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n";
Assert(node.getKind() == kind::BITVECTOR_NEG);
Bits a;
@@ -639,7 +639,7 @@ void uDivModRec(const Bits& a, const Bits& b, Bits& q, Bits& r, unsigned rec_wid
}
void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n";
Assert(node.getKind() == kind::BITVECTOR_UDIV_TOTAL && q.size() == 0);
Bits a, b;
@@ -666,7 +666,7 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
}
void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n";
Assert(node.getKind() == kind::BITVECTOR_UREM_TOTAL && rem.size() == 0);
Bits a, b;
@@ -694,23 +694,23 @@ void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
void DefaultSdivBB (TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+ Debug("bitvector") << "theory::bv:: Unimplemented kind "
<< node.getKind() << "\n";
Unimplemented();
}
void DefaultSremBB (TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+ Debug("bitvector") << "theory::bv:: Unimplemented kind "
<< node.getKind() << "\n";
Unimplemented();
}
void DefaultSmodBB (TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+ Debug("bitvector") << "theory::bv:: Unimplemented kind "
<< node.getKind() << "\n";
Unimplemented();
}
void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node << "\n";
Assert (node.getKind() == kind::BITVECTOR_SHL &&
res.size() == 0);
Bits a, b;
@@ -738,12 +738,12 @@ void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) {
}
}
if(Debug.isOn("bitvector-bb")) {
- BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n";
+ Debug("bitvector-bb") << "with bits: " << toString(res) << "\n";
}
}
void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node << "\n";
Assert (node.getKind() == kind::BITVECTOR_LSHR &&
res.size() == 0);
Bits a, b;
@@ -771,13 +771,13 @@ void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) {
}
}
if(Debug.isOn("bitvector-bb")) {
- BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n";
+ Debug("bitvector-bb") << "with bits: " << toString(res) << "\n";
}
}
void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node << "\n";
Assert (node.getKind() == kind::BITVECTOR_ASHR &&
res.size() == 0);
Bits a, b;
@@ -806,7 +806,7 @@ void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) {
}
}
if(Debug.isOn("bitvector-bb")) {
- BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n";
+ Debug("bitvector-bb") << "with bits: " << toString(res) << "\n";
}
}
@@ -825,14 +825,14 @@ void DefaultExtractBB (TNode node, Bits& bits, Bitblaster* bb) {
Assert (bits.size() == high - low + 1);
if(Debug.isOn("bitvector-bb")) {
- BVDebug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
- BVDebug("bitvector-bb") << " with bits " << toString(bits);
+ Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << " with bits " << toString(bits);
}
}
void DefaultRepeatBB (TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+ Debug("bitvector") << "theory::bv:: Unimplemented kind "
<< node.getKind() << "\n";
// this should be rewritten
Unimplemented();
@@ -840,7 +840,7 @@ void DefaultRepeatBB (TNode node, Bits& bits, Bitblaster* bb) {
void DefaultZeroExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node << "\n";
// this should be rewritten
Unimplemented();
@@ -848,7 +848,7 @@ void DefaultZeroExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
}
void DefaultSignExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node << "\n";
Assert (node.getKind() == kind::BITVECTOR_SIGN_EXTEND &&
res_bits.size() == 0);
@@ -871,14 +871,14 @@ void DefaultSignExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
}
void DefaultRotateRightBB (TNode node, Bits& res, Bitblaster* bb) {
- BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+ Debug("bitvector") << "theory::bv:: Unimplemented kind "
<< node.getKind() << "\n";
Unimplemented();
}
void DefaultRotateLeftBB (TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+ Debug("bitvector") << "theory::bv:: Unimplemented kind "
<< node.getKind() << "\n";
Unimplemented();
}
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 91482526a..4f5325e10 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -92,7 +92,7 @@ void Bitblaster::bbAtom(TNode node) {
// make sure it is marked as an atom
addAtom(node);
- BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
+ Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
++d_statistics.d_numAtoms;
// the bitblasted definition of the atom
Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this));
@@ -115,7 +115,7 @@ void Bitblaster::bbTerm(TNode node, Bits& bits) {
return;
}
- BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
+ Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
++d_statistics.d_numTerms;
d_termBBStrategies[node.getKind()] (node, bits,this);
@@ -195,8 +195,8 @@ bool Bitblaster::assertToSat(TNode lit, bool propagate) {
markerLit = ~markerLit;
}
- BVDebug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n";
- BVDebug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal: " << markerLit << "\n";
+ Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n";
+ Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal: " << markerLit << "\n";
SatValue ret = d_satSolver->assertAssumption(markerLit, propagate);
@@ -221,7 +221,7 @@ bool Bitblaster::solve(bool quick_solve) {
Trace("bitvector") << " " << d_cnfStream->getNode(*it) << "\n";
}
}
- BVDebug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n";
+ Debug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n";
return SAT_VALUE_TRUE == d_satSolver->solve();
}
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index e113048b8..501aafb29 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -53,7 +53,7 @@ void BitblastSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
}
bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) {
- BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions (" << e << ")" << std::endl;
+ Debug("bitvector::bitblaster") << "BitblastSolver::addAssertions (" << e << ")" << std::endl;
//// Eager bit-blasting
if (options::bitvectorEagerBitblast()) {
@@ -106,7 +106,7 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory:
// solving
if (e == Theory::EFFORT_FULL || options::bitvectorEagerFullcheck()) {
Assert(!d_bv->inConflict());
- BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions solving. \n";
+ Debug("bitvector::bitblaster") << "BitblastSolver::addAssertions solving. \n";
bool ok = d_bitblaster->solve();
if (!ok) {
std::vector<TNode> conflictAtoms;
diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp
index ca3e3e35c..f11b1252b 100644
--- a/src/theory/bv/bv_subtheory_eq.cpp
+++ b/src/theory/bv/bv_subtheory_eq.cpp
@@ -131,7 +131,7 @@ bool EqualitySolver::addAssertions(const std::vector<TNode>& assertions, Theory:
}
bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
- BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
+ Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
if (value) {
return d_solver.storePropagation(equality);
} else {
@@ -140,7 +140,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool v
}
bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
- BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
+ Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
if (value) {
return d_solver.storePropagation(predicate);
} else {
diff --git a/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h
index e4bcbca47..ec7f6d66d 100644
--- a/src/theory/bv/cd_set_collection.h
+++ b/src/theory/bv/cd_set_collection.h
@@ -71,7 +71,7 @@ class BacktrackableSetCollection {
const tree_entry_type& node = d_memory.back();
if(Debug.isOn("cd_set_collection")) {
- BVDebug("cd_set_collection") << "BacktrackableSetCollection::backtrack(): removing " << node.getValue()
+ Debug("cd_set_collection") << "BacktrackableSetCollection::backtrack(): removing " << node.getValue()
<< " from " << internalToString(getRoot(d_memory.size()-1)) << std::endl;
}
@@ -279,7 +279,7 @@ public:
// Find the biggest node smaleer than value (it must exist)
while (set != null) {
if(Debug.isOn("set_collection")) {
- BVDebug("set_collection") << "BacktrackableSetCollection::getPrev(" << toString(set) << "," << value << ")" << std::endl;
+ Debug("set_collection") << "BacktrackableSetCollection::getPrev(" << toString(set) << "," << value << ")" << std::endl;
}
const tree_entry_type& node = d_memory[set];
if (node.getValue() >= value) {
@@ -308,7 +308,7 @@ public:
// Find the smallest node bigger than value (it must exist)
while (set != null) {
if(Debug.isOn("set_collection")) {
- BVDebug("set_collection") << "BacktrackableSetCollection::getNext(" << toString(set) << "," << value << ")" << std::endl;
+ Debug("set_collection") << "BacktrackableSetCollection::getNext(" << toString(set) << "," << value << ")" << std::endl;
}
const tree_entry_type& node = d_memory[set];
if (node.getValue() <= value) {
@@ -377,7 +377,7 @@ public:
Assert(isValid(set));
if(Debug.isOn("set_collection")) {
- BVDebug("set_collection") << "BacktrackableSetCollection::getElements(" << toString(set) << "," << lowerBound << "," << upperBound << ")" << std::endl;
+ Debug("set_collection") << "BacktrackableSetCollection::getElements(" << toString(set) << "," << lowerBound << "," << upperBound << ")" << std::endl;
}
// Empty set no elements
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 7acb93cc2..de5b70557 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -72,7 +72,7 @@ TheoryBV::Statistics::~Statistics() {
}
void TheoryBV::preRegisterTerm(TNode node) {
- BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
+ Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
if (options::bitvectorEagerBitblast()) {
// don't use the equality engine in the eager bit-blasting
@@ -88,7 +88,7 @@ void TheoryBV::sendConflict() {
if (d_conflictNode.isNull()) {
return;
} else {
- BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
+ Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
d_out->conflict(d_conflictNode);
d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
d_conflictNode = Node::null();
@@ -97,7 +97,7 @@ void TheoryBV::sendConflict() {
void TheoryBV::check(Effort e)
{
- BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
+ Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
// if we are already in conflict just return the conflict
if (inConflict()) {
@@ -111,7 +111,7 @@ void TheoryBV::check(Effort e)
Assertion assertion = get();
TNode fact = assertion.assertion;
new_assertions.push_back(fact);
- BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n";
+ Debug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n";
}
if (!inConflict()) {
@@ -138,7 +138,7 @@ void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
}
void TheoryBV::propagate(Effort e) {
- BVDebug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
+ Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
if (inConflict()) {
return;
@@ -152,7 +152,7 @@ void TheoryBV::propagate(Effort e) {
}
if (!ok) {
- BVDebug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl;
+ Debug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl;
setConflict();
}
}
@@ -197,7 +197,7 @@ Node TheoryBV::ppRewrite(TNode t)
bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
{
- Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ")" << std::endl;
+ Debug("bitvector::propagate") << indent() << getSatContext()->getLevel() << " " << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ")" << std::endl;
// If already in conflict, no more propagation
if (d_conflict) {
@@ -240,18 +240,18 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
// Ask the appropriate subtheory for the explanation
if (propagatedBy(literal, SUB_EQUALITY)) {
- BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << "): EQUALITY" << std::endl;
+ Debug("bitvector::explain") << "TheoryBV::explain(" << literal << "): EQUALITY" << std::endl;
d_equalitySolver.explain(literal, assumptions);
} else {
Assert(propagatedBy(literal, SUB_BITBLAST));
- BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl;
+ Debug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl;
d_bitblastSolver.explain(literal, assumptions);
}
}
Node TheoryBV::explain(TNode node) {
- BVDebug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl;
+ Debug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl;
std::vector<TNode> assumptions;
// Ask for the explanation
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index f9650932e..bd7a8131a 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -334,7 +334,7 @@ public:
template<bool checkApplies>
static inline Node run(TNode node) {
if (!checkApplies || applies(node)) {
- BVDebug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ")" << std::endl;
+ Debug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ")" << std::endl;
Assert(checkApplies || applies(node));
//++ s_statistics->d_ruleApplications;
Node result = apply(node);
@@ -355,7 +355,7 @@ public:
<< CheckSatCommand(condition.toExpr());
}
}
- BVDebug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ") => " << result << std::endl;
+ Debug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ") => " << result << std::endl;
return result;
} else {
return node;
@@ -486,7 +486,7 @@ bool RewriteRule<EmptyRule>::applies(TNode node) {
template<> inline
Node RewriteRule<EmptyRule>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<EmptyRule> for " << node.getKind() <<"\n";
+ Debug("bv-rewrite") << "RewriteRule<EmptyRule> for " << node.getKind() <<"\n";
Unreachable();
return node;
}
diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index 498378638..178b17b43 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -37,7 +37,7 @@ bool RewriteRule<EvalAnd>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalAnd>::apply(TNode node) {
Unreachable();
- BVDebug("bv-rewrite") << "RewriteRule<EvalAnd>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalAnd>(" << node << ")" << std::endl;
BitVector a = node[0].getConst<BitVector>();
BitVector b = node[1].getConst<BitVector>();
BitVector res = a & b;
@@ -56,7 +56,7 @@ bool RewriteRule<EvalOr>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalOr>::apply(TNode node) {
Unreachable();
- BVDebug("bv-rewrite") << "RewriteRule<EvalOr>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalOr>(" << node << ")" << std::endl;
BitVector a = node[0].getConst<BitVector>();
BitVector b = node[1].getConst<BitVector>();
BitVector res = a | b;
@@ -75,7 +75,7 @@ bool RewriteRule<EvalXor>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalXor>::apply(TNode node) {
Unreachable();
- BVDebug("bv-rewrite") << "RewriteRule<EvalXor>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalXor>(" << node << ")" << std::endl;
BitVector a = node[0].getConst<BitVector>();
BitVector b = node[1].getConst<BitVector>();
BitVector res = a ^ b;
@@ -91,7 +91,7 @@ Node RewriteRule<EvalXor>::apply(TNode node) {
// template<> inline
// Node RewriteRule<EvalXnor>::apply(TNode node) {
-// BVDebug("bv-rewrite") << "RewriteRule<EvalXnor>(" << node << ")" << std::endl;
+// Debug("bv-rewrite") << "RewriteRule<EvalXnor>(" << node << ")" << std::endl;
// BitVector a = node[0].getConst<BitVector>();
// BitVector b = node[1].getConst<BitVector>();
// BitVector res = ~ (a ^ b);
@@ -106,7 +106,7 @@ bool RewriteRule<EvalNot>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalNot>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<EvalNot>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalNot>(" << node << ")" << std::endl;
BitVector a = node[0].getConst<BitVector>();
BitVector res = ~ a;
return utils::mkConst(res);
@@ -120,7 +120,7 @@ Node RewriteRule<EvalNot>::apply(TNode node) {
// template<> inline
// Node RewriteRule<EvalComp>::apply(TNode node) {
-// BVDebug("bv-rewrite") << "RewriteRule<EvalComp>(" << node << ")" << std::endl;
+// Debug("bv-rewrite") << "RewriteRule<EvalComp>(" << node << ")" << std::endl;
// BitVector a = node[0].getConst<BitVector>();
// BitVector b = node[1].getConst<BitVector>();
// BitVector res;
@@ -141,7 +141,7 @@ bool RewriteRule<EvalMult>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalMult>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<EvalMult>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalMult>(" << node << ")" << std::endl;
TNode::iterator child_it = node.begin();
BitVector res = (*child_it).getConst<BitVector>();
for(++child_it; child_it != node.end(); ++child_it) {
@@ -158,7 +158,7 @@ bool RewriteRule<EvalPlus>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalPlus>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<EvalPlus>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalPlus>(" << node << ")" << std::endl;
TNode::iterator child_it = node.begin();
BitVector res = (*child_it).getConst<BitVector>();
for(++child_it; child_it != node.end(); ++child_it) {
@@ -175,7 +175,7 @@ Node RewriteRule<EvalPlus>::apply(TNode node) {
// template<> inline
// Node RewriteRule<EvalSub>::apply(TNode node) {
-// BVDebug("bv-rewrite") << "RewriteRule<EvalSub>(" << node << ")" << std::endl;
+// Debug("bv-rewrite") << "RewriteRule<EvalSub>(" << node << ")" << std::endl;
// BitVector a = node[0].getConst<BitVector>();
// BitVector b = node[1].getConst<BitVector>();
// BitVector res = a - b;
@@ -190,7 +190,7 @@ bool RewriteRule<EvalNeg>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalNeg>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<EvalNeg>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalNeg>(" << node << ")" << std::endl;
BitVector a = node[0].getConst<BitVector>();
BitVector res = - a;
@@ -204,7 +204,7 @@ bool RewriteRule<EvalUdiv>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalUdiv>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<EvalUdiv>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalUdiv>(" << node << ")" << std::endl;
BitVector a = node[0].getConst<BitVector>();
BitVector b = node[1].getConst<BitVector>();
BitVector res = a.unsignedDivTotal(b);
@@ -219,7 +219,7 @@ bool RewriteRule<EvalUrem>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalUrem>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<EvalUrem>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalUrem>(" << node << ")" << std::endl;
BitVector a = node[0].getConst<BitVector>();
BitVector b = node[1].getConst<BitVector>();
BitVector res = a.unsignedRemTotal(b);
@@ -234,7 +234,7 @@ bool RewriteRule<EvalShl>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalShl>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<EvalShl>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalShl>(" << node << ")" << std::endl;
BitVector a = node[0].getConst<BitVector>();
BitVector b = node[1].getConst<BitVector>();
@@ -250,7 +250,7 @@ bool RewriteRule<EvalLshr>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalLshr>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<EvalLshr>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalLshr>(" << node << ")" << std::endl;
BitVector a = node[0].getConst<BitVector>();
BitVector b = node[1].getConst<BitVector>();
@@ -266,7 +266,7 @@ bool RewriteRule<EvalAshr>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalAshr>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<EvalAshr>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalAshr>(" << node << ")" << std::endl;
BitVector a = node[0].getConst<BitVector>();
BitVector b = node[1].getConst<BitVector>();
@@ -282,7 +282,7 @@ bool RewriteRule<EvalUlt>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalUlt>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<EvalUlt>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalUlt>(" << node << ")" << std::endl;
BitVector a = node[0].getConst<BitVector>();
BitVector b = node[1].getConst<BitVector>();
@@ -300,7 +300,7 @@ bool RewriteRule<EvalSlt>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalSlt>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<EvalSlt>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalSlt>(" << node << ")" << std::endl;
BitVector a = node[0].getConst<BitVector>();
BitVector b = node[1].getConst<BitVector>();
@@ -319,7 +319,7 @@ bool RewriteRule<EvalUle>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalUle>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<EvalUle>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalUle>(" << node << ")" << std::endl;
BitVector a = node[0].getConst<BitVector>();
BitVector b = node[1].getConst<BitVector>();
@@ -337,7 +337,7 @@ bool RewriteRule<EvalSle>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalSle>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<EvalSle>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalSle>(" << node << ")" << std::endl;
BitVector a = node[0].getConst<BitVector>();
BitVector b = node[1].getConst<BitVector>();
@@ -355,7 +355,7 @@ bool RewriteRule<EvalExtract>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalExtract>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<EvalExtract>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalExtract>(" << node << ")" << std::endl;
BitVector a = node[0].getConst<BitVector>();
unsigned lo = utils::getExtractLow(node);
unsigned hi = utils::getExtractHigh(node);
@@ -373,7 +373,7 @@ bool RewriteRule<EvalConcat>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalConcat>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<EvalConcat>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalConcat>(" << node << ")" << std::endl;
unsigned num = node.getNumChildren();
BitVector res = node[0].getConst<BitVector>();
for(unsigned i = 1; i < num; ++i ) {
@@ -391,7 +391,7 @@ bool RewriteRule<EvalSignExtend>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalSignExtend>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<EvalSignExtend>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalSignExtend>(" << node << ")" << std::endl;
BitVector a = node[0].getConst<BitVector>();
unsigned amount = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
BitVector res = a.signExtend(amount);
@@ -407,7 +407,7 @@ bool RewriteRule<EvalEquals>::applies(TNode node) {
template<> inline
Node RewriteRule<EvalEquals>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<EvalEquals>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<EvalEquals>(" << node << ")" << std::endl;
BitVector a = node[0].getConst<BitVector>();
BitVector b = node[1].getConst<BitVector>();
if (a == b) {
diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index b44c72f74..ade345d1c 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -33,7 +33,7 @@ bool RewriteRule<ConcatFlatten>::applies(TNode node) {
template<> inline
Node RewriteRule<ConcatFlatten>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << node << ")" << std::endl;
NodeBuilder<> result(kind::BITVECTOR_CONCAT);
std::vector<Node> processing_stack;
processing_stack.push_back(node);
@@ -48,7 +48,7 @@ Node RewriteRule<ConcatFlatten>::apply(TNode node) {
}
}
Node resultNode = result;
- BVDebug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << resultNode << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << resultNode << ")" << std::endl;
return resultNode;
}
@@ -60,7 +60,7 @@ bool RewriteRule<ConcatExtractMerge>::applies(TNode node) {
template<> inline
Node RewriteRule<ConcatExtractMerge>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<ConcatExtractMerge>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<ConcatExtractMerge>(" << node << ")" << std::endl;
std::vector<Node> mergedExtracts;
@@ -121,7 +121,7 @@ bool RewriteRule<ConcatConstantMerge>::applies(TNode node) {
template<> inline
Node RewriteRule<ConcatConstantMerge>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ")" << std::endl;
std::vector<Node> mergedConstants;
for (unsigned i = 0, end = node.getNumChildren(); i < end;) {
@@ -150,7 +150,7 @@ Node RewriteRule<ConcatConstantMerge>::apply(TNode node) {
}
}
- BVDebug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ") => " << utils::mkConcat(mergedConstants) << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ") => " << utils::mkConcat(mergedConstants) << std::endl;
return utils::mkConcat(mergedConstants);
}
@@ -168,7 +168,7 @@ bool RewriteRule<ExtractWhole>::applies(TNode node) {
template<> inline
Node RewriteRule<ExtractWhole>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<ExtractWhole>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<ExtractWhole>(" << node << ")" << std::endl;
return node[0];
}
@@ -181,7 +181,7 @@ bool RewriteRule<ExtractConstant>::applies(TNode node) {
template<> inline
Node RewriteRule<ExtractConstant>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<ExtractConstant>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<ExtractConstant>(" << node << ")" << std::endl;
Node child = node[0];
BitVector childValue = child.getConst<BitVector>();
return utils::mkConst(childValue.extract(utils::getExtractHigh(node), utils::getExtractLow(node)));
@@ -189,7 +189,7 @@ Node RewriteRule<ExtractConstant>::apply(TNode node) {
template<> inline
bool RewriteRule<ExtractConcat>::applies(TNode node) {
- //BVDebug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
+ //Debug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
if (node[0].getKind() != kind::BITVECTOR_CONCAT) return false;
return true;
@@ -197,7 +197,7 @@ bool RewriteRule<ExtractConcat>::applies(TNode node) {
template<> inline
Node RewriteRule<ExtractConcat>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
int extract_high = utils::getExtractHigh(node);
int extract_low = utils::getExtractLow(node);
@@ -230,7 +230,7 @@ bool RewriteRule<ExtractExtract>::applies(TNode node) {
template<> inline
Node RewriteRule<ExtractExtract>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<ExtractExtract>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<ExtractExtract>(" << node << ")" << std::endl;
// x[i:j][k:l] ~> x[k+j:l+j]
Node child = node[0];
@@ -244,7 +244,7 @@ Node RewriteRule<ExtractExtract>::apply(TNode node) {
template<> inline
bool RewriteRule<FailEq>::applies(TNode node) {
- //BVDebug("bv-rewrite") << "RewriteRule<FailEq>(" << node << ")" << std::endl;
+ //Debug("bv-rewrite") << "RewriteRule<FailEq>(" << node << ")" << std::endl;
if (node.getKind() != kind::EQUAL) return false;
if (node[0].getKind() != kind::CONST_BITVECTOR) return false;
if (node[1].getKind() != kind::CONST_BITVECTOR) return false;
@@ -264,7 +264,7 @@ bool RewriteRule<SimplifyEq>::applies(TNode node) {
template<> inline
Node RewriteRule<SimplifyEq>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<SimplifyEq>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<SimplifyEq>(" << node << ")" << std::endl;
return utils::mkTrue();
}
@@ -275,7 +275,7 @@ bool RewriteRule<ReflexivityEq>::applies(TNode node) {
template<> inline
Node RewriteRule<ReflexivityEq>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl;
return node[1].eqNode(node[0]);
}
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 6b3d0f770..39f55f26c 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -41,7 +41,7 @@ bool RewriteRule<ExtractBitwise>::applies(TNode node) {
template<> inline
Node RewriteRule<ExtractBitwise>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<ExtractBitwise>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<ExtractBitwise>(" << node << ")" << std::endl;
unsigned high = utils::getExtractHigh(node);
unsigned low = utils::getExtractLow(node);
std::vector<Node> children;
@@ -65,7 +65,7 @@ bool RewriteRule<ExtractNot>::applies(TNode node) {
template<> inline
Node RewriteRule<ExtractNot>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<ExtractNot>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<ExtractNot>(" << node << ")" << std::endl;
unsigned low = utils::getExtractLow(node);
unsigned high = utils::getExtractHigh(node);
Node a = utils::mkExtract(node[0][0], high, low);
@@ -88,7 +88,7 @@ bool RewriteRule<ExtractArith>::applies(TNode node) {
template<> inline
Node RewriteRule<ExtractArith>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<ExtractArith>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<ExtractArith>(" << node << ")" << std::endl;
unsigned low = utils::getExtractLow(node);
Assert (low == 0);
unsigned high = utils::getExtractHigh(node);
@@ -117,7 +117,7 @@ bool RewriteRule<ExtractArith2>::applies(TNode node) {
template<> inline
Node RewriteRule<ExtractArith2>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<ExtractArith2>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<ExtractArith2>(" << node << ")" << std::endl;
unsigned low = utils::getExtractLow(node);
unsigned high = utils::getExtractHigh(node);
std::vector<Node> children;
@@ -151,7 +151,7 @@ bool RewriteRule<FlattenAssocCommut>::applies(TNode node) {
template<> inline
Node RewriteRule<FlattenAssocCommut>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl;
std::vector<Node> processingStack;
processingStack.push_back(node);
std::vector<Node> children;
@@ -291,7 +291,7 @@ bool RewriteRule<PlusCombineLikeTerms>::applies(TNode node) {
template<> inline
Node RewriteRule<PlusCombineLikeTerms>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<PlusCombineLikeTerms>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<PlusCombineLikeTerms>(" << node << ")" << std::endl;
unsigned size = utils::getSize(node);
BitVector constSum(size, (unsigned)0);
std::map<Node, BitVector> factorToCoefficient;
@@ -348,7 +348,7 @@ bool RewriteRule<MultSimplify>::applies(TNode node) {
template<> inline
Node RewriteRule<MultSimplify>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<MultSimplify>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<MultSimplify>(" << node << ")" << std::endl;
unsigned size = utils::getSize(node);
BitVector constant(size, Integer(1));
@@ -397,7 +397,7 @@ bool RewriteRule<MultDistribConst>::applies(TNode node) {
template<> inline
Node RewriteRule<MultDistribConst>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<MultDistribConst>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<MultDistribConst>(" << node << ")" << std::endl;
TNode constant = node[1];
TNode factor = node[0];
@@ -434,7 +434,7 @@ bool RewriteRule<SolveEq>::applies(TNode node) {
// Doesn't do full solving (yet), instead, if a term appears both on lhs and rhs, it subtracts from both sides so that one side's coeff is zero
template<> inline
Node RewriteRule<SolveEq>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<SolveEq>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<SolveEq>(" << node << ")" << std::endl;
TNode left = node[0];
TNode right = node[1];
@@ -662,7 +662,7 @@ static inline Node mkNodeKind(Kind k, TNode node, TNode c) {
template<> inline
Node RewriteRule<BitwiseEq>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<BitwiseEq>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<BitwiseEq>(" << node << ")" << std::endl;
TNode term;
BitVector c;
@@ -745,7 +745,7 @@ bool RewriteRule<NegMult>::applies(TNode node) {
template<> inline
Node RewriteRule<NegMult>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<NegMult>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<NegMult>(" << node << ")" << std::endl;
TNode mult = node[0];
NodeBuilder<> nb(kind::BITVECTOR_MULT);
BitVector bv(utils::getSize(node), (unsigned)1);
@@ -767,7 +767,7 @@ bool RewriteRule<NegSub>::applies(TNode node) {
template<> inline
Node RewriteRule<NegSub>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<NegSub>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<NegSub>(" << node << ")" << std::endl;
return utils::mkNode(kind::BITVECTOR_SUB, node[0][1], node[0][0]);
}
@@ -779,7 +779,7 @@ bool RewriteRule<NegPlus>::applies(TNode node) {
template<> inline
Node RewriteRule<NegPlus>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<NegPlus>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<NegPlus>(" << node << ")" << std::endl;
std::vector<Node> children;
for (unsigned i = 0; i < node[0].getNumChildren(); ++i) {
children.push_back(utils::mkNode(kind::BITVECTOR_NEG, node[0][i]));
@@ -820,7 +820,7 @@ bool RewriteRule<AndSimplify>::applies(TNode node) {
template<> inline
Node RewriteRule<AndSimplify>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
// this will remove duplicates
std::hash_map<TNode, Count, TNodeHashFunction> subterms;
@@ -883,7 +883,7 @@ bool RewriteRule<OrSimplify>::applies(TNode node) {
template<> inline
Node RewriteRule<OrSimplify>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<OrSimplify>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<OrSimplify>(" << node << ")" << std::endl;
// this will remove duplicates
std::hash_map<TNode, Count, TNodeHashFunction> subterms;
@@ -946,7 +946,7 @@ bool RewriteRule<XorSimplify>::applies(TNode node) {
template<> inline
Node RewriteRule<XorSimplify>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<XorSimplify>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<XorSimplify>(" << node << ")" << std::endl;
std::hash_map<TNode, Count, TNodeHashFunction> subterms;
@@ -1041,7 +1041,7 @@ Node RewriteRule<XorSimplify>::apply(TNode node) {
// template<> inline
// Node RewriteRule<AndSimplify>::apply(TNode node) {
-// BVDebug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
+// Debug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
// return resultNode;
// }
@@ -1053,7 +1053,7 @@ Node RewriteRule<XorSimplify>::apply(TNode node) {
// template<> inline
// Node RewriteRule<>::apply(TNode node) {
-// BVDebug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl;
+// Debug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl;
// return resultNode;
// }
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 94983e03a..4202f8c2e 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -33,7 +33,7 @@ bool RewriteRule<UgtEliminate>::applies(TNode node) {
template<>
Node RewriteRule<UgtEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<UgtEliminate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<UgtEliminate>(" << node << ")" << std::endl;
TNode a = node[0];
TNode b = node[1];
Node result = utils::mkNode(kind::BITVECTOR_ULT, b, a);
@@ -48,7 +48,7 @@ bool RewriteRule<UgeEliminate>::applies(TNode node) {
template<>
Node RewriteRule<UgeEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<UgeEliminate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<UgeEliminate>(" << node << ")" << std::endl;
TNode a = node[0];
TNode b = node[1];
Node result = utils::mkNode(kind::BITVECTOR_ULE, b, a);
@@ -63,7 +63,7 @@ bool RewriteRule<SgtEliminate>::applies(TNode node) {
template<>
Node RewriteRule<SgtEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<SgtEliminate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<SgtEliminate>(" << node << ")" << std::endl;
TNode a = node[0];
TNode b = node[1];
Node result = utils::mkNode(kind::BITVECTOR_SLT, b, a);
@@ -78,7 +78,7 @@ bool RewriteRule<SgeEliminate>::applies(TNode node) {
template<>
Node RewriteRule<SgeEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<SgeEliminate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<SgeEliminate>(" << node << ")" << std::endl;
TNode a = node[0];
TNode b = node[1];
Node result = utils::mkNode(kind::BITVECTOR_SLE, b, a);
@@ -92,7 +92,7 @@ bool RewriteRule<SltEliminate>::applies(TNode node) {
template <>
Node RewriteRule<SltEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<SltEliminate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<SltEliminate>(" << node << ")" << std::endl;
unsigned size = utils::getSize(node[0]);
Node pow_two = utils::mkConst(BitVector(size, Integer(1).multiplyByPow2(size - 1)));
@@ -110,7 +110,7 @@ bool RewriteRule<SleEliminate>::applies(TNode node) {
template <>
Node RewriteRule<SleEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<SleEliminate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<SleEliminate>(" << node << ")" << std::endl;
unsigned size = utils::getSize(node[0]);
Node pow_two = utils::mkConst(BitVector(size, Integer(1).multiplyByPow2(size - 1)));
@@ -128,7 +128,7 @@ bool RewriteRule<CompEliminate>::applies(TNode node) {
template <>
Node RewriteRule<CompEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<CompEliminate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<CompEliminate>(" << node << ")" << std::endl;
Node comp = utils::mkNode(kind::EQUAL, node[0], node[1]);
Node one = utils::mkConst(1, 1);
Node zero = utils::mkConst(1, 0);
@@ -143,7 +143,7 @@ bool RewriteRule<SubEliminate>::applies(TNode node) {
template <>
Node RewriteRule<SubEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<SubEliminate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<SubEliminate>(" << node << ")" << std::endl;
Node negb = utils::mkNode(kind::BITVECTOR_NEG, node[1]);
Node a = node[0];
@@ -158,7 +158,7 @@ bool RewriteRule<RepeatEliminate>::applies(TNode node) {
template<>
Node RewriteRule<RepeatEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<RepeatEliminate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<RepeatEliminate>(" << node << ")" << std::endl;
TNode a = node[0];
unsigned amount = node.getOperator().getConst<BitVectorRepeat>().repeatAmount;
Assert(amount >= 1);
@@ -180,7 +180,7 @@ bool RewriteRule<RotateLeftEliminate>::applies(TNode node) {
template<>
Node RewriteRule<RotateLeftEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<RotateLeftEliminate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<RotateLeftEliminate>(" << node << ")" << std::endl;
TNode a = node[0];
unsigned amount = node.getOperator().getConst<BitVectorRotateLeft>().rotateLeftAmount;
amount = amount % utils::getSize(a);
@@ -202,7 +202,7 @@ bool RewriteRule<RotateRightEliminate>::applies(TNode node) {
template<>
Node RewriteRule<RotateRightEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<RotateRightEliminate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<RotateRightEliminate>(" << node << ")" << std::endl;
TNode a = node[0];
unsigned amount = node.getOperator().getConst<BitVectorRotateRight>().rotateRightAmount;
amount = amount % utils::getSize(a);
@@ -225,7 +225,7 @@ bool RewriteRule<NandEliminate>::applies(TNode node) {
template<>
Node RewriteRule<NandEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<NandEliminate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<NandEliminate>(" << node << ")" << std::endl;
TNode a = node[0];
TNode b = node[1];
Node andNode = utils::mkNode(kind::BITVECTOR_AND, a, b);
@@ -241,7 +241,7 @@ bool RewriteRule<NorEliminate>::applies(TNode node) {
template<>
Node RewriteRule<NorEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<NorEliminate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<NorEliminate>(" << node << ")" << std::endl;
TNode a = node[0];
TNode b = node[1];
Node orNode = utils::mkNode(kind::BITVECTOR_OR, a, b);
@@ -257,7 +257,7 @@ bool RewriteRule<XnorEliminate>::applies(TNode node) {
template<>
Node RewriteRule<XnorEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<XnorEliminate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<XnorEliminate>(" << node << ")" << std::endl;
TNode a = node[0];
TNode b = node[1];
Node xorNode = utils::mkNode(kind::BITVECTOR_XOR, a, b);
@@ -272,7 +272,7 @@ bool RewriteRule<SdivEliminate>::applies(TNode node) {
template<>
Node RewriteRule<SdivEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<SdivEliminate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<SdivEliminate>(" << node << ")" << std::endl;
TNode a = node[0];
TNode b = node[1];
@@ -301,7 +301,7 @@ bool RewriteRule<SremEliminate>::applies(TNode node) {
template<>
Node RewriteRule<SremEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<SremEliminate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<SremEliminate>(" << node << ")" << std::endl;
TNode a = node[0];
TNode b = node[1];
unsigned size = utils::getSize(a);
@@ -327,7 +327,7 @@ bool RewriteRule<SmodEliminate>::applies(TNode node) {
template<>
Node RewriteRule<SmodEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<SmodEliminate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<SmodEliminate>(" << node << ")" << std::endl;
TNode s = node[0];
TNode t = node[1];
unsigned size = utils::getSize(s);
@@ -382,7 +382,7 @@ bool RewriteRule<ZeroExtendEliminate>::applies(TNode node) {
template<>
Node RewriteRule<ZeroExtendEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<ZeroExtendEliminate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<ZeroExtendEliminate>(" << node << ")" << std::endl;
TNode bv = node[0];
unsigned amount = node.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
@@ -402,7 +402,7 @@ bool RewriteRule<SignExtendEliminate>::applies(TNode node) {
template<>
Node RewriteRule<SignExtendEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<SignExtendEliminate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<SignExtendEliminate>(" << node << ")" << std::endl;
unsigned amount = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
if(amount == 0) {
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 8bcc64414..9d1cafab9 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -43,7 +43,7 @@ bool RewriteRule<ShlByConst>::applies(TNode node) {
template<> inline
Node RewriteRule<ShlByConst>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<ShlByConst>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<ShlByConst>(" << node << ")" << std::endl;
Integer amount = node[1].getConst<BitVector>().toInteger();
Node a = node[0];
@@ -79,7 +79,7 @@ bool RewriteRule<LshrByConst>::applies(TNode node) {
template<> inline
Node RewriteRule<LshrByConst>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<LshrByConst>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<LshrByConst>(" << node << ")" << std::endl;
Integer amount = node[1].getConst<BitVector>().toInteger();
Node a = node[0];
@@ -115,7 +115,7 @@ bool RewriteRule<AshrByConst>::applies(TNode node) {
template<> inline
Node RewriteRule<AshrByConst>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<AshrByConst>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<AshrByConst>(" << node << ")" << std::endl;
Integer amount = node[1].getConst<BitVector>().toInteger();
Node a = node[0];
@@ -160,7 +160,7 @@ bool RewriteRule<BitwiseIdemp>::applies(TNode node) {
template<> inline
Node RewriteRule<BitwiseIdemp>::apply(TNode node) {
Unreachable();
- BVDebug("bv-rewrite") << "RewriteRule<BitwiseIdemp>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<BitwiseIdemp>(" << node << ")" << std::endl;
return node[0];
}
@@ -183,7 +183,7 @@ bool RewriteRule<AndZero>::applies(TNode node) {
template<> inline
Node RewriteRule<AndZero>::apply(TNode node) {
Unreachable();
- BVDebug("bv-rewrite") << "RewriteRule<AndZero>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<AndZero>(" << node << ")" << std::endl;
return utils::mkConst(utils::getSize(node), 0);
}
@@ -207,7 +207,7 @@ bool RewriteRule<AndOne>::applies(TNode node) {
template<> inline
Node RewriteRule<AndOne>::apply(TNode node) {
Unreachable();
- BVDebug("bv-rewrite") << "RewriteRule<AndOne>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<AndOne>(" << node << ")" << std::endl;
unsigned size = utils::getSize(node);
if (node[0] == utils::mkOnes(size)) {
@@ -237,7 +237,7 @@ bool RewriteRule<OrZero>::applies(TNode node) {
template<> inline
Node RewriteRule<OrZero>::apply(TNode node) {
Unreachable();
- BVDebug("bv-rewrite") << "RewriteRule<OrZero>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<OrZero>(" << node << ")" << std::endl;
unsigned size = utils::getSize(node);
if (node[0] == utils::mkConst(size, 0)) {
@@ -268,7 +268,7 @@ bool RewriteRule<OrOne>::applies(TNode node) {
template<> inline
Node RewriteRule<OrOne>::apply(TNode node) {
Unreachable();
- BVDebug("bv-rewrite") << "RewriteRule<OrOne>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<OrOne>(" << node << ")" << std::endl;
return utils::mkOnes(utils::getSize(node));
}
@@ -290,7 +290,7 @@ bool RewriteRule<XorDuplicate>::applies(TNode node) {
template<> inline
Node RewriteRule<XorDuplicate>::apply(TNode node) {
Unreachable();
- BVDebug("bv-rewrite") << "RewriteRule<XorDuplicate>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<XorDuplicate>(" << node << ")" << std::endl;
return utils::mkConst(BitVector(utils::getSize(node), Integer(0)));
}
@@ -316,7 +316,7 @@ bool RewriteRule<XorOne>::applies(TNode node) {
template<> inline
Node RewriteRule<XorOne>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<XorOne>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<XorOne>(" << node << ")" << std::endl;
Node ones = utils::mkOnes(utils::getSize(node));
std::vector<Node> children;
bool found_ones = false;
@@ -360,7 +360,7 @@ bool RewriteRule<XorZero>::applies(TNode node) {
template<> inline
Node RewriteRule<XorZero>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<XorZero>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<XorZero>(" << node << ")" << std::endl;
std::vector<Node> children;
Node zero = utils::mkConst(utils::getSize(node), 0);
@@ -393,7 +393,7 @@ bool RewriteRule<BitwiseNotAnd>::applies(TNode node) {
template<> inline
Node RewriteRule<BitwiseNotAnd>::apply(TNode node) {
Unreachable();
- BVDebug("bv-rewrite") << "RewriteRule<BitwiseNegAnd>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<BitwiseNegAnd>(" << node << ")" << std::endl;
return utils::mkConst(BitVector(utils::getSize(node), Integer(0)));
}
@@ -415,7 +415,7 @@ bool RewriteRule<BitwiseNotOr>::applies(TNode node) {
template<> inline
Node RewriteRule<BitwiseNotOr>::apply(TNode node) {
Unreachable();
- BVDebug("bv-rewrite") << "RewriteRule<BitwiseNotOr>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<BitwiseNotOr>(" << node << ")" << std::endl;
uint32_t size = utils::getSize(node);
Integer ones = Integer(1).multiplyByPow2(size) - 1;
return utils::mkConst(BitVector(size, ones));
@@ -435,7 +435,7 @@ bool RewriteRule<XorNot>::applies(TNode node) {
template<> inline
Node RewriteRule<XorNot>::apply(TNode node) {
Unreachable();
- BVDebug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl;
Node a = node[0][0];
Node b = node[1][0];
return utils::mkNode(kind::BITVECTOR_XOR, a, b);
@@ -455,7 +455,7 @@ bool RewriteRule<NotXor>::applies(TNode node) {
template<> inline
Node RewriteRule<NotXor>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<NotXor>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<NotXor>(" << node << ")" << std::endl;
std::vector<Node> children;
TNode::iterator child_it = node[0].begin();
children.push_back(utils::mkNode(kind::BITVECTOR_NOT, *child_it));
@@ -479,7 +479,7 @@ bool RewriteRule<NotIdemp>::applies(TNode node) {
template<> inline
Node RewriteRule<NotIdemp>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<XorIdemp>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<XorIdemp>(" << node << ")" << std::endl;
return node[0][0];
}
@@ -500,7 +500,7 @@ bool RewriteRule<LtSelf>::applies(TNode node) {
template<> inline
Node RewriteRule<LtSelf>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<LtSelf>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<LtSelf>(" << node << ")" << std::endl;
return utils::mkFalse();
}
@@ -519,7 +519,7 @@ bool RewriteRule<LteSelf>::applies(TNode node) {
template<> inline
Node RewriteRule<LteSelf>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<LteSelf>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<LteSelf>(" << node << ")" << std::endl;
return utils::mkTrue();
}
@@ -537,7 +537,7 @@ bool RewriteRule<UltZero>::applies(TNode node) {
template<> inline
Node RewriteRule<UltZero>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl;
return utils::mkFalse();
}
@@ -555,7 +555,7 @@ bool RewriteRule<UltSelf>::applies(TNode node) {
template<> inline
Node RewriteRule<UltSelf>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<UltSelf>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<UltSelf>(" << node << ")" << std::endl;
return utils::mkFalse();
}
@@ -574,7 +574,7 @@ bool RewriteRule<UleZero>::applies(TNode node) {
template<> inline
Node RewriteRule<UleZero>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<UleZero>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<UleZero>(" << node << ")" << std::endl;
return utils::mkNode(kind::EQUAL, node[0], node[1]);
}
@@ -592,7 +592,7 @@ bool RewriteRule<UleSelf>::applies(TNode node) {
template<> inline
Node RewriteRule<UleSelf>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<UleSelf>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<UleSelf>(" << node << ")" << std::endl;
return utils::mkTrue();
}
@@ -611,7 +611,7 @@ bool RewriteRule<ZeroUle>::applies(TNode node) {
template<> inline
Node RewriteRule<ZeroUle>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<ZeroUle>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<ZeroUle>(" << node << ")" << std::endl;
return utils::mkTrue();
}
@@ -634,7 +634,7 @@ bool RewriteRule<UleMax>::applies(TNode node) {
template<> inline
Node RewriteRule<UleMax>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<UleMax>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<UleMax>(" << node << ")" << std::endl;
return utils::mkTrue();
}
@@ -652,7 +652,7 @@ bool RewriteRule<NotUlt>::applies(TNode node) {
template<> inline
Node RewriteRule<NotUlt>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<NotUlt>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<NotUlt>(" << node << ")" << std::endl;
Node ult = node[0];
Node a = ult[0];
Node b = ult[1];
@@ -673,7 +673,7 @@ bool RewriteRule<NotUle>::applies(TNode node) {
template<> inline
Node RewriteRule<NotUle>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<NotUle>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<NotUle>(" << node << ")" << std::endl;
Node ult = node[0];
Node a = ult[0];
Node b = ult[1];
@@ -701,7 +701,7 @@ bool RewriteRule<MultPow2>::applies(TNode node) {
template<> inline
Node RewriteRule<MultPow2>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<MultPow2>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<MultPow2>(" << node << ")" << std::endl;
std::vector<Node> children;
unsigned exponent = 0;
@@ -736,7 +736,7 @@ bool RewriteRule<NegIdemp>::applies(TNode node) {
template<> inline
Node RewriteRule<NegIdemp>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<NegIdemp>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<NegIdemp>(" << node << ")" << std::endl;
return node[0][0];
}
@@ -754,7 +754,7 @@ bool RewriteRule<UdivPow2>::applies(TNode node) {
template<> inline
Node RewriteRule<UdivPow2>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node << ")" << std::endl;
Node a = node[0];
unsigned power = utils::isPow2Const(node[1]) -1;
@@ -778,7 +778,7 @@ bool RewriteRule<UdivOne>::applies(TNode node) {
template<> inline
Node RewriteRule<UdivOne>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<UdivOne>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<UdivOne>(" << node << ")" << std::endl;
return node[0];
}
@@ -796,7 +796,7 @@ bool RewriteRule<UdivSelf>::applies(TNode node) {
template<> inline
Node RewriteRule<UdivSelf>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<UdivSelf>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<UdivSelf>(" << node << ")" << std::endl;
return utils::mkConst(utils::getSize(node), 1);
}
@@ -814,7 +814,7 @@ bool RewriteRule<UremPow2>::applies(TNode node) {
template<> inline
Node RewriteRule<UremPow2>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<UremPow2>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<UremPow2>(" << node << ")" << std::endl;
TNode a = node[0];
unsigned power = utils::isPow2Const(node[1]) - 1;
if (power == 0) {
@@ -839,7 +839,7 @@ bool RewriteRule<UremOne>::applies(TNode node) {
template<> inline
Node RewriteRule<UremOne>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<UremOne>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<UremOne>(" << node << ")" << std::endl;
return utils::mkConst(utils::getSize(node), 0);
}
@@ -857,7 +857,7 @@ bool RewriteRule<UremSelf>::applies(TNode node) {
template<> inline
Node RewriteRule<UremSelf>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<UremSelf>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<UremSelf>(" << node << ")" << std::endl;
return utils::mkConst(utils::getSize(node), 0);
}
@@ -877,7 +877,7 @@ bool RewriteRule<ShiftZero>::applies(TNode node) {
template<> inline
Node RewriteRule<ShiftZero>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<ShiftZero>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<ShiftZero>(" << node << ")" << std::endl;
return node[0];
}
@@ -905,7 +905,7 @@ bool RewriteRule<BBPlusNeg>::applies(TNode node) {
template<> inline
Node RewriteRule<BBPlusNeg>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RewriteRule<BBPlusNeg>(" << node << ")" << std::endl;
+ Debug("bv-rewrite") << "RewriteRule<BBPlusNeg>(" << node << ")" << std::endl;
std::vector<Node> children;
unsigned neg_count = 0;
@@ -944,7 +944,7 @@ Node RewriteRule<BBPlusNeg>::apply(TNode node) {
// template<> inline
// Node RewriteRule<BBFactorOut>::apply(TNode node) {
-// BVDebug("bv-rewrite") << "RewriteRule<BBFactorOut>(" << node << ")" << std::endl;
+// Debug("bv-rewrite") << "RewriteRule<BBFactorOut>(" << node << ")" << std::endl;
// std::hash_set<TNode, TNodeHashFunction> factors;
// for (unsigned i = 0; i < node.getNumChildren(); ++i) {
@@ -980,7 +980,7 @@ Node RewriteRule<BBPlusNeg>::apply(TNode node) {
// template<> inline
// Node RewriteRule<>::apply(TNode node) {
-// BVDebug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl;
+// Debug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl;
// return ;
// }
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 3f59be86d..7d851d0fb 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -24,12 +24,6 @@
#include <sstream>
#include "expr/node_manager.h"
-#ifdef CVC4_DEBUG
-#define BVDebug(x) Debug(x)
-#else
-#define BVDebug(x) if (false) Debug(x)
-#endif
-
namespace CVC4 {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback