diff options
author | Tim King <taking@cs.nyu.edu> | 2013-02-14 16:11:42 -0500 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-02-14 16:11:42 -0500 |
commit | fc4121b761dd524ad5fe37789381e5814737e6b9 (patch) | |
tree | fec292ebddd652d5938c7e9f266b52a4770bfae1 /src/theory/bv/bitblaster.cpp | |
parent | 63ca7c0a10dcd6b3be42d4d513f842db76733392 (diff) |
Removing BVDebug and replacing with Debug.
Diffstat (limited to 'src/theory/bv/bitblaster.cpp')
-rw-r--r-- | src/theory/bv/bitblaster.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
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(); } |