diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 1 | ||||
-rw-r--r-- | src/theory/arith/congruence_manager.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/congruence_manager.h | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 5 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_eq.cpp | 4 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_eq.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 5 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 2 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 4 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.h | 5 | ||||
-rw-r--r-- | src/theory/theory.h | 12 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 32 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 13 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 49 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 42 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 4 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 2 |
22 files changed, 170 insertions, 38 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7c913578b..03834825d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -554,6 +554,7 @@ void SmtEngine::finishInit() { d_theoryEngine->setPropEngine(d_propEngine); d_theoryEngine->setDecisionEngine(d_decisionEngine); + d_theoryEngine->finishInit(); // [MGD 10/20/2011] keep around in incremental mode, due to a // cleanup ordering issue and Nodes/TNodes. If SAT is popped diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 09410f15b..5ee250c09 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -65,6 +65,10 @@ ArithCongruenceManager::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_conflicts); } +void ArithCongruenceManager::setMasterEqualityEngine(eq::EqualityEngine* eq) { + d_ee.setMasterEqualityEngine(eq); +} + void ArithCongruenceManager::watchedVariableIsZero(Constraint lb, Constraint ub){ Assert(lb->isLowerBound()); Assert(ub->isUpperBound()); diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 502ea5cf0..5e2c80a63 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -144,6 +144,8 @@ public: return d_explanationMap.find(n) != d_explanationMap.end(); } + void setMasterEqualityEngine(eq::EqualityEngine* eq); + private: Node externalToInternal(TNode n) const{ Assert(canExplain(n)); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 141b22dc6..6ec6c7090 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -91,6 +91,10 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha TheoryArith::~TheoryArith(){} +void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) { + d_congruenceManager.setMasterEqualityEngine(eq); +} + Node skolemFunction(const std::string& name, TypeNode dom, TypeNode range){ NodeManager* currNM = NodeManager::currentNM(); TypeNode functionType = currNM->mkFunctionType(dom, range); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 0773ab7ba..ad041208d 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -341,6 +341,8 @@ public: */ void preRegisterTerm(TNode n); + void setMasterEqualityEngine(eq::EqualityEngine* eq); + void check(Effort e); void propagate(Effort e); Node explain(TNode n); diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index f40fea0ba..b8c1ace4b 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -111,7 +111,6 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC } } - TheoryArrays::~TheoryArrays() { StatisticsRegistry::unregisterStat(&d_numRow); @@ -124,6 +123,10 @@ TheoryArrays::~TheoryArrays() { } +void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine* eq) { + d_equalityEngine.setMasterEqualityEngine(eq); +} + ///////////////////////////////////////////////////////////////////////////// // PREPROCESSING diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index eaa3ca431..240cfad9a 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -123,6 +123,8 @@ class TheoryArrays : public Theory { TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); ~TheoryArrays(); + void setMasterEqualityEngine(eq::EqualityEngine* eq); + std::string identify() const { return std::string("TheoryArrays"); } ///////////////////////////////////////////////////////////////////////////// diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp index 17ea7034b..ca3e3e35c 100644 --- a/src/theory/bv/bv_subtheory_eq.cpp +++ b/src/theory/bv/bv_subtheory_eq.cpp @@ -67,6 +67,10 @@ EqualitySolver::EqualitySolver(context::Context* c, TheoryBV* bv) } } +void EqualitySolver::setMasterEqualityEngine(eq::EqualityEngine* eq) { + d_equalityEngine.setMasterEqualityEngine(eq); +} + void EqualitySolver::preRegister(TNode node) { if (!d_useEqualityEngine) return; diff --git a/src/theory/bv/bv_subtheory_eq.h b/src/theory/bv/bv_subtheory_eq.h index 64fe12706..2b024cfd4 100644 --- a/src/theory/bv/bv_subtheory_eq.h +++ b/src/theory/bv/bv_subtheory_eq.h @@ -63,7 +63,7 @@ class EqualitySolver : public SubtheorySolver { public: EqualitySolver(context::Context* c, TheoryBV* bv); - + void setMasterEqualityEngine(eq::EqualityEngine* eq); void preRegister(TNode node); bool addAssertions(const std::vector<TNode>& assertions, Theory::Effort e); void explain(TNode literal, std::vector<TNode>& assumptions); diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index a37ed59c8..7acb93cc2 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -50,6 +50,11 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& TheoryBV::~TheoryBV() {} + +void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { + d_equalitySolver.setMasterEqualityEngine(eq); +} + TheoryBV::Statistics::Statistics(): d_avgConflictSize("theory::bv::AvgBVConflictSize"), d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0), diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 933fd8700..0c8df3fca 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -50,6 +50,8 @@ public: TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); ~TheoryBV(); + void setMasterEqualityEngine(eq::EqualityEngine* eq); + void preRegisterTerm(TNode n); void check(Effort e); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 6b576cba8..8ec45efb9 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -56,6 +56,10 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, TheoryDatatypes::~TheoryDatatypes() { } +void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) { + d_equalityEngine.setMasterEqualityEngine(eq); +} + TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( Node n, bool doMake ){ std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n ); if( !hasEqcInfo( n ) ){ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 16e403e95..5cda9eeae 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -179,6 +179,9 @@ public: TheoryDatatypes(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); ~TheoryDatatypes(); + + void setMasterEqualityEngine(eq::EqualityEngine* eq); + /** propagate */ void propagate(Effort effort); /** propagate */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 6e704ba1c..446c9285e 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -36,17 +36,22 @@ using namespace CVC4::theory::quantifiers; TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, qe), - d_numRestarts(0){ + d_numRestarts(0), + d_masterEqualityEngine(0) +{ d_numInstantiations = 0; d_baseDecLevel = -1; out.handleUserAttribute( "axiom", this ); out.handleUserAttribute( "conjecture", this ); } - TheoryQuantifiers::~TheoryQuantifiers() { } +void TheoryQuantifiers::setMasterEqualityEngine(eq::EqualityEngine* eq) { + d_masterEqualityEngine = eq; +} + void TheoryQuantifiers::addSharedTerm(TNode t) { Debug("quantifiers-other") << "TheoryQuantifiers::addSharedTerm(): " << t << endl; diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 7b050bb1c..12b735497 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -31,6 +31,7 @@ namespace CVC4 { class TheoryEngine; namespace theory { + namespace quantifiers { class ModelEngine; @@ -49,10 +50,14 @@ private: KEEP_STATISTIC(TimerStat, d_theoryTime, "theory::quantifiers::theoryTime"); + eq::EqualityEngine* d_masterEqualityEngine; + public: TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); ~TheoryQuantifiers(); + void setMasterEqualityEngine(eq::EqualityEngine* eq); + void addSharedTerm(TNode t); void notifyEq(TNode lhs, TNode rhs); void preRegisterTerm(TNode n); diff --git a/src/theory/theory.h b/src/theory/theory.h index 95fe03c82..4d535a8af 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -54,6 +54,10 @@ namespace rrinst{ class CandidateGenerator; } +namespace eq { +class EqualityEngine; +} + /** * Information about an assertion for the theories. */ @@ -246,7 +250,8 @@ protected: * Construct a Theory. */ Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext, - OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) throw() + OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, + QuantifiersEngine* qe, eq::EqualityEngine* master = 0) throw() : d_id(id) , d_satContext(satContext) , d_userContext(userContext) @@ -515,6 +520,11 @@ public: virtual void addSharedTerm(TNode n) { } /** + * Called to set the master equality engine. + */ + virtual void setMasterEqualityEngine(eq::EqualityEngine* eq) { } + + /** * Return the current theory care graph. Theories should overload computeCareGraph to do * the actual computation, and use addCarePair to add pairs to the care graph. */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 4b4316db1..cd3b34879 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -42,12 +42,26 @@ #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/uf/equality_engine.h" using namespace std; using namespace CVC4; using namespace CVC4::theory; +void TheoryEngine::finishInit() { + if (d_logicInfo.isQuantified()) { + Assert(d_masterEqualityEngine == 0); + d_masterEqualityEngine = new eq::EqualityEngine(getSatContext(), "theory::master"); + + for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { + if (d_theoryTable[theoryId]) { + d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine); + } + } + } +} + TheoryEngine::TheoryEngine(context::Context* context, context::UserContext* userContext, RemoveITE& iteRemover, @@ -58,6 +72,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_userContext(userContext), d_logicInfo(logicInfo), d_sharedTerms(this, context), + d_masterEqualityEngine(NULL), d_quantEngine(NULL), d_curr_model(NULL), d_curr_model_builder(NULL), @@ -114,6 +129,8 @@ TheoryEngine::~TheoryEngine() { delete d_quantEngine; + delete d_masterEqualityEngine; + StatisticsRegistry::unregisterStat(&d_combineTheoriesTime); } @@ -229,21 +246,6 @@ void TheoryEngine::dumpAssertions(const char* tag) { } } - -template<typename T, bool doAssert> -class scoped_vector_clear { - vector<T>& d_v; -public: - scoped_vector_clear(vector<T>& v) - : d_v(v) { - Assert(!doAssert || d_v.empty()); - } - ~scoped_vector_clear() { - d_v.clear(); - } - -}; - /** * Check all (currently-active) theories for conflicts. * @param effort the effort level to use diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index d6e984f8f..de872db42 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -76,8 +76,13 @@ namespace theory { class Instantiator; class TheoryModel; class TheoryEngineModelBuilder; + + namespace eq { + class EqualityEngine; + } }/* CVC4::theory namespace */ + class DecisionEngine; /** @@ -124,6 +129,11 @@ class TheoryEngine { SharedTermsDatabase d_sharedTerms; /** + * Master equality engine, to share with theories. + */ + theory::eq::EqualityEngine* d_masterEqualityEngine; + + /** * The quantifiers engine */ theory::QuantifiersEngine* d_quantEngine; @@ -428,6 +438,9 @@ public: d_decisionEngine = decisionEngine; } + /** Called when all initialization of options/logic is done */ + void finishInit(); + /** * Get a pointer to the underlying propositional engine. */ diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 90de8d0d2..636427ed1 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -79,8 +79,9 @@ EqualityEngine::~EqualityEngine() throw(AssertionException) { } -EqualityEngine::EqualityEngine(context::Context* context, std::string name) +EqualityEngine::EqualityEngine(context::Context* context, std::string name) : ContextNotifyObj(context) +, d_masterEqualityEngine(0) , d_context(context) , d_done(context, false) , d_performNotify(true) @@ -102,6 +103,7 @@ EqualityEngine::EqualityEngine(context::Context* context, std::string name) EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name) : ContextNotifyObj(context) +, d_masterEqualityEngine(0) , d_context(context) , d_done(context, false) , d_performNotify(true) @@ -121,6 +123,11 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c init(); } +void EqualityEngine::setMasterEqualityEngine(EqualityEngine* master) { + Assert(d_masterEqualityEngine == 0); + d_masterEqualityEngine = master; +} + void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) { Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << ")" << std::endl; if (back) { @@ -294,6 +301,11 @@ void EqualityEngine::addTerm(TNode t) { d_nodeIndividualTrigger[tId] = newTriggerTermSet(); } + // If this is not an internal node, add it to the master + if (d_masterEqualityEngine && !d_isInternal[result]) { + d_masterEqualityEngine->addTerm(t); + } + propagate(); Debug("equality") << d_name << "::eq::addTerm(" << t << ") => " << result << std::endl; @@ -1213,9 +1225,34 @@ void EqualityEngine::propagate() { continue; } - // Depending on the merge preference (such as size, or being a constant), merge them + // Vector to collect the triggered events std::vector<TriggerId> triggers; - if ((node2.getSize() > node1.getSize() && !d_isConstant[t1classId]) || d_isConstant[t2classId]) { + + // Figure out the merge preference + EqualityNodeId mergeInto = t1classId; + if (d_isInternal[t2classId] != d_isInternal[t1classId]) { + // We always keep non-internal nodes as representatives: if any node in + // the class is non-internal, then the representative will be non-internal + if (d_isInternal[t1classId]) { + mergeInto = t2classId; + } else { + mergeInto = t1classId; + } + } else if (d_isConstant[t2classId] != d_isConstant[t1classId]) { + // We always keep constants as representatives: if any (at most one) node + // in the class in a constant, then the representative will be a constant + if (d_isConstant[t2classId]) { + mergeInto = t2classId; + } else { + mergeInto = t1classId; + } + } else if (node2.getSize() > node1.getSize()) { + // We always merge into the bigger class to reduce the amount of traversing + // we need to do + mergeInto = t2classId; + } + + if (mergeInto == t2classId) { Debug("equality") << d_name << "::eq::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl; d_assertedEqualities.push_back(Equality(t2classId, t1classId)); d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1; @@ -1231,6 +1268,12 @@ void EqualityEngine::propagate() { } } + // If not merging internal nodes, notify the master + if (d_masterEqualityEngine && !d_isInternal[mergeInto]) { + d_masterEqualityEngine->assertEqualityInternal(d_nodes[t1classId], d_nodes[t2classId], TNode::null()); + d_masterEqualityEngine->propagate(); + } + // Notify the triggers if (d_performNotify && !d_done) { for (size_t trigger_i = 0, trigger_end = triggers.size(); trigger_i < trigger_end && !d_done; ++ trigger_i) { diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 166362951..9bc2cb61c 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -151,8 +151,35 @@ class EqualityEngine : public context::ContextNotifyObj { /** Default implementation of the notification object */ static EqualityEngineNotifyNone s_notifyNone; + /** + * Master equality engine that gets all the equality information from + * this one, or null if none. + */ + EqualityEngine* d_masterEqualityEngine; + public: + /** + * Initialize the equality engine, given the notification class. + */ + EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name); + + /** + * Initialize the equality engine with no notification class. + */ + EqualityEngine(context::Context* context, std::string name); + + /** + * Just a destructor. + */ + virtual ~EqualityEngine() throw(AssertionException); + + /** + * Set the master equality engine for this one. Master engine will get copies of all + * the terms and equalities from this engine. + */ + void setMasterEqualityEngine(EqualityEngine* master); + /** Statistics about the equality engine instance */ struct Statistics { /** Total number of merges */ @@ -640,21 +667,6 @@ private: public: /** - * Initialize the equality engine, given the notification class. - */ - EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name); - - /** - * Initialize the equality engine with no notification class. - */ - EqualityEngine(context::Context* context, std::string name); - - /** - * Just a destructor. - */ - virtual ~EqualityEngine() throw(AssertionException); - - /** * Adds a term to the term database. */ void addTerm(TNode t); diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index d76d95adb..e6ae3747c 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -45,6 +45,10 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& d_equalityEngine.addFunctionKind(kind::APPLY_UF); } +void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) { + d_equalityEngine.setMasterEqualityEngine(eq); +} + static Node mkAnd(const std::vector<TNode>& conjunctions) { Assert(conjunctions.size() > 0); diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index f30619e2e..46a17a5e0 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -187,6 +187,8 @@ public: } } + void setMasterEqualityEngine(eq::EqualityEngine* eq); + void check(Effort); void preRegisterTerm(TNode term); Node explain(TNode n); |