diff options
author | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
commit | 42b665f2a00643c81b42932fab1441987628c5a5 (patch) | |
tree | aa851e1fc4828f5a4d94ce0c11fa6d2d1199636f /src/theory/bv | |
parent | 7006d5ba2f68c01638a2ab2c98a86b41dcf4467c (diff) |
Merged bit-vector and uf proof branch.
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bitblast_strategies_template.h | 57 | ||||
-rw-r--r-- | src/theory/bv/bitblast_utils.h | 2 | ||||
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 13 | ||||
-rw-r--r-- | src/theory/bv/bv_eager_solver.cpp | 11 | ||||
-rw-r--r-- | src/theory/bv/bv_eager_solver.h | 5 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory.h | 3 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.cpp | 45 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.h | 7 | ||||
-rw-r--r-- | src/theory/bv/eager_bitblaster.cpp | 52 | ||||
-rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 37 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 14 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 8 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_core.h | 3 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h | 3 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 6 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 10 |
16 files changed, 169 insertions, 107 deletions
diff --git a/src/theory/bv/bitblast_strategies_template.h b/src/theory/bv/bitblast_strategies_template.h index 0990c2f29..bc022a02d 100644 --- a/src/theory/bv/bitblast_strategies_template.h +++ b/src/theory/bv/bitblast_strategies_template.h @@ -253,17 +253,17 @@ void DefaultAndBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { Assert(node.getKind() == kind::BITVECTOR_AND && bits.size() == 0); - - for(unsigned j = 0; j < utils::getSize(node); ++j) { - std::vector<T> and_j; - for (unsigned i = 0; i < node.getNumChildren(); ++i) { - std::vector<T> current; - bb->bbTerm(node[i], current); - and_j.push_back(current[j]); - Assert(utils::getSize(node) == current.size()); + + bb->bbTerm(node[0], bits); + std::vector<T> current; + for(unsigned j = 1; j < node.getNumChildren(); ++j) { + bb->bbTerm(node[j], current); + for (unsigned i = 0; i < utils::getSize(node); ++i) { + bits[i] = mkAnd(bits[i], current[i]); } - bits.push_back(mkAnd(and_j)); + current.clear(); } + Assert (bits.size() == utils::getSize(node)); } template <class T> @@ -272,17 +272,17 @@ void DefaultOrBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { Assert(node.getKind() == kind::BITVECTOR_OR && bits.size() == 0); - - for(unsigned j = 0; j < utils::getSize(node); ++j) { - std::vector<T> or_j; - for (unsigned i = 0; i < node.getNumChildren(); ++i) { - std::vector<T> current; - bb->bbTerm(node[i], current); - or_j.push_back(current[j]); - Assert(utils::getSize(node) == current.size()); + + bb->bbTerm(node[0], bits); + std::vector<T> current; + for(unsigned j = 1; j < node.getNumChildren(); ++j) { + bb->bbTerm(node[j], current); + for (unsigned i = 0; i < utils::getSize(node); ++i) { + bits[i] = mkOr(bits[i], current[i]); } - bits.push_back(mkOr(or_j)); + current.clear(); } + Assert (bits.size() == utils::getSize(node)); } template <class T> @@ -291,20 +291,17 @@ void DefaultXorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { Assert(node.getKind() == kind::BITVECTOR_XOR && bits.size() == 0); - - for(unsigned j = 0; j < utils::getSize(node); ++j) { - std::vector<T> first; - bb->bbTerm(node[0], first); - T bitj = first[j]; - - for (unsigned i = 1; i < node.getNumChildren(); ++i) { - std::vector<T> current; - bb->bbTerm(node[i], current); - bitj = mkXor(bitj, current[j]); - Assert(utils::getSize(node) == current.size()); + + bb->bbTerm(node[0], bits); + std::vector<T> current; + for(unsigned j = 1; j < node.getNumChildren(); ++j) { + bb->bbTerm(node[j], current); + for (unsigned i = 0; i < utils::getSize(node); ++i) { + bits[i] = mkXor(bits[i], current[i]); } - bits.push_back(bitj); + current.clear(); } + Assert (bits.size() == utils::getSize(node)); } template <class T> diff --git a/src/theory/bv/bitblast_utils.h b/src/theory/bv/bitblast_utils.h index a236c69e8..adaed31c1 100644 --- a/src/theory/bv/bitblast_utils.h +++ b/src/theory/bv/bitblast_utils.h @@ -221,7 +221,7 @@ inline void shiftAddMultiplier(const std::vector<T>&a, const std::vector<T>&b, s T carry_in = mkFalse<T>(); T carry_out; for(unsigned j = 0; j < res.size() -k; ++j) { - T aj = mkAnd(a[j], b[k]); + T aj = mkAnd(b[k], a[j]); carry_out = mkOr(mkAnd(res[j+k], aj), mkAnd( mkXor(res[j+k], aj), carry_in)); res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in); diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index ec76bb4f6..66eea0997 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -85,6 +85,8 @@ protected: TermDefMap d_termCache; ModelCache d_modelCache; + BitVectorProof * d_bvp; + void initAtomBBStrategies(); void initTermBBStrategies(); protected: @@ -105,7 +107,7 @@ public: bool hasBBTerm(TNode node) const; void getBBTerm(TNode node, Bits& bits) const; - void storeBBTerm(TNode term, const Bits& bits); + virtual 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 @@ -171,7 +173,9 @@ public: void bbAtom(TNode node); Node getBBAtom(TNode atom) const; void storeBBAtom(TNode atom, Node atom_bb); - bool hasBBAtom(TNode atom) const; + void storeBBTerm(TNode node, const Bits& bits); + bool hasBBAtom(TNode atom) const; + TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false); ~TLazyBitblaster() throw(); /** @@ -201,6 +205,7 @@ public: * constants to equivalence classes that don't already have them */ void collectModelInfo(TheoryModel* m, bool fullModel); + void setProofLog( BitVectorProof * bvp ); typedef TNodeSet::const_iterator vars_iterator; vars_iterator beginVars() { return d_variables.begin(); } @@ -277,9 +282,12 @@ public: bool hasBBAtom(TNode atom) const; void bbFormula(TNode formula); void storeBBAtom(TNode atom, Node atom_bb); + void storeBBTerm(TNode node, const Bits& bits); + bool assertToSat(TNode node, bool propagate = true); bool solve(); void collectModelInfo(TheoryModel* m, bool fullModel); + void setProofLog( BitVectorProof * bvp ); }; class BitblastingRegistrar: public prop::Registrar { @@ -406,6 +414,7 @@ template <class T> TBitblaster<T>::TBitblaster() : d_termCache() , d_modelCache() + , d_bvp( NULL ) { initAtomBBStrategies(); initTermBBStrategies(); diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index 66b1c4182..2af8d04d6 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -16,6 +16,7 @@ #include "options/bv_options.h" #include "theory/bv/bitblaster_template.h" +#include "proof/bitvector_proof.h" #include "theory/bv/bv_eager_solver.h" using namespace std; @@ -54,6 +55,12 @@ void EagerBitblastSolver::initialize() { d_aigBitblaster = new AigBitblaster(); } else { d_bitblaster = new EagerBitblaster(d_bv); + THEORY_PROOF( + if( d_bvp ){ + d_bitblaster->setProofLog( d_bvp ); + d_bvp->setBitblaster(d_bitblaster); + } + ); } } @@ -112,3 +119,7 @@ void EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) { AlwaysAssert(!d_useAig && d_bitblaster); d_bitblaster->collectModelInfo(m, fullModel); } + +void EagerBitblastSolver::setProofLog( BitVectorProof * bvp ) { + d_bvp = bvp; +} diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index ff13867cc..cfc84dae1 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -39,7 +39,9 @@ class EagerBitblastSolver { EagerBitblaster* d_bitblaster; AigBitblaster* d_aigBitblaster; bool d_useAig; - TheoryBV* d_bv; + + TheoryBV* d_bv; + BitVectorProof * d_bvp; public: EagerBitblastSolver(theory::bv::TheoryBV* bv); @@ -53,6 +55,7 @@ public: bool isInitialized(); void initialize(); void collectModelInfo(theory::TheoryModel* m, bool fullModel); + void setProofLog( BitVectorProof * bvp ); }; } diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 9a314fd6a..402dd6be3 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -74,6 +74,8 @@ protected: /** The bit-vector theory */ TheoryBV* d_bv; + /** proof log */ + BitVectorProof * d_bvp; AssertionQueue d_assertionQueue; context::CDO<uint32_t> d_assertionIndex; public: @@ -102,6 +104,7 @@ public: return res; } virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); } + virtual void setProofLog( BitVectorProof * bvp ) {} AssertionQueue::const_iterator assertionsBegin() { return d_assertionQueue.begin(); } AssertionQueue::const_iterator assertionsEnd() { return d_assertionQueue.end(); } }; diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index 9f8cb580c..e7630bb3f 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -24,6 +24,8 @@ #include "theory/bv/bv_subtheory_bitblast.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" +#include "proof/proof_manager.h" +#include "proof/bitvector_proof.h" using namespace std; using namespace CVC4::context; @@ -44,7 +46,8 @@ BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv) d_abstractionModule(NULL), d_quickCheck(options::bitvectorQuickXplain() ? new BVQuickCheck("bb", bv) : NULL), d_quickXplain(options::bitvectorQuickXplain() ? new QuickXPlain("bb", d_quickCheck) : NULL) -{} +{ +} BitblastSolver::~BitblastSolver() { delete d_quickXplain; @@ -232,40 +235,6 @@ Node BitblastSolver::getModelValue(TNode node) 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) { @@ -279,6 +248,12 @@ void BitblastSolver::setConflict(TNode conflict) { d_bv->setConflict(final_conflict); } +void BitblastSolver::setProofLog( BitVectorProof * bvp ) { + d_bitblaster->setProofLog( bvp ); + bvp->setBitblaster(d_bitblaster); +} + }/* namespace CVC4::theory::bv */ }/* namespace CVC4::theory */ }/* namespace CVC4 */ + diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 0e066eefb..c69069109 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -73,8 +73,9 @@ public: void bitblastQueue(); void setAbstraction(AbstractionModule* module); uint64_t computeAtomWeight(TNode atom); + void setProofLog( BitVectorProof * bvp ); }; -} -} -} +} /* namespace CVC4::theory::bv */ +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index 000abe62b..2e4f06c38 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -19,16 +19,13 @@ #include "options/bv_options.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" +#include "proof/bitvector_proof.h" #include "smt/smt_statistics_registry.h" #include "theory/bv/bitblaster_template.h" #include "theory/bv/theory_bv.h" #include "theory/theory_model.h" -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::bv; - namespace CVC4 { namespace theory { namespace bv { @@ -46,13 +43,19 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) d_bitblastingRegistrar = new BitblastingRegistrar(this); d_nullContext = new context::Context(); - d_satSolver = prop::SatSolverFactory::createMinisat( - d_nullContext, smtStatisticsRegistry(), "EagerBitblaster"); - d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, - d_nullContext, d_bv->globals()); - + d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, + smtStatisticsRegistry(), + "EagerBitblaster"); + d_cnfStream = new prop::TseitinCnfStream(d_satSolver, + d_bitblastingRegistrar, + d_nullContext, + d_bv->globals(), + options::proof(), + "EagerBitblaster"); + MinisatEmptyNotify* notify = new MinisatEmptyNotify(); d_satSolver->setNotify(notify); + d_bvp = NULL; } EagerBitblaster::~EagerBitblaster() { @@ -85,21 +88,34 @@ void EagerBitblaster::bbAtom(TNode node) { // the bitblasted definition of the atom Node normalized = Rewriter::rewrite(node); Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ? - Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) : - normalized; + d_atomBBStrategies[normalized.getKind()](normalized, this) : + normalized; + + if (!options::proof()) { + atom_bb = Rewriter::rewrite(atom_bb); + } + // asserting that the atom is true iff the definition holds Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb); - AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); - storeBBAtom(node, atom_definition); + AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); + storeBBAtom(node, atom_bb); d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null()); } void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) { - // no need to store the definition for the lazy bit-blaster - d_bbAtoms.insert(atom); + if( d_bvp ){ + d_bvp->registerAtomBB(atom.toExpr(), atom_bb.toExpr()); + } + d_bbAtoms.insert(atom); } +void EagerBitblaster::storeBBTerm(TNode node, const Bits& bits) { + if( d_bvp ){ d_bvp->registerTermBB(node.toExpr()); } + d_termCache.insert(std::make_pair(node, bits)); +} + + bool EagerBitblaster::hasBBAtom(TNode atom) const { return d_bbAtoms.find(atom) != d_bbAtoms.end(); } @@ -211,6 +227,12 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { } } +void EagerBitblaster::setProofLog( BitVectorProof * bvp ) { + d_bvp = bvp; + d_satSolver->setProofLog(bvp); + bvp->initCnfProof(d_cnfStream, d_nullContext); +} + bool EagerBitblaster::isSharedTerm(TNode node) { return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); } diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index 34a9418dd..9268e2152 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -25,7 +25,9 @@ #include "theory/bv/theory_bv.h" #include "theory/rewriter.h" #include "theory/theory_model.h" -#include "theory_bv_utils.h" +#include "proof/bitvector_proof.h" +#include "proof/proof_manager.h" +#include "theory/bv/theory_bv_utils.h" namespace CVC4 { namespace theory { @@ -51,8 +53,12 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, c, smtStatisticsRegistry(), name); d_nullRegistrar = new prop::NullRegistrar(); d_nullContext = new context::Context(); - d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar, - d_nullContext, d_bv->globals()); + d_cnfStream = new prop::TseitinCnfStream(d_satSolver, + d_nullRegistrar, + d_nullContext, + d_bv->globals(), + options::proof(), + "LazyBitblaster"); d_satSolverNotify = d_emptyNotify ? (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : @@ -127,8 +133,12 @@ void TLazyBitblaster::bbAtom(TNode node) { // the bitblasted definition of the atom Node normalized = Rewriter::rewrite(node); Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ? - Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) : - normalized; + d_atomBBStrategies[normalized.getKind()](normalized, this) : normalized; + + if (!options::proof()) { + atom_bb = Rewriter::rewrite(atom_bb); + } + // asserting that the atom is true iff the definition holds Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb); storeBBAtom(node, atom_bb); @@ -136,10 +146,19 @@ void TLazyBitblaster::bbAtom(TNode node) { } void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) { - // no need to store the definition for the lazy bit-blaster + // No need to store the definition for the lazy bit-blaster (unless proofs are enabled). + if( d_bvp != NULL ){ + d_bvp->registerAtomBB(atom.toExpr(), atom_bb.toExpr()); + } d_bbAtoms.insert(atom); } +void TLazyBitblaster::storeBBTerm(TNode node, const Bits& bits) { + if( d_bvp ){ d_bvp->registerTermBB(node.toExpr()); } + d_termCache.insert(std::make_pair(node, bits)); +} + + bool TLazyBitblaster::hasBBAtom(TNode atom) const { return d_bbAtoms.find(atom) != d_bbAtoms.end(); } @@ -483,6 +502,12 @@ void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { } } +void TLazyBitblaster::setProofLog( BitVectorProof * bvp ){ + d_bvp = bvp; + d_satSolver->setProofLog( bvp ); + bvp->initCnfProof(d_cnfStream, d_nullContext); +} + void TLazyBitblaster::clearSolver() { Assert (d_ctx->getLevel() == 0); delete d_satSolver; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 4acd1b847..8f7e975cd 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -30,6 +30,8 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" +#include "proof/theory_proof.h" +#include "proof/proof_manager.h" #include "theory/valuation.h" using namespace CVC4::context; @@ -363,7 +365,6 @@ void TheoryBV::checkForLemma(TNode fact) { } } - void TheoryBV::check(Effort e) { if (done() && !fullEffort(e)) { @@ -706,6 +707,7 @@ Node TheoryBV::explain(TNode node) { // return the explanation Node explanation = utils::mkAnd(assumptions); Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl; + Debug("bitvector::explain") << "TheoryBV::explain done. \n"; return explanation; } @@ -796,6 +798,16 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector return changed; } +void TheoryBV::setProofLog( BitVectorProof * bvp ) { + if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER ){ + d_eagerSolver->setProofLog( bvp ); + }else{ + for( unsigned i=0; i< d_subtheories.size(); i++ ){ + d_subtheories[i]->setProofLog( bvp ); + } + } +} + void TheoryBV::setConflict(Node conflict) { if (options::bvAbstraction()) { Node new_conflict = d_abstractionModule->simplifyConflict(conflict); diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index e7e4d464f..27138abfc 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -87,7 +87,10 @@ public: void ppStaticLearn(TNode in, NodeBuilder<>& learned); void presolve(); - bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); + + bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); + + void setProofLog( BitVectorProof * bvp ); private: @@ -209,11 +212,10 @@ private: void sendConflict(); - void lemma(TNode node) { d_out->lemma(node); d_lemmasAdded = true; } + void lemma(TNode node) { d_out->lemma(node, RULE_CONFLICT); d_lemmasAdded = true; } void checkForLemma(TNode node); - friend class LazyBitblaster; friend class TLazyBitblaster; friend class EagerBitblaster; diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h index 676df5dde..185985b3b 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_core.h +++ b/src/theory/bv/theory_bv_rewrite_rules_core.h @@ -276,7 +276,8 @@ bool RewriteRule<ReflexivityEq>::applies(TNode node) { template<> inline Node RewriteRule<ReflexivityEq>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl; - return node[1].eqNode(node[0]); + Node res = node[1].eqNode(node[0]); + return res; } } 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 cd173a6dd..d5d6c39dd 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -325,7 +325,8 @@ Node RewriteRule<XnorEliminate>::apply(TNode node) { TNode a = node[0]; TNode b = node[1]; Node xorNode = utils::mkNode(kind::BITVECTOR_XOR, a, b); - return utils::mkNode(kind::BITVECTOR_NOT, xorNode); + Node result = utils::mkNode(kind::BITVECTOR_NOT, xorNode); + return result; } diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 3bf390ded..4d3b676c9 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -379,8 +379,8 @@ Node RewriteRule<XorZero>::apply(TNode node) { children.push_back(node[i]); } } - - return utils::mkNode(kind::BITVECTOR_XOR, children); + Node res = utils::mkNode(kind::BITVECTOR_XOR, children); + return res; } @@ -488,7 +488,7 @@ bool RewriteRule<NotIdemp>::applies(TNode node) { template<> inline Node RewriteRule<NotIdemp>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<XorIdemp>(" << node << ")" << std::endl; + Debug("bv-rewrite") << "RewriteRule<NotIdemp>(" << node << ")" << std::endl; return node[0][0]; } diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index ba8074fbb..993be309b 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -51,11 +51,11 @@ inline unsigned getSize(TNode node) { return node.getType().getBitVectorSize(); } -// this seems to behave strangely -inline const Integer& getBit(TNode node, unsigned i) { - Assert (0); - Assert (node.getKind() == kind::CONST_BITVECTOR); - return node.getConst<BitVector>().extract(i, i).getValue(); +inline const bool getBit(TNode node, unsigned i) { + Assert (i < utils::getSize(node) && + node.getKind() == kind::CONST_BITVECTOR); + Integer bit = node.getConst<BitVector>().extract(i, i).getValue(); + return (bit == 1u); } inline Node mkTrue() { |