diff options
Diffstat (limited to 'src/theory/bv/bitblaster.cpp')
-rw-r--r-- | src/theory/bv/bitblaster.cpp | 196 |
1 files changed, 103 insertions, 93 deletions
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index 8579012ab..d17dd588f 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -12,7 +12,7 @@ ** \brief [[ Add one-line brief description here ]] ** ** [[ Add lengthier description here ]] - ** + ** **/ #include "bitblaster.h" @@ -29,7 +29,7 @@ using namespace std; using namespace CVC4::theory::bv::utils; -using namespace CVC4::context; +using namespace CVC4::context; using namespace CVC4::prop; namespace CVC4 { @@ -37,20 +37,20 @@ namespace theory { namespace bv{ std::string toString(Bits& bits) { - ostringstream os; + ostringstream os; for (int i = bits.size() - 1; i >= 0; --i) { TNode bit = bits[i]; if (bit.getKind() == kind::CONST_BOOLEAN) { os << (bit.getConst<bool>() ? "1" : "0"); } else { - os << bit<< " "; + os << bit<< " "; } } os <<"\n"; - - return os.str(); + + return os.str(); } -/////// Bitblaster +/////// Bitblaster Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) : d_bv(bv), @@ -64,38 +64,41 @@ Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) : d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar(), new Context()); MinisatNotify* notify = new MinisatNotify(d_cnfStream, bv); - d_satSolver->setNotify(notify); + d_satSolver->setNotify(notify); // initializing the bit-blasting strategies - initAtomBBStrategies(); - initTermBBStrategies(); + initAtomBBStrategies(); + initTermBBStrategies(); } Bitblaster::~Bitblaster() { delete d_cnfStream; - delete d_satSolver; + delete d_satSolver; } -/** +/** * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver * NOTE: duplicate clauses are not detected because of marker literal * @param node the atom to be bitblasted - * + * */ void Bitblaster::bbAtom(TNode node) { node = node.getKind() == kind::NOT? node[0] : node; - + if (hasBBAtom(node)) { - return; + return; } // make sure it is marked as an atom - addAtom(node); + addAtom(node); - Debug("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)); + Node normalized = Rewriter::rewrite(node); + Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ? + Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) : + normalized; // asserting that the atom is true iff the definition holds Node atom_definition = mkNode(kind::IFF, node, atom_bb); @@ -123,14 +126,14 @@ void Bitblaster::bbTerm(TNode node, Bits& bits) { return; } - Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; + Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; ++d_statistics.d_numTerms; d_termBBStrategies[node.getKind()] (node, bits,this); - + Assert (bits.size() == utils::getSize(node)); - cacheTermDef(node, bits); + cacheTermDef(node, bits); } Node Bitblaster::bbOptimize(TNode node) { @@ -139,21 +142,21 @@ Node Bitblaster::bbOptimize(TNode node) { if (node.getKind() == kind::BITVECTOR_PLUS) { if (RewriteRule<BBPlusNeg>::applies(node)) { Node res = RewriteRule<BBPlusNeg>::run<false>(node); - return res; + return res; } // if (RewriteRule<BBFactorOut>::applies(node)) { // Node res = RewriteRule<BBFactorOut>::run<false>(node); - // return res; - // } + // return res; + // } } else if (node.getKind() == kind::BITVECTOR_MULT) { if (RewriteRule<MultPow2>::applies(node)) { Node res = RewriteRule<MultPow2>::run<false>(node); - return res; + return res; } } - - return node; + + return node; } /// Public methods @@ -170,31 +173,31 @@ void Bitblaster::explain(TNode atom, std::vector<TNode>& explanation) { std::vector<SatLiteral> literal_explanation; d_satSolver->explain(d_cnfStream->getLiteral(atom), literal_explanation); for (unsigned i = 0; i < literal_explanation.size(); ++i) { - explanation.push_back(d_cnfStream->getNode(literal_explanation[i])); + explanation.push_back(d_cnfStream->getNode(literal_explanation[i])); } } -/** +/* * Asserts the clauses corresponding to the atom to the Sat Solver * by turning on the marker literal (i.e. setting it to false) * @param node the atom to be asserted - * + * */ - + bool Bitblaster::propagate() { return d_satSolver->propagate() == prop::SAT_VALUE_TRUE; } bool Bitblaster::assertToSat(TNode lit, bool propagate) { // strip the not - TNode atom; + TNode atom; if (lit.getKind() == kind::NOT) { - atom = lit[0]; + atom = lit[0]; } else { - atom = lit; + atom = lit; } - + Assert (hasBBAtom(atom)); SatLiteral markerLit = d_cnfStream->getLiteral(atom); @@ -202,9 +205,9 @@ bool Bitblaster::assertToSat(TNode lit, bool propagate) { if(lit.getKind() == kind::NOT) { markerLit = ~markerLit; } - + Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n"; - Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal: " << markerLit << "\n"; + Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal: " << markerLit << "\n"; SatValue ret = d_satSolver->assertAssumption(markerLit, propagate); @@ -214,13 +217,13 @@ bool Bitblaster::assertToSat(TNode lit, bool propagate) { return ret == prop::SAT_VALUE_TRUE; } -/** - * Calls the solve method for the Sat Solver. +/** + * Calls the solve method for the Sat Solver. * passing it the marker literals to be asserted - * + * * @return true for sat, and false for unsat */ - + bool Bitblaster::solve(bool quick_solve) { if (Trace.isOn("bitvector")) { Trace("bitvector") << "Bitblaster::solve() asserted atoms "; @@ -229,24 +232,24 @@ bool Bitblaster::solve(bool quick_solve) { Trace("bitvector") << " " << d_cnfStream->getNode(*it) << "\n"; } } - Debug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; - return SAT_VALUE_TRUE == d_satSolver->solve(); + Debug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; + return SAT_VALUE_TRUE == d_satSolver->solve(); } void Bitblaster::getConflict(std::vector<TNode>& conflict) { SatClause conflictClause; d_satSolver->getUnsatCore(conflictClause); - + for (unsigned i = 0; i < conflictClause.size(); i++) { - SatLiteral lit = conflictClause[i]; + SatLiteral lit = conflictClause[i]; TNode atom = d_cnfStream->getNode(lit); - Node not_atom; + Node not_atom; if (atom.getKind() == kind::NOT) { not_atom = atom[0]; } else { - not_atom = NodeManager::currentNM()->mkNode(kind::NOT, atom); + not_atom = NodeManager::currentNM()->mkNode(kind::NOT, atom); } - conflict.push_back(not_atom); + conflict.push_back(not_atom); } } @@ -256,9 +259,9 @@ void Bitblaster::getConflict(std::vector<TNode>& conflict) { void Bitblaster::initAtomBBStrategies() { for (int i = 0 ; i < kind::LAST_KIND; ++i ) { - d_atomBBStrategies[i] = UndefinedAtomBBStrategy; + d_atomBBStrategies[i] = UndefinedAtomBBStrategy; } - + /// setting default bb strategies for atoms d_atomBBStrategies [ kind::EQUAL ] = DefaultEqBB; d_atomBBStrategies [ kind::BITVECTOR_ULT ] = DefaultUltBB; @@ -269,7 +272,7 @@ void Bitblaster::initAtomBBStrategies() { d_atomBBStrategies [ kind::BITVECTOR_SLE ] = DefaultSleBB; d_atomBBStrategies [ kind::BITVECTOR_SGT ] = DefaultSgtBB; d_atomBBStrategies [ kind::BITVECTOR_SGE ] = DefaultSgeBB; - + } void Bitblaster::initTermBBStrategies() { @@ -278,7 +281,7 @@ void Bitblaster::initTermBBStrategies() { for (int i = 0 ; i < kind::LAST_KIND; ++i ) { d_termBBStrategies[i] = DefaultVarBB; } - + /// setting default bb strategies for terms: // d_termBBStrategies [ kind::VARIABLE ] = DefaultVarBB; d_termBBStrategies [ kind::CONST_BITVECTOR ] = DefaultConstBB; @@ -295,13 +298,13 @@ void Bitblaster::initTermBBStrategies() { d_termBBStrategies [ kind::BITVECTOR_PLUS ] = DefaultPlusBB; d_termBBStrategies [ kind::BITVECTOR_SUB ] = DefaultSubBB; d_termBBStrategies [ kind::BITVECTOR_NEG ] = DefaultNegBB; - d_termBBStrategies [ kind::BITVECTOR_UDIV ] = UndefinedTermBBStrategy; - d_termBBStrategies [ kind::BITVECTOR_UREM ] = UndefinedTermBBStrategy; + d_termBBStrategies [ kind::BITVECTOR_UDIV ] = UndefinedTermBBStrategy; + d_termBBStrategies [ kind::BITVECTOR_UREM ] = UndefinedTermBBStrategy; d_termBBStrategies [ kind::BITVECTOR_UDIV_TOTAL ] = DefaultUdivBB; d_termBBStrategies [ kind::BITVECTOR_UREM_TOTAL ] = DefaultUremBB; - d_termBBStrategies [ kind::BITVECTOR_SDIV ] = UndefinedTermBBStrategy; - d_termBBStrategies [ kind::BITVECTOR_SREM ] = UndefinedTermBBStrategy; - d_termBBStrategies [ kind::BITVECTOR_SMOD ] = UndefinedTermBBStrategy; + d_termBBStrategies [ kind::BITVECTOR_SDIV ] = UndefinedTermBBStrategy; + d_termBBStrategies [ kind::BITVECTOR_SREM ] = UndefinedTermBBStrategy; + d_termBBStrategies [ kind::BITVECTOR_SMOD ] = UndefinedTermBBStrategy; d_termBBStrategies [ kind::BITVECTOR_SHL ] = DefaultShlBB; d_termBBStrategies [ kind::BITVECTOR_LSHR ] = DefaultLshrBB; d_termBBStrategies [ kind::BITVECTOR_ASHR ] = DefaultAshrBB; @@ -313,22 +316,22 @@ void Bitblaster::initTermBBStrategies() { d_termBBStrategies [ kind::BITVECTOR_ROTATE_LEFT ] = DefaultRotateLeftBB; } - + bool Bitblaster::hasBBAtom(TNode atom) const { return d_bitblastedAtoms.find(atom) != d_bitblastedAtoms.end(); } void Bitblaster::cacheTermDef(TNode term, Bits def) { Assert (d_termCache.find(term) == d_termCache.end()); - d_termCache[term] = def; + d_termCache[term] = def; } bool Bitblaster::hasBBTerm(TNode node) const { - return d_termCache.find(node) != d_termCache.end(); + return d_termCache.find(node) != d_termCache.end(); } void Bitblaster::getBBTerm(TNode node, Bits& bits) const { - Assert (hasBBTerm(node)); + Assert (hasBBTerm(node)); // copy? bits = d_termCache.find(node)->second; } @@ -337,7 +340,7 @@ Bitblaster::Statistics::Statistics() : d_numTermClauses("theory::bv::NumberOfTermSatClauses", 0), d_numAtomClauses("theory::bv::NumberOfAtomSatClauses", 0), d_numTerms("theory::bv::NumberOfBitblastedTerms", 0), - d_numAtoms("theory::bv::NumberOfBitblastedAtoms", 0), + d_numAtoms("theory::bv::NumberOfBitblastedAtoms", 0), d_bitblastTimer("theory::bv::BitblastTimer") { StatisticsRegistry::registerStat(&d_numTermClauses); @@ -374,7 +377,7 @@ void Bitblaster::MinisatNotify::notify(prop::SatClause& clause) { }; void Bitblaster::MinisatNotify::safePoint() { - d_bv->d_out->safePoint(); + d_bv->d_out->safePoint(); } EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) { @@ -417,70 +420,77 @@ EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) { bool Bitblaster::isSharedTerm(TNode node) { - return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); + return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); } bool Bitblaster::hasValue(TNode a) { - Assert (d_termCache.find(a) != d_termCache.end()); + Assert (d_termCache.find(a) != d_termCache.end()); Bits bits = d_termCache[a]; for (int i = bits.size() -1; i >= 0; --i) { - SatValue bit_value; - if (d_cnfStream->hasLiteral(bits[i])) { + SatValue bit_value; + if (d_cnfStream->hasLiteral(bits[i])) { SatLiteral bit = d_cnfStream->getLiteral(bits[i]); bit_value = d_satSolver->value(bit); if (bit_value == SAT_VALUE_UNKNOWN) - return false; + return false; } else { - return false; + return false; } } - return true; + return true; } -/** +/** * Returns the value a is currently assigned to in the SAT solver - * or null if the value is completely unassigned. - * - * @param a - * - * @return + * or null if the value is completely unassigned. + * + * @param a + * @param fullModel whether to create a "full model," i.e., add + * constants to equivalence classes that don't already have them + * + * @return */ -Node Bitblaster::getVarValue(TNode a) { +Node Bitblaster::getVarValue(TNode a, bool fullModel) { if (d_termCache.find(a) == d_termCache.end()) { Assert(isSharedTerm(a)); - return Node(); + return Node(); } Bits bits = d_termCache[a]; - Integer value(0); + Integer value(0); for (int i = bits.size() -1; i >= 0; --i) { SatValue bit_value; - if (d_cnfStream->hasLiteral(bits[i])) { + if (d_cnfStream->hasLiteral(bits[i])) { SatLiteral bit = d_cnfStream->getLiteral(bits[i]); bit_value = d_satSolver->value(bit); - Assert (bit_value != SAT_VALUE_UNKNOWN); + Assert (bit_value != SAT_VALUE_UNKNOWN); } else { - // the bit is unconstrainted so we can give it an arbitrary value + //TODO: return Node() if fullModel=false? + // the bit is unconstrainted so we can give it an arbitrary value bit_value = SAT_VALUE_FALSE; } - Integer bit_int = bit_value == SAT_VALUE_TRUE ? Integer(1) : Integer(0); - value = value * 2 + bit_int; + Integer bit_int = bit_value == SAT_VALUE_TRUE ? Integer(1) : Integer(0); + value = value * 2 + bit_int; } - return utils::mkConst(BitVector(bits.size(), value)); + return utils::mkConst(BitVector(bits.size(), value)); } -void Bitblaster::collectModelInfo(TheoryModel* m) { +void Bitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { __gnu_cxx::hash_set<TNode, TNodeHashFunction>::iterator it = d_variables.begin(); for (; it!= d_variables.end(); ++it) { TNode var = *it; if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { - Node const_value = getVarValue(var); + Node const_value = getVarValue(var, fullModel); if(const_value == Node()) { - // if the value is unassigned just set it to zero - const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); + if( fullModel ){ + // if the value is unassigned just set it to zero + const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); + } + } + if(const_value != Node()) { + Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= " + << var << " " + << const_value << "))\n"; + m->assertEquality(var, const_value, true); } - Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= " - << var << " " - << const_value << "))\n"; - m->assertEquality(var, const_value, true); } } } |