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 | |
parent | 7006d5ba2f68c01638a2ab2c98a86b41dcf4467c (diff) |
Merged bit-vector and uf proof branch.
Diffstat (limited to 'src/theory')
33 files changed, 470 insertions, 262 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 508a4b323..cbcccd734 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -26,9 +26,10 @@ #include "smt_util/command.h" #include "theory/rewriter.h" #include "theory/theory_model.h" +#include "proof/theory_proof.h" +#include "proof/proof_manager.h" #include "theory/valuation.h" - using namespace std; namespace CVC4 { @@ -54,27 +55,28 @@ const bool d_solveWrite2 = false; TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, SmtGlobals* globals) - : Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, globals), - d_numRow("theory::arrays::number of Row lemmas", 0), - d_numExt("theory::arrays::number of Ext lemmas", 0), - d_numProp("theory::arrays::number of propagations", 0), - d_numExplain("theory::arrays::number of explanations", 0), - d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0), - d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0), - d_numGetModelValSplits("theory::arrays::number of getModelVal splits", 0), - d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0), - d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0), - d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0), - d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP" , true), + const LogicInfo& logicInfo, SmtGlobals* globals, + std::string name) + : Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, globals, name), + d_numRow(name + "theory::arrays::number of Row lemmas", 0), + d_numExt(name + "theory::arrays::number of Ext lemmas", 0), + d_numProp(name + "theory::arrays::number of propagations", 0), + d_numExplain(name + "theory::arrays::number of explanations", 0), + d_numNonLinear(name + "theory::arrays::number of calls to setNonLinear", 0), + d_numSharedArrayVarSplits(name + "theory::arrays::number of shared array var splits", 0), + d_numGetModelValSplits(name + "theory::arrays::number of getModelVal splits", 0), + d_numGetModelValConflicts(name + "theory::arrays::number of getModelVal conflicts", 0), + d_numSetModelValSplits(name + "theory::arrays::number of setModelVal splits", 0), + d_numSetModelValConflicts(name + "theory::arrays::number of setModelVal conflicts", 0), + d_ppEqualityEngine(u, name + "theory::arrays::TheoryArraysPP" , true), d_ppFacts(u), // d_ppCache(u), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), d_isPreRegistered(c), - d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual", true), + d_mayEqualEqualityEngine(c, name + "theory::arrays::TheoryArraysMayEqual", true), d_notify(*this), - d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays", true), + d_equalityEngine(d_notify, c, name + "theory::arrays::TheoryArrays", true), d_conflict(c, false), d_backtracker(c), d_infoMap(c, &d_backtracker), @@ -1385,7 +1387,8 @@ void TheoryArrays::check(Effort e) { weakEquivBuildCond(r[0], r[1], conjunctions); weakEquivBuildCond(r2[0], r[1], conjunctions); lemma = mkAnd(conjunctions, true); - d_out->lemma(lemma, false, false, true); + // LSH FIXME: which kind of arrays lemma is this + d_out->lemma(lemma, RULE_INVALID, false, false, true); d_readTableContext->pop(); return; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index f1b02d99e..88d83bfb9 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -128,7 +128,7 @@ class TheoryArrays : public Theory { TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, - SmtGlobals* globals); + SmtGlobals* globals, std::string name = ""); ~TheoryArrays(); void setMasterEqualityEngine(eq::EqualityEngine* eq); 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() { diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 2491aef3a..d5c12457a 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -22,6 +22,7 @@ #include "base/cvc4_assert.h" #include "smt/logic_exception.h" #include "theory/interrupted.h" +#include "proof/proof_manager.h" #include "util/resource_manager.h" namespace CVC4 { @@ -99,8 +100,10 @@ public: * assigned false), or else a literal by itself (in the case of a * unit conflict) which is assigned TRUE (and T-conflicting) in the * current assignment. + * @param pf - a proof of the conflict. This is only non-null if proofs + * are enabled. */ - virtual void conflict(TNode n) throw(AssertionException, UnsafeInterruptException) = 0; + virtual void conflict(TNode n, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException) = 0; /** * Propagate a theory literal. @@ -115,16 +118,31 @@ public: * been detected. (This requests a split.) * * @param n - a theory lemma valid at decision level 0 + * @param rule - the proof rule for this lemma * @param removable - whether the lemma can be removed at any point * @param preprocess - whether to apply more aggressive preprocessing * @param sendAtoms - whether to ensure atoms are sent to the theory * @return the "status" of the lemma, including user level at which * the lemma resides; the lemma will be removed when this user level pops */ - virtual LemmaStatus lemma(TNode n, bool removable = false, - bool preprocess = false, bool sendAtoms = false) - throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) = 0; + virtual LemmaStatus lemma(TNode n, ProofRule rule, + bool removable = false, + bool preprocess = false, + bool sendAtoms = false) + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; + + /** + * Variant of the lemma function that does not require providing a proof rule. + */ + virtual LemmaStatus lemma(TNode n, + bool removable = false, + bool preprocess = false, + bool sendAtoms = false) + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { + return lemma(n, RULE_INVALID, removable, preprocess, sendAtoms); + } + /** * Request a split on a new theory atom. This is equivalent to * calling lemma({OR n (NOT n)}). diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index c98429dd2..d89724cbd 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -40,7 +40,9 @@ static CVC4_THREADLOCAL(std::hash_set<Node, NodeHashFunction>*) s_rewriteStack = class RewriterInitializer { static RewriterInitializer s_rewriterInitializer; - RewriterInitializer() { Rewriter::init(); } + RewriterInitializer() { + Rewriter::init(); + } ~RewriterInitializer() { Rewriter::shutdown(); } };/* class RewriterInitializer */ @@ -190,7 +192,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // Incorporate the children if necessary if (rewriteStackTop.node.getNumChildren() > 0) { - rewriteStackTop.node = rewriteStackTop.builder; + Node rewritten = rewriteStackTop.builder; + rewriteStackTop.node = rewritten; rewriteStackTop.theoryId = theoryOf(rewriteStackTop.node); } @@ -208,7 +211,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { Assert(s_rewriteStack->find(response.node) == s_rewriteStack->end()); s_rewriteStack->insert(response.node); #endif - rewriteStackTop.node = rewriteTo(newTheoryId, response.node); + Node rewritten = rewriteTo(newTheoryId, response.node); + rewriteStackTop.node = rewritten; #ifdef CVC4_ASSERTIONS s_rewriteStack->erase(response.node); #endif diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 9e946f8d7..45c9b1936 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -50,8 +50,9 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){ Theory::Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, - SmtGlobals* globals) throw() + SmtGlobals* globals, std::string name) throw() : d_id(id) + , d_instanceName(name) , d_satContext(satContext) , d_userContext(userContext) , d_logicInfo(logicInfo) @@ -60,12 +61,12 @@ Theory::Theory(TheoryId id, context::Context* satContext, context::UserContext* , d_sharedTermsIndex(satContext, 0) , d_careGraph(NULL) , d_quantEngine(NULL) - , d_checkTime(statName(id, "checkTime")) - , d_computeCareGraphTime(statName(id, "computeCareGraphTime")) + , d_checkTime(getFullInstanceName() + "::checkTime") + , d_computeCareGraphTime(getFullInstanceName() + "::computeCareGraphTime") , d_sharedTerms(satContext) , d_out(&out) , d_valuation(valuation) - , d_proofEnabled(false) + , d_proofsEnabled(false) , d_globals(globals) { smtStatisticsRegistry()->registerStat(&d_checkTime); diff --git a/src/theory/theory.h b/src/theory/theory.h index f7d9ee6a0..2c3c66d8b 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -149,6 +149,11 @@ private: */ TheoryId d_id; + /** Name of this theory instance. Along with the TheoryId this should provide + * an unique string identifier for each instance of a Theory class. We need + * this to ensure unique statistics names over multiple theory instances. */ + std::string d_instanceName; + /** * The SAT search context for the Theory. */ @@ -204,12 +209,6 @@ protected: /** time spent in theory combination */ TimerStat d_computeCareGraphTime; - static std::string statName(TheoryId id, const char* statName) { - std::stringstream ss; - ss << "theory<" << id << ">::" << statName; - return ss.str(); - } - /** * The only method to add suff to the care graph. */ @@ -247,7 +246,7 @@ protected: */ Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, - SmtGlobals* globals) throw(); + SmtGlobals* globals, std::string name = "") throw(); // taking : No default. /** * This is called at shutdown time by the TheoryEngine, just before @@ -272,6 +271,12 @@ protected: Valuation d_valuation; /** + * Whether proofs are enabled + * + */ + bool d_proofsEnabled; + + /** * Returns the next assertion in the assertFact() queue. * * @return the next assertion in the assertFact() queue @@ -290,12 +295,6 @@ protected: void printFacts(std::ostream& os) const; void debugPrintFacts() const; - /** - * Whether proofs are enabled - * - */ - bool d_proofEnabled; - SmtGlobals* d_globals; public: @@ -416,6 +415,13 @@ public: return d_id; } + std::string getFullInstanceName() const { + std::stringstream ss; + ss << "theory<" << d_id << ">" << d_instanceName; + return ss.str(); + } + + /** * Get the SAT context associated to this Theory. */ @@ -855,7 +861,11 @@ public: */ virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL); - + /** + * Turn on proof-production mode. + */ + void produceProofs() { d_proofsEnabled = true; } + /** Returns a pointer to the globals copy the theory is using. */ SmtGlobals* globals() { return d_globals; } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 25eac2ed4..be2a89dbc 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -27,7 +27,7 @@ #include "options/options.h" #include "options/quantifiers_options.h" #include "proof/proof_manager.h" -#include "proof/proof_manager.h" +#include "proof/theory_proof.h" #include "smt/logic_exception.h" #include "smt_util/ite_removal.h" #include "smt_util/lemma_output_channel.h" @@ -54,8 +54,6 @@ using namespace CVC4::theory; namespace CVC4 { void TheoryEngine::finishInit() { - PROOF (ProofManager::initTheoryProof(); ); - // initialize the quantifiers engine d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this); @@ -157,6 +155,8 @@ TheoryEngine::TheoryEngine(context::Context* context, d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); + PROOF (ProofManager::currentPM()->initTheoryProofEngine(d_globals); ); + d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor()); smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded); @@ -377,7 +377,7 @@ void TheoryEngine::check(Theory::Effort effort) { printAssertions("theory::assertions::fulleffort"); } } - + // Note that we've discharged all the facts d_factsAsserted = false; @@ -414,7 +414,7 @@ void TheoryEngine::check(Theory::Effort effort) { // must build model at this point d_curr_model_builder->buildModel(d_curr_model, true); } - Trace("theory::assertions-model") << endl; + Trace("theory::assertions-model") << endl; if (Trace.isOn("theory::assertions-model")) { printAssertions("theory::assertions-model"); } @@ -486,7 +486,7 @@ void TheoryEngine::combineTheories() { // We need to split on it Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl; - lemma(equality.orNode(equality.notNode()), false, false, false, carePair.theory); + lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory); // This code is supposed to force preference to follow what the theory models already have // but it doesn't seem to make a big difference - need to explore more -Clark // if (true) { @@ -1371,7 +1371,12 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The } } -theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, bool preprocess, theory::TheoryId atomsTo) { +theory::LemmaStatus TheoryEngine::lemma(TNode node, + ProofRule rule, + bool negated, + bool removable, + bool preprocess, + theory::TheoryId atomsTo) { // For resource-limiting (also does a time check). // spendResource(); @@ -1420,10 +1425,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable } // assert to prop engine - d_propEngine->assertLemma(additionalLemmas[0], negated, removable, RULE_INVALID, node); + d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, node); for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]); - d_propEngine->assertLemma(additionalLemmas[i], false, removable, RULE_INVALID, node); + d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, node); } // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. @@ -1467,11 +1472,11 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { Node fullConflict = mkExplanation(explanationVector); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; Assert(properConflict(fullConflict)); - lemma(fullConflict, true, true, false, THEORY_LAST); + lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST); } else { // When only one theory, the conflict should need no processing Assert(properConflict(conflict)); - lemma(conflict, true, true, false, THEORY_LAST); + lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST); } } @@ -1483,27 +1488,27 @@ void TheoryEngine::staticInitializeBVOptions(const std::vector<Node>& assertions if (options::produceModels()) throw ModalException("Slicer does not currently support model generation. Use --bv-eq-slicer=off"); useSlicer = true; - + } else if (options::bitvectorEqualitySlicer() == bv::BITVECTOR_SLICER_OFF) { return; - + } else if (options::bitvectorEqualitySlicer() == bv::BITVECTOR_SLICER_AUTO) { if (options::incrementalSolving() || options::produceModels()) return; - useSlicer = true; + useSlicer = true; bv::utils::TNodeBoolMap cache; for (unsigned i = 0; i < assertions.size(); ++i) { - useSlicer = useSlicer && bv::utils::isCoreTerm(assertions[i], cache); + useSlicer = useSlicer && bv::utils::isCoreTerm(assertions[i], cache); } } - + if (useSlicer) { - bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV]; + bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV]; bv_theory->enableCoreTheorySlicer(); } - + } void TheoryEngine::ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) { @@ -1511,12 +1516,12 @@ void TheoryEngine::ppBvToBool(const std::vector<Node>& assertions, std::vector<N } bool TheoryEngine::ppBvAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) { - bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV]; - return bv_theory->applyAbstraction(assertions, new_assertions); + bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV]; + return bv_theory->applyAbstraction(assertions, new_assertions); } void TheoryEngine::mkAckermanizationAsssertions(std::vector<Node>& assertions) { - bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV]; + bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV]; bv_theory->mkAckermanizationAsssertions(assertions); } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 7cb15ca97..0bf00c079 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -269,8 +269,9 @@ class TheoryEngine { } } - void conflict(TNode conflictNode) throw(AssertionException, UnsafeInterruptException) { + void conflict(TNode conflictNode, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException) { Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; + Assert(pf == NULL); // theory shouldn't be producing proofs yet ++ d_statistics.conflicts; d_engine->d_outputChannelUsed = true; d_engine->conflict(conflictNode, d_theory); @@ -283,18 +284,23 @@ class TheoryEngine { return d_engine->propagate(literal, d_theory); } - theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false, bool sendAtoms = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) { + theory::LemmaStatus lemma(TNode lemma, + ProofRule rule, + bool removable = false, + bool preprocess = false, + bool sendAtoms = false) + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - return d_engine->lemma(lemma, false, removable, preprocess, sendAtoms ? d_theory : theory::THEORY_LAST); + return d_engine->lemma(lemma, rule, false, removable, preprocess, sendAtoms ? d_theory: theory::THEORY_LAST); } theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - return d_engine->lemma(lemma, false, removable, false, d_theory); + return d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory); } void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { @@ -304,7 +310,7 @@ class TheoryEngine { "A boolean variable asserted to be true to force a restart"); Trace("theory::restart") << "EngineOutputChannel<" << d_theory << ">::restart(" << restartVar << ")" << std::endl; ++ d_statistics.restartDemands; - lemma(restartVar, true); + lemma(restartVar, RULE_INVALID, true); } void requirePhase(TNode n, bool phase) @@ -436,7 +442,12 @@ class TheoryEngine { * @param removable can the lemma be remove (restrictions apply) * @param needAtoms if not THEORY_LAST, then */ - theory::LemmaStatus lemma(TNode node, bool negated, bool removable, bool preprocess, theory::TheoryId atomsTo); + theory::LemmaStatus lemma(TNode node, + ProofRule rule, + bool negated, + bool removable, + bool preprocess, + theory::TheoryId atomsTo); /** Enusre that the given atoms are send to the given theory */ void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory); diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index f0b616d62..6247833f8 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -71,7 +71,7 @@ public: void safePoint(uint64_t ammount) throw(Interrupted, AssertionException) {} - void conflict(TNode n) + void conflict(TNode n, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException) { push(CONFLICT, n); } @@ -87,7 +87,10 @@ public: push(PROPAGATE_AS_DECISION, n); } - LemmaStatus lemma(TNode n, bool removable, bool preprocess, bool sendAtoms) throw(AssertionException, UnsafeInterruptException) { + LemmaStatus lemma(TNode n, ProofRule rule, + bool removable = false, + bool preprocess = false, + bool sendAtoms = false) throw(AssertionException, UnsafeInterruptException) { push(LEMMA, n); return LemmaStatus(Node::null(), 0); } diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 828d53144..8df323992 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -314,10 +314,10 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) { // How many children are not constants yet d_subtermsToEvaluate[result] = t.getNumChildren(); for (unsigned i = 0; i < t.getNumChildren(); ++ i) { - if (isConstant(getNodeId(t[i]))) { - Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluates " << t[i] << std::endl; - subtermEvaluates(result); - } + if (isConstant(getNodeId(t[i]))) { + Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluates " << t[i] << std::endl; + subtermEvaluates(result); + } } } } else { @@ -335,7 +335,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) { } else if (d_constantsAreTriggers && d_isConstant[result]) { // Non-Boolean constants are trigger terms for all tags EqualityNodeId tId = getNodeId(t); - // Setup the new set + // Setup the new set Theory::Set newSetTags = 0; EqualityNodeId newSetTriggers[THEORY_LAST]; unsigned newSetTriggersSize = THEORY_LAST; @@ -629,12 +629,12 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl; const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized; // If it's interpreted and we can interpret - if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId]) { - // Get the actual term id - TNode term = d_nodes[funId]; - subtermEvaluates(getNodeId(term)); - } - // Check if there is an application with find arguments + if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId]) { + // Get the actual term id + TNode term = d_nodes[funId]; + subtermEvaluates(getNodeId(term)); + } + // Check if there is an application with find arguments EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind(); EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind(); FunctionApplication funNormalized(fun.type, aNormalized, bNormalized); @@ -972,7 +972,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st // If the nodes are the same, we're done if (t1Id == t2Id){ if( eqp ) { - eqp->d_node = d_nodes[t1Id]; + eqp->d_node = ProofManager::currentPM()->mkOp(d_nodes[t1Id]); } return; } @@ -1029,6 +1029,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st MergeReasonType reasonType = d_equalityEdges[currentEdge].getReasonType(); Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl; + Debug("equality") << d_name << " in currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl; EqProof * eqpc = NULL; //make child proof if a proof is being constructed @@ -1051,6 +1052,20 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st if( eqpc ){ eqpc->d_children.push_back( eqpc1 ); eqpc->d_children.push_back( eqpc2 ); + Debug("equality-pf") << "Congruence : " << d_nodes[currentNode] << " " << d_nodes[edgeNode] << std::endl; + if( d_nodes[currentNode].getKind()==kind::EQUAL ){ + //leave node null for now + eqpc->d_node = Node::null(); + }else{ + Debug("equality-pf") << d_nodes[f1.a] << " / " << d_nodes[f2.a] << ", " << d_nodes[f1.b] << " / " << d_nodes[f2.b] << std::endl; + if(d_nodes[f1.a].getKind() == kind::APPLY_UF || + d_nodes[f1.a].getKind() == kind::SELECT || + d_nodes[f1.a].getKind() == kind::STORE) { + eqpc->d_node = d_nodes[f1.a]; + } else { + eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF, ProofManager::currentPM()->mkOp(d_nodes[f1.a]), d_nodes[f1.b]); + } + } } Debug("equality") << pop; break; @@ -1103,13 +1118,14 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st // Construct the equality Debug("equality") << d_name << "::eq::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl; if( eqpc ){ - if( reasonType==MERGED_THROUGH_EQUALITY ){ + if(reasonType == MERGED_THROUGH_EQUALITY) { eqpc->d_node = d_equalityEdges[currentEdge].getReason(); - }else{ - //theory-specific proof rule : TODO - eqpc->d_id = reasonType; - //eqpc->d_node = d_equalityEdges[currentEdge].getNodeId(); + } else { + // theory-specific proof rule + eqpc->d_node = d_nodes[d_equalityEdges[currentEdge].getNodeId()].eqNode(d_nodes[currentNode]); + Debug("equality-pf") << "theory eq : " << eqpc->d_node << std::endl; } + eqpc->d_id = reasonType; } equalities.push_back(d_equalityEdges[currentEdge].getReason()); break; @@ -1120,13 +1136,32 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st currentEdge = bfsQueue[currentIndex].edgeId; currentIndex = bfsQueue[currentIndex].previousIndex; + //---from Morgan--- + if(eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) { + if(eqpc->d_node.isNull()) { + Assert(eqpc->d_children.size() == 1); + EqProof *p = eqpc; + eqpc = p->d_children[0]; + delete p; + } else { + Assert(eqpc->d_children.empty()); + } + } + //---end from Morgan--- + eqp_trans.push_back( eqpc ); } while (currentEdge != null_id); - if( eqp ){ - eqp->d_id = MERGED_THROUGH_TRANS; - eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() ); + if(eqp) { + if(eqp_trans.size() == 1) { + *eqp = *eqp_trans[0]; + delete eqp_trans[0]; + } else { + eqp->d_id = MERGED_THROUGH_TRANS; + eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() ); + eqp->d_node = NodeManager::currentNM()->mkNode(d_nodes[t1Id].getType().isBoolean() ? kind::IFF : kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]); + } } // Done @@ -2057,8 +2092,7 @@ bool EqClassIterator::isFinished() const { return d_current == null_id; } - -void EqProof::debug_print( const char * c, unsigned tb ){ +void EqProof::debug_print( const char * c, unsigned tb ) const{ for( unsigned i=0; i<tb; i++ ) { Debug( c ) << " "; } Debug( c ) << d_id << "("; if( !d_children.empty() || !d_node.isNull() ){ diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 87074aebc..9cfa16adf 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -879,8 +879,8 @@ public: MergeReasonType d_id; Node d_node; std::vector< EqProof * > d_children; - void debug_print( const char * c, unsigned tb = 0 ); -}; + void debug_print( const char * c, unsigned tb = 0 ) const; +};/* class EqProof */ } // Namespace eq } // Namespace theory diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index f0b50b778..888fa140f 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -21,6 +21,9 @@ typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRul operator COMBINED_CARDINALITY_CONSTRAINT 1 "combined cardinality constraint; parameter is a positive integer constant k that bounds the sum of the cardinalities of all sorts in the signature" typerule COMBINED_CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CombinedCardinalityConstraintTypeRule +parameterized PARTIAL_APPLY_UF APPLY_UF 1: "partial uninterpreted function application" +typerule PARTIAL_APPLY_UF ::CVC4::theory::uf::PartialTypeRule + operator CARDINALITY_VALUE 1 "cardinality value of sort S: first parameter is (any) term of sort S" typerule CARDINALITY_VALUE ::CVC4::theory::uf::CardinalityValueTypeRule diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index d5e18ed14..4f7a2667c 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -167,7 +167,8 @@ void SymmetryBreaker::Template::reset() { d_reps.clear(); } -SymmetryBreaker::SymmetryBreaker(context::Context* context) : +SymmetryBreaker::SymmetryBreaker(context::Context* context, + std::string name) : ContextNotifyObj(context), d_assertionsToRerun(context), d_rerunningAssertions(false), @@ -178,7 +179,10 @@ SymmetryBreaker::SymmetryBreaker(context::Context* context) : d_template(), d_normalizationCache(), d_termEqs(), - d_termEqsOnly() { + d_termEqsOnly(), + d_name(name), + d_stats(d_name) +{ } class SBGuard { @@ -461,7 +465,7 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) { Debug("ufsymm") << "UFSYMM =====================================================" << endl << "UFSYMM have " << d_permutations.size() << " permutation sets" << endl; if(!d_permutations.empty()) { - { TimerStat::CodeTimer codeTimer(d_initNormalizationTimer); + { TimerStat::CodeTimer codeTimer(d_stats.d_initNormalizationTimer); // normalize d_phi for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) { @@ -476,12 +480,12 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) { for(Permutations::iterator i = d_permutations.begin(); i != d_permutations.end(); ++i) { - ++d_permutationSetsConsidered; + ++(d_stats.d_permutationSetsConsidered); const Permutation& p = *i; Debug("ufsymm") << "UFSYMM looking at permutation: " << p << endl; size_t n = p.size() - 1; if(invariantByPermutations(p)) { - ++d_permutationSetsInvariant; + ++(d_stats.d_permutationSetsInvariant); selectTerms(p); set<Node> cts; while(!d_terms.empty() && cts.size() <= n) { @@ -539,11 +543,11 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) { Node d; if(disj.getNumChildren() > 1) { d = disj; - ++d_clauses; + ++(d_stats.d_clauses); } else { d = disj[0]; disj.clear(); - ++d_units; + ++(d_stats.d_units); } if(Debug.isOn("ufsymm")) { Debug("ufsymm") << "UFSYMM symmetry-breaking clause: " << d << endl; @@ -569,7 +573,7 @@ void SymmetryBreaker::guessPermutations() { } bool SymmetryBreaker::invariantByPermutations(const Permutation& p) { - TimerStat::CodeTimer codeTimer(d_invariantByPermutationsTimer); + TimerStat::CodeTimer codeTimer(d_stats.d_invariantByPermutationsTimer); // use d_phi Debug("ufsymm") << "UFSYMM invariantByPermutations()? " << p << endl; @@ -681,7 +685,7 @@ static bool isSubset(const T1& s, const T2& t) { } void SymmetryBreaker::selectTerms(const Permutation& p) { - TimerStat::CodeTimer codeTimer(d_selectTermsTimer); + TimerStat::CodeTimer codeTimer(d_stats.d_selectTermsTimer); // use d_phi, put into d_terms Debug("ufsymm") << "UFSYMM selectTerms(): " << p << endl; @@ -733,6 +737,35 @@ void SymmetryBreaker::selectTerms(const Permutation& p) { } } +SymmetryBreaker::Statistics::Statistics(std::string name) + : d_clauses(name + "theory::uf::symmetry_breaker::clauses", 0) + , d_units(name + "theory::uf::symmetry_breaker::units", 0) + , d_permutationSetsConsidered(name + "theory::uf::symmetry_breaker::permutationSetsConsidered", 0) + , d_permutationSetsInvariant(name + "theory::uf::symmetry_breaker::permutationSetsInvariant", 0) + , d_invariantByPermutationsTimer(name + "theory::uf::symmetry_breaker::timers::invariantByPermutations") + , d_selectTermsTimer(name + "theory::uf::symmetry_breaker::timers::selectTerms") + , d_initNormalizationTimer(name + "theory::uf::symmetry_breaker::timers::initNormalization") +{ + smtStatisticsRegistry()->registerStat(&d_clauses); + smtStatisticsRegistry()->registerStat(&d_units); + smtStatisticsRegistry()->registerStat(&d_permutationSetsConsidered); + smtStatisticsRegistry()->registerStat(&d_permutationSetsInvariant); + smtStatisticsRegistry()->registerStat(&d_invariantByPermutationsTimer); + smtStatisticsRegistry()->registerStat(&d_selectTermsTimer); + smtStatisticsRegistry()->registerStat(&d_initNormalizationTimer); +} + +SymmetryBreaker::Statistics::~Statistics() +{ + smtStatisticsRegistry()->unregisterStat(&d_clauses); + smtStatisticsRegistry()->unregisterStat(&d_units); + smtStatisticsRegistry()->unregisterStat(&d_permutationSetsConsidered); + smtStatisticsRegistry()->unregisterStat(&d_permutationSetsInvariant); + smtStatisticsRegistry()->unregisterStat(&d_invariantByPermutationsTimer); + smtStatisticsRegistry()->unregisterStat(&d_selectTermsTimer); + smtStatisticsRegistry()->unregisterStat(&d_initNormalizationTimer); +} + SymmetryBreaker::Terms::iterator SymmetryBreaker::selectMostPromisingTerm(Terms& terms) { // use d_phi diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index 763ced650..5523c1c0d 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -128,35 +128,30 @@ private: Node normInternal(TNode phi, size_t level); Node norm(TNode n); + std::string d_name; + // === STATISTICS === /** number of new clauses that come from the SymmetryBreaker */ - KEEP_STATISTIC(IntStat, - d_clauses, - "theory::uf::symmetry_breaker::clauses", 0); - /** number of new clauses that come from the SymmetryBreaker */ - KEEP_STATISTIC(IntStat, - d_units, - "theory::uf::symmetry_breaker::units", 0); - /** number of potential permutation sets we found */ - KEEP_STATISTIC(IntStat, - d_permutationSetsConsidered, - "theory::uf::symmetry_breaker::permutationSetsConsidered", 0); - /** number of invariant permutation sets we found */ - KEEP_STATISTIC(IntStat, - d_permutationSetsInvariant, - "theory::uf::symmetry_breaker::permutationSetsInvariant", 0); - /** time spent in invariantByPermutations() */ - KEEP_STATISTIC(TimerStat, - d_invariantByPermutationsTimer, - "theory::uf::symmetry_breaker::timers::invariantByPermutations"); - /** time spent in selectTerms() */ - KEEP_STATISTIC(TimerStat, - d_selectTermsTimer, - "theory::uf::symmetry_breaker::timers::selectTerms"); - /** time spent in initial round of normalization */ - KEEP_STATISTIC(TimerStat, - d_initNormalizationTimer, - "theory::uf::symmetry_breaker::timers::initNormalization"); + struct Statistics { + /** number of new clauses that come from the SymmetryBreaker */ + IntStat d_clauses; + IntStat d_units; + /** number of potential permutation sets we found */ + IntStat d_permutationSetsConsidered; + /** number of invariant permutation sets we found */ + IntStat d_permutationSetsInvariant; + /** time spent in invariantByPermutations() */ + TimerStat d_invariantByPermutationsTimer; + /** time spent in selectTerms() */ + TimerStat d_selectTermsTimer; + /** time spent in initial round of normalization */ + TimerStat d_initNormalizationTimer; + + Statistics(std::string name); + ~Statistics(); + }; + + Statistics d_stats; protected: @@ -167,7 +162,7 @@ protected: public: - SymmetryBreaker(context::Context* context); + SymmetryBreaker(context::Context* context, std::string name = ""); ~SymmetryBreaker() throw() {} void assertFormula(TNode phi); void apply(std::vector<Node>& newClauses); diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index e21b7ef7d..93a920f82 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -20,30 +20,34 @@ #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/uf_options.h" +#include "proof/proof_manager.h" +#include "proof/theory_proof.h" +#include "proof/uf_proof.h" #include "theory/theory_model.h" #include "theory/type_enumerator.h" #include "theory/uf/theory_uf_strong_solver.h" using namespace std; -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::uf; + +namespace CVC4 { +namespace theory { +namespace uf { /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, SmtGlobals* globals) - : Theory(THEORY_UF, c, u, out, valuation, logicInfo, globals), + const LogicInfo& logicInfo, SmtGlobals* globals, std::string name) + : Theory(THEORY_UF, c, u, out, valuation, logicInfo, globals, name), d_notify(*this), /* The strong theory solver can be notified by EqualityEngine::init(), * so make sure it's initialized first. */ d_thss(NULL), - d_equalityEngine(d_notify, c, "theory::uf::TheoryUF", true), + d_equalityEngine(d_notify, c, name + "theory::uf::TheoryUF", true), d_conflict(c, false), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), d_functionsTerms(c), - d_symb(u) + d_symb(u, name) { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_UF); @@ -204,27 +208,29 @@ Node TheoryUF::getNextDecisionRequest(){ } } -void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) { +void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf) { // Do the work bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; - eq::EqProof * eqp = d_proofEnabled ? new eq::EqProof : NULL; if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { - d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, eqp); + d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, pf); } else { - d_equalityEngine.explainPredicate(atom, polarity, assumptions, eqp); + d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf); } - //for now, just print debug - //TODO : send the proof outwards : d_out->conflict( lem, eqp ); - if( eqp ){ - eqp->debug_print("uf-pf"); + if( pf ){ + Debug("uf-pf") << std::endl; + pf->debug_print("uf-pf"); } } Node TheoryUF::explain(TNode literal) { + return explain(literal, NULL); +} + +Node TheoryUF::explain(TNode literal, eq::EqProof* pf) { Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl; std::vector<TNode> assumptions; - explain(literal, assumptions); + explain(literal, assumptions, pf); return mkAnd(assumptions); } @@ -508,13 +514,14 @@ void TheoryUF::computeCareGraph() { }/* TheoryUF::computeCareGraph() */ void TheoryUF::conflict(TNode a, TNode b) { - //TODO: create EqProof at this level if d_proofEnabled = true + eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL; if (a.getKind() == kind::CONST_BOOLEAN) { - d_conflictNode = explain(a.iffNode(b)); + d_conflictNode = explain(a.iffNode(b),pf); } else { - d_conflictNode = explain(a.eqNode(b)); + d_conflictNode = explain(a.eqNode(b),pf); } - d_out->conflict(d_conflictNode); + ProofUF * puf = d_proofsEnabled ? new ProofUF( pf ) : NULL; + d_out->conflict(d_conflictNode, puf); d_conflict = true; } @@ -541,3 +548,8 @@ void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { d_thss->assertDisequal(t1, t2, reason); } } + + +} /* namespace CVC4::theory::uf */ +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index aff78f53d..bd0016be7 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -128,9 +128,15 @@ private: /** * Explain why this literal is true by adding assumptions + * with proof (if "pf" is non-NULL). */ - void explain(TNode literal, std::vector<TNode>& assumptions); + void explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf); + /** + * Explain a literal, with proof (if "pf" is non-NULL). + */ + Node explain(TNode literal, eq::EqProof* pf); + /** Literals to propagate */ context::CDList<Node> d_literalsToPropagate; @@ -163,7 +169,7 @@ public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, - SmtGlobals* globals); + SmtGlobals* globals, std::string name = ""); ~TheoryUF(); diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 6faab8517..05b95e9e1 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -107,6 +107,14 @@ public: } };/* class CardinalityConstraintTypeRule */ +class PartialTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + return n.getOperator().getType().getRangeType(); + } +};/* class PartialTypeRule */ + class CardinalityValueTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) |