From: lianah Date: Fri, 15 Aug 2014 23:46:06 +0000 (-0400) Subject: Making getEqualityStatus more powerful for bit-vector theory. X-Git-Tag: cvc5-1.0.0~6666 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=866492a200cbbf069b6c3466e36c30ac13741ae3;p=cvc5.git Making getEqualityStatus more powerful for bit-vector theory. --- diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index ecd7013c7..ea31e3821 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -74,19 +74,22 @@ protected: typedef std::vector Bits; typedef __gnu_cxx::hash_map TermDefMap; typedef __gnu_cxx::hash_set TNodeSet; + typedef __gnu_cxx::hash_map ModelCache; typedef void (*TermBBStrategy) (TNode, Bits&, TBitblaster*); typedef T (*AtomBBStrategy) (TNode, TBitblaster*); // caches and mappings - TermDefMap d_termCache; - + TermDefMap d_termCache; + ModelCache d_modelCache; + void initAtomBBStrategies(); void initTermBBStrategies(); protected: /// function tables for the various bitblasting strategies indexed by node kind TermBBStrategy d_termBBStrategies[kind::LAST_KIND]; AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; + virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0; public: TBitblaster(); virtual ~TBitblaster() {} @@ -97,9 +100,18 @@ public: virtual bool hasBBAtom(TNode atom) const = 0; virtual void storeBBAtom(TNode atom, T atom_bb) = 0; + bool hasBBTerm(TNode node) const; void getBBTerm(TNode node, Bits& bits) const; - void storeBBTerm(TNode term, const Bits& bits); + void storeBBTerm(TNode term, const Bits& bits); + /** + * Return a constant representing the value of a in the model. + * If fullModel is true set unconstrained bits to 0. If not return + * NullNode() for a fully or partially unconstrained. + * + */ + Node getTermModel(TNode node, bool fullModel); + void invalidateModelCache(); }; @@ -109,7 +121,6 @@ class TLazyBitblaster : public TBitblaster { typedef std::vector Bits; typedef context::CDList AssertionList; typedef context::CDHashMap , prop::SatLiteralHashFunction> ExplanationMap; - /** This class gets callbacks from minisat on propagations */ class MinisatNotify : public prop::BVSatSolverInterface::Notify { prop::CnfStream* d_cnf; @@ -143,9 +154,12 @@ class TLazyBitblaster : public TBitblaster { TNodeSet d_bbAtoms; AbstractionModule* d_abstraction; bool d_emptyNotify; + + context::CDO d_satSolverFullModel; void addAtom(TNode atom); bool hasValue(TNode a); + Node getModelFromSatSolver(TNode a, bool fullModel); public: void bbTerm(TNode node, Bits& bits); void bbAtom(TNode node); @@ -172,14 +186,7 @@ public: void setAbstraction(AbstractionModule* abs); theory::EqualityStatus getEqualityStatus(TNode a, TNode b); - /** - * Return a constant Node representing the value of a variable - * in the current model. - * @param a - * - * @return - */ - Node getVarValue(TNode a, bool fullModel=true); + /** * Adds a constant value for each bit-blasted variable in the model. * @@ -245,7 +252,7 @@ class EagerBitblaster : public TBitblaster { TNodeSet d_bbAtoms; TNodeSet d_variables; - Node getVarValue(TNode a, bool fullModel); + Node getModelFromSatSolver(TNode a, bool fullModel); bool isSharedTerm(TNode node); public: @@ -299,7 +306,7 @@ class AigBitblaster : public TBitblaster { bool hasInput(TNode input); void convertToCnfAndAssert(); void assertToSatSolver(Cnf_Dat_t* pCnf); - + Node getModelFromSatSolver(TNode a, bool fullModel) { Unreachable(); } public: AigBitblaster(); ~AigBitblaster(); @@ -387,6 +394,7 @@ template void TBitblaster::initTermBBStrategies() { template TBitblaster::TBitblaster() : d_termCache() + , d_modelCache() { initAtomBBStrategies(); initTermBBStrategies(); @@ -407,6 +415,53 @@ void TBitblaster::storeBBTerm(TNode node, const Bits& bits) { d_termCache.insert(std::make_pair(node, bits)); } +template +void TBitblaster::invalidateModelCache() { + d_modelCache.clear(); +} + +template +Node TBitblaster::getTermModel(TNode node, bool fullModel) { + if (d_modelCache.find(node) != d_modelCache.end()) + return d_modelCache[node]; + + if (node.isConst()) + return node; + + Node value = getModelFromSatSolver(node, false); + if (!value.isNull()) { + Debug("bv-equality-status")<< "TLazyBitblaster::getTermModel from SatSolver" << node <<" => " << value <<"\n"; + d_modelCache[node] = value; + Assert (value.isConst()); + return value; + } + + if (Theory::isLeafOf(node, theory::THEORY_BV)) { + // if it is a leaf may ask for fullModel + value = getModelFromSatSolver(node, fullModel); + Debug("bv-equality-status")<< "TLazyBitblaster::getTermModel from VarValue" << node <<" => " << value <<"\n"; + Assert (!value.isNull()); + d_modelCache[node] = value; + return value; + } + Assert (node.getType().isBitVector()); + + NodeBuilder<> nb(node.getKind()); + if (node.getMetaKind() == kind::metakind::PARAMETERIZED) { + nb << node.getOperator(); + } + + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + nb << getTermModel(node[i], fullModel); + } + value = nb; + value = Rewriter::rewrite(value); + Assert (value.isConst()); + d_modelCache[node] = value; + Debug("bv-term-model")<< "TLazyBitblaster::getTermModel Building Value" << node <<" => " << value <<"\n"; + return value; +} + } /* bv namespace */ diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp index 5f35f95e3..b2b4eebdf 100644 --- a/src/theory/bv/bv_quick_check.cpp +++ b/src/theory/bv/bv_quick_check.cpp @@ -115,7 +115,7 @@ BVQuickCheck::vars_iterator BVQuickCheck::endVars() { } Node BVQuickCheck::getVarValue(TNode var) { - return d_bitblaster->getVarValue(var); + return d_bitblaster->getTermModel(var, true); } diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index a2a6e19ac..35542fc68 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -103,6 +103,7 @@ void BitblastSolver::bitblastQueue() { // don't bit-blast lemma atoms continue; } + Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n"; d_bitblaster->bbAtom(atom); } } @@ -218,48 +219,45 @@ void BitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) { Node BitblastSolver::getModelValue(TNode node) { - if (!d_validModelCache) { - d_modelCache.clear(); - d_validModelCache = true; - } - return getModelValueRec(node); -} - -Node BitblastSolver::getModelValueRec(TNode node) -{ - Node val; - if (node.isConst()) { - return node; - } - NodeMap::iterator it = d_modelCache.find(node); - if (it != d_modelCache.end()) { - val = (*it).second; - Debug("bitvector-model") << node << " => (cached) " << val <<"\n"; - return val; - } - if (d_bv->isLeaf(node)) { - val = d_bitblaster->getVarValue(node); - if (val == Node()) { - // If no value in model, just set to 0 - val = utils::mkConst(utils::getSize(node), (unsigned)0); - } - } else { - NodeBuilder<> valBuilder(node.getKind()); - if (node.getMetaKind() == kind::metakind::PARAMETERIZED) { - valBuilder << node.getOperator(); - } - for (unsigned i = 0; i < node.getNumChildren(); ++i) { - valBuilder << getModelValueRec(node[i]); - } - val = valBuilder; - val = Rewriter::rewrite(val); - } - Assert(val.isConst()); - d_modelCache[node] = val; - Debug("bitvector-model") << node << " => " << val <<"\n"; + Node val = d_bitblaster->getTermModel(node, false); return val; } +// Node BitblastSolver::getModelValueRec(TNode node) +// { +// Node val; +// if (node.isConst()) { +// return node; +// } +// NodeMap::iterator it = d_modelCache.find(node); +// if (it != d_modelCache.end()) { +// val = (*it).second; +// Debug("bitvector-model") << node << " => (cached) " << val <<"\n"; +// return val; +// } +// if (d_bv->isLeaf(node)) { +// val = d_bitblaster->getVarValue(node); +// if (val == Node()) { +// // If no value in model, just set to 0 +// val = utils::mkConst(utils::getSize(node), (unsigned)0); +// } +// } else { +// NodeBuilder<> valBuilder(node.getKind()); +// if (node.getMetaKind() == kind::metakind::PARAMETERIZED) { +// valBuilder << node.getOperator(); +// } +// for (unsigned i = 0; i < node.getNumChildren(); ++i) { +// valBuilder << getModelValueRec(node[i]); +// } +// val = valBuilder; +// val = Rewriter::rewrite(val); +// } +// Assert(val.isConst()); +// d_modelCache[node] = val; +// Debug("bitvector-model") << node << " => " << val <<"\n"; +// return val; +// } + void BitblastSolver::setConflict(TNode conflict) { Node final_conflict = conflict; diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 414abdcce..77461163c 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -57,7 +57,7 @@ class BitblastSolver : public SubtheorySolver { AbstractionModule* d_abstractionModule; BVQuickCheck* d_quickCheck; QuickXPlain* d_quickXplain; - Node getModelValueRec(TNode node); + // Node getModelValueRec(TNode node); void setConflict(TNode conflict); public: BitblastSolver(context::Context* c, TheoryBV* bv); diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index e8fee00f5..38b9a1a0a 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -156,11 +156,11 @@ bool EagerBitblaster::solve() { * * @return */ -Node EagerBitblaster::getVarValue(TNode a, bool fullModel) { +Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) { if (!hasBBTerm(a)) { - Assert(isSharedTerm(a)); - return Node(); + return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node(); } + Bits bits; getBBTerm(a, bits); Integer value(0); @@ -171,7 +171,8 @@ Node EagerBitblaster::getVarValue(TNode a, bool fullModel) { bit_value = d_satSolver->value(bit); Assert (bit_value != prop::SAT_VALUE_UNKNOWN); } else { - // the bit is unconstrainted so we can give it an arbitrary value + if (!fullModel) return Node(); + // unconstrained bits default to false bit_value = prop::SAT_VALUE_FALSE; } Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0); @@ -182,19 +183,17 @@ Node EagerBitblaster::getVarValue(TNode a, bool fullModel) { void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { - TNodeSet::const_iterator it = d_variables.begin(); + TNodeSet::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, fullModel); - if(const_value == Node()) { - if( fullModel ){ - // if the value is unassigned just set it to zero - const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); - } - } + if (d_bv->isLeaf(var) || isSharedTerm(var)) { + // only shared terms could not have been bit-blasted + Assert (hasBBTerm(var) || isSharedTerm(var)); + + Node const_value = getModelFromSatSolver(var, fullModel); + if(const_value != Node()) { - Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= " + Debug("bitvector-model") << "EagerBitblaster::collectModelInfo (assert (= " << var << " " << const_value << "))\n"; m->assertEquality(var, const_value, true); diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index f721a22f0..101d8b082 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -41,6 +41,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const st , d_bbAtoms() , d_abstraction(NULL) , d_emptyNotify(emptyNotify) + , d_satSolverFullModel(c, false) , d_name(name) , d_statistics(name) { d_satSolver = prop::SatSolverFactory::createMinisat(c, name); @@ -258,6 +259,7 @@ bool TLazyBitblaster::solve() { } } Debug("bitvector") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms->size() <<"\n"; + d_satSolverFullModel.set(true); return prop::SAT_VALUE_TRUE == d_satSolver->solve(); } @@ -354,42 +356,38 @@ void TLazyBitblaster::MinisatNotify::safePoint() { d_bv->d_out->safePoint(); } + EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) { + Debug("bv-equality-status")<< "TLazyBitblaster::getEqualityStatus " << a <<" = " << b <<"\n"; + Debug("bv-equality-status")<< "BVSatSolver has full model? " << d_satSolverFullModel.get() <<"\n"; - // We don't want to bit-blast every possibly expensive term for the sake of equality checking - if (hasBBTerm(a) && hasBBTerm(b)) { - - Bits a_bits, b_bits; - getBBTerm(a, a_bits); - getBBTerm(b, b_bits); - theory::EqualityStatus status = theory::EQUALITY_TRUE_IN_MODEL; - for (unsigned i = 0; i < a_bits.size(); ++ i) { - if (d_cnfStream->hasLiteral(a_bits[i]) && d_cnfStream->hasLiteral(b_bits[i])) { - prop::SatLiteral a_lit = d_cnfStream->getLiteral(a_bits[i]); - prop::SatValue a_lit_value = d_satSolver->value(a_lit); - if (a_lit_value != prop::SAT_VALUE_UNKNOWN) { - prop::SatLiteral b_lit = d_cnfStream->getLiteral(b_bits[i]); - prop::SatValue b_lit_value = d_satSolver->value(b_lit); - if (b_lit_value != prop::SAT_VALUE_UNKNOWN) { - if (a_lit_value != b_lit_value) { - return theory::EQUALITY_FALSE_IN_MODEL; - } - } else { - status = theory::EQUALITY_UNKNOWN; - } - } { - status = theory::EQUALITY_UNKNOWN; - } - } else { - status = theory::EQUALITY_UNKNOWN; - } - } + // First check if it trivially rewrites to false/true + Node a_eq_b = Rewriter::rewrite(utils::mkNode(kind::EQUAL, a, b)); - return status; + if (a_eq_b == utils::mkFalse()) return theory::EQUALITY_FALSE; + if (a_eq_b == utils::mkTrue()) return theory::EQUALITY_TRUE; - } else { - return theory::EQUALITY_UNKNOWN; + if (!d_satSolverFullModel.get()) + return theory::EQUALITY_UNKNOWN; + + // Check if cache is valid (invalidated in check and pops) + if (d_bv->d_invalidateModelCache.get()) { + invalidateModelCache(); } + d_bv->d_invalidateModelCache.set(false); + + Node a_value = getTermModel(a, true); + Node b_value = getTermModel(b, true); + + Assert (a_value.isConst() && + b_value.isConst()); + + if (a_value == b_value) { + Debug("bv-equality-status")<< "theory::EQUALITY_TRUE_IN_MODEL\n"; + return theory::EQUALITY_TRUE_IN_MODEL; + } + Debug("bv-equality-status")<< "theory::EQUALITY_FALSE_IN_MODEL\n"; + return theory::EQUALITY_FALSE_IN_MODEL; } @@ -424,11 +422,11 @@ bool TLazyBitblaster::hasValue(TNode a) { * * @return */ -Node TLazyBitblaster::getVarValue(TNode a, bool fullModel) { +Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) { if (!hasBBTerm(a)) { - Assert(isSharedTerm(a)); - return Node(); + return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node(); } + Bits bits; getBBTerm(a, bits); Integer value(0); @@ -439,7 +437,8 @@ Node TLazyBitblaster::getVarValue(TNode a, bool fullModel) { bit_value = d_satSolver->value(bit); Assert (bit_value != prop::SAT_VALUE_UNKNOWN); } else { - // the bit is unconstrainted so we can give it an arbitrary value + if (!fullModel) return Node(); + // unconstrained bits default to false bit_value = prop::SAT_VALUE_FALSE; } Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0); @@ -449,23 +448,26 @@ Node TLazyBitblaster::getVarValue(TNode a, bool fullModel) { } void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { - TNodeSet::iterator it = d_variables.begin(); - for (; it!= d_variables.end(); ++it) { + std::set termSet; + d_bv->computeRelevantTerms(termSet); + + for (std::set::const_iterator it = termSet.begin(); it != termSet.end(); ++it) { TNode var = *it; - if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { - Node const_value = getVarValue(var, fullModel); - if(const_value == Node()) { - 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") << "TLazyBitblaster::collectModelInfo (assert (= " - << var << " " - << const_value << "))\n"; + // not actually a leaf of the bit-vector theory + if (d_variables.find(var) == d_variables.end()) + continue; + + Assert (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)); + // only shared terms could not have been bit-blasted + Assert (hasBBTerm(var) || isSharedTerm(var)); + + Node const_value = getModelFromSatSolver(var, fullModel); + Assert (const_value.isNull() || const_value.isConst()); + if(const_value != Node()) { + Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= " + << var << " " + << const_value << "))\n"; m->assertEquality(var, const_value, true); - } } } } @@ -481,7 +483,7 @@ void TLazyBitblaster::clearSolver() { d_bbAtoms.clear(); d_variables.clear(); d_termCache.clear(); - + // recreate sat solver d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx); d_cnfStream = new prop::TseitinCnfStream(d_satSolver, diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 4abf25bb1..40bc2417b 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -49,6 +49,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_staticLearnCache(), d_lemmasAdded(c, false), d_conflict(c, false), + d_invalidateModelCache(c, true), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), d_propagatedBy(c), @@ -357,7 +358,8 @@ void TheoryBV::checkForLemma(TNode fact) { void TheoryBV::check(Effort e) { Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; - + // we may be getting new assertions so the model cache may not be sound + d_invalidateModelCache.set(true); // if we are using the eager solver if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { // this can only happen on an empty benchmark diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 22d9f6775..a37a4019e 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -141,6 +141,9 @@ private: // Are we in conflict? context::CDO d_conflict; + // Invalidate the model cache if check was called + context::CDO d_invalidateModelCache; + /** The conflict node */ Node d_conflictNode;