From 8aaee8d5acce9887329f3e5a6fdeb425e428ec79 Mon Sep 17 00:00:00 2001 From: lianah Date: Mon, 4 Feb 2013 21:16:55 -0500 Subject: [PATCH] Fixing regression failure. The only unfixed ones seem model related which would require some graph coloring algorithm. --- src/theory/bv/bitblaster.cpp | 29 ++++++++++++++++++++----- src/theory/bv/bitblaster.h | 3 ++- src/theory/bv/bv_subtheory_bitblast.cpp | 16 +++----------- src/theory/bv/bv_subtheory_core.cpp | 9 +++++++- src/theory/bv/slicer.cpp | 1 + src/theory/bv/slicer.h | 3 ++- src/theory/bv/theory_bv.cpp | 6 ++++- src/theory/bv/theory_bv.h | 4 +++- 8 files changed, 47 insertions(+), 24 deletions(-) diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index 91482526a..cc589c5c3 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(); } @@ -412,6 +412,23 @@ bool Bitblaster::isSharedTerm(TNode node) { 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()); + Bits bits = d_termCache[a]; + for (int i = bits.size() -1; i >= 0; --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; + } else { + return false; + } + } + return true; +} + Node Bitblaster::getVarValue(TNode a) { Assert (d_termCache.find(a) != d_termCache.end()); Bits bits = d_termCache[a]; @@ -436,7 +453,7 @@ void Bitblaster::collectModelInfo(TheoryModel* m) { __gnu_cxx::hash_set::iterator it = d_variables.begin(); for (; it!= d_variables.end(); ++it) { TNode var = *it; - if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { + if ((Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) && hasValue(var)) { Node const_value = getVarValue(var); Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= " << var << " " diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h index fb4394673..84a67e884 100644 --- a/src/theory/bv/bitblaster.h +++ b/src/theory/bv/bitblaster.h @@ -124,7 +124,8 @@ class Bitblaster { // division is bitblasted in terms of constraints // so it needs to use private bitblaster interface void bbUdiv(TNode node, Bits& bits); - void bbUrem(TNode node, Bits& bits); + void bbUrem(TNode node, Bits& bits); + bool hasValue(TNode a); public: void cacheTermDef(TNode node, Bits def); // public so we can cache remainder for division void bbTerm(TNode node, Bits& bits); diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index e113048b8..985a9b500 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -53,18 +53,8 @@ void BitblastSolver::explain(TNode literal, std::vector& assumptions) { } bool BitblastSolver::addAssertions(const std::vector& assertions, Theory::Effort e) { - BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions (" << e << ")" << std::endl; - - //// Eager bit-blasting - if (options::bitvectorEagerBitblast()) { - for (unsigned i = 0; i < assertions.size(); ++i) { - TNode atom = assertions[i].getKind() == kind::NOT ? assertions[i][0] : assertions[i]; - if (atom.getKind() != kind::BITVECTOR_BITOF) { - d_bitblaster->bbAtom(atom); - } - } - return true; - } + Debug("bitvector::bitblaster") << "BitblastSolver::addAssertions (" << e << ")" << std::endl; + Debug("bitvector::bitblaster") << "number of assertions: " << assertions.size() << std::endl; //// Lazy bit-blasting @@ -106,7 +96,7 @@ bool BitblastSolver::addAssertions(const std::vector& 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 conflictAtoms; diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 1e74f86f2..a3290ff7c 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -157,7 +157,14 @@ bool CoreSolver::addAssertions(const std::vector& assertions, Theory::Eff if (d_isCoreTheory && !d_slicer->isCoreTerm(fact)) { d_isCoreTheory = false; } - ok = decomposeFact(fact); + + // only reason about equalities + // FIXME: should we slice when we have the terms in inequalities? + if (fact.getKind() == kind::EQUAL || (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) { + ok = decomposeFact(fact); + } else { + ok = assertFact(fact, fact); + } if (!ok) return false; } diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index 55402251d..87295e8f6 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -481,6 +481,7 @@ void Slicer::getBaseDecomposition(TNode node, std::vector& decomp) { current_low += current_size; decomp.push_back(current); } + // cache the result Debug("bv-slicer") << "as ["; for (unsigned i = 0; i < decomp.size(); ++i) { diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index f3b16e3d7..b0929d617 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -229,7 +229,8 @@ public: class Slicer { __gnu_cxx::hash_map d_idToNode; __gnu_cxx::hash_map d_nodeToId; - __gnu_cxx::hash_map d_coreTermCache; + __gnu_cxx::hash_map d_coreTermCache; + __gnu_cxx::hash_map, TNodeHashFunction> d_decompositionCache; UnionFind d_unionFind; ExtractTerm registerTerm(TNode node); public: diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 848063b76..bb4b480d6 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -41,6 +41,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_alreadyPropagatedSet(c), d_sharedTermsSet(c), d_slicer(), + d_bitblastAssertionsQueue(c), d_bitblastSolver(c, this), d_coreSolver(c, this, &d_slicer), d_statistics(), @@ -117,6 +118,7 @@ void TheoryBV::check(Effort e) Assertion assertion = get(); TNode fact = assertion.assertion; new_assertions.push_back(fact); + d_bitblastAssertionsQueue.push_back(fact); Debug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n"; } @@ -128,6 +130,9 @@ void TheoryBV::check(Effort e) if (!inConflict() && !d_coreSolver.isCoreTheory()) { // sending assertions to the bitblast solver if it's not just core theory d_bitblastSolver.addAssertions(new_assertions, e); + } else { + // sending assertions to the bitblast solver if it's not just core theory + d_bitblastSolver.addAssertions(new_assertions, EFFORT_STANDARD); } if (inConflict()) { @@ -140,7 +145,6 @@ void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){ // Assert (fullModel); // can only query full model d_coreSolver.collectModelInfo(m); d_bitblastSolver.collectModelInfo(m); - } void TheoryBV::propagate(Effort e) { diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index c16e854cc..ec72f40e1 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -47,9 +47,11 @@ class TheoryBV : public Theory { Slicer d_slicer; + context::CDQueue d_bitblastAssertionsQueue; + BitblastSolver d_bitblastSolver; CoreSolver d_coreSolver; - + public: TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); -- 2.30.2