From 0c624b4f57c5f1bc3c94058fe5b1da4bdd724041 Mon Sep 17 00:00:00 2001 From: Dejan Jovanovic Date: Fri, 26 Dec 2014 19:15:13 -0800 Subject: [PATCH] Adding an option to the equality engine constructor to treat all constants as trigger terms. I've disabled constants as triggers for all equality engines except for the shared terms engine where it is needed. --- .cproject | 2 +- src/theory/arith/congruence_manager.cpp | 2 +- src/theory/arrays/theory_arrays.cpp | 6 +++--- src/theory/bv/bv_subtheory_core.cpp | 2 +- src/theory/datatypes/theory_datatypes.cpp | 2 +- src/theory/quantifiers/conjecture_generator.cpp | 2 +- src/theory/sets/theory_sets_private.cpp | 2 +- src/theory/shared_terms_database.cpp | 2 +- src/theory/strings/theory_strings.cpp | 2 +- src/theory/theory_engine.cpp | 4 ++-- src/theory/theory_model.cpp | 2 +- src/theory/uf/equality_engine.cpp | 8 +++++--- src/theory/uf/equality_engine.h | 7 +++++-- src/theory/uf/theory_uf.cpp | 2 +- 14 files changed, 25 insertions(+), 20 deletions(-) diff --git a/.cproject b/.cproject index cd310c481..fdbe0b295 100644 --- a/.cproject +++ b/.cproject @@ -18,7 +18,7 @@ - + diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index f2874f075..90029495b 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -34,7 +34,7 @@ ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDa d_constraintDatabase(cd), d_setupLiteral(setup), d_avariables(avars), - d_ee(d_notify, c, "theory::arith::ArithCongruenceManager") + d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", false) {} ArithCongruenceManager::Statistics::Statistics(): diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 8b313e124..94f3f573e 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -61,15 +61,15 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC 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"), + d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP" , false), d_ppFacts(u), // d_ppCache(u), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), d_isPreRegistered(c), - d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual"), + d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual", false), d_notify(*this), - d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays"), + d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays", false), d_conflict(c, false), d_backtracker(c), d_infoMap(c, &d_backtracker), diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 938a93b85..fc23347c6 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -32,7 +32,7 @@ using namespace CVC4::theory::bv::utils; CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv) : SubtheorySolver(c, bv), d_notify(*this), - d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"), + d_equalityEngine(d_notify, c, "theory::bv::TheoryBV", false), d_slicer(new Slicer()), d_isComplete(c, true), d_useSlicer(false), diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 0429c3aab..bf986a138 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -46,7 +46,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_infer(c), d_infer_exp(c), d_notify( *this ), - d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes"), + d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes", false), d_labels( c ), d_selector_apps( c ), //d_consEqc( c ), diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 2f8822b53..520ea5e70 100755 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -81,7 +81,7 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& ConjectureGenerator::ConjectureGenerator( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ), d_notify( *this ), -d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee"), +d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false), d_ee_conjectures( c ){ d_fullEffortCount = 0; d_uequalityEngine.addFunctionKind( kind::APPLY_UF ); diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index e229d3a6f..1892ecceb 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1086,7 +1086,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, context::UserContext* u): d_external(external), d_notify(*this), - d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate"), + d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate", false), d_trueNode(NodeManager::currentNM()->mkConst(true)), d_falseNode(NodeManager::currentNM()->mkConst(false)), d_conflict(c), diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 6e50cb82d..a41326350 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -29,7 +29,7 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, context::Co , d_alreadyNotifiedMap(context) , d_registeredEqualities(context) , d_EENotify(*this) -, d_equalityEngine(d_EENotify, context, "SharedTermsDatabase") +, d_equalityEngine(d_EENotify, context, "SharedTermsDatabase", true) , d_theoryEngine(theoryEngine) , d_inConflict(context, false) { diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 67b055d33..a2eb58cdc 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -37,7 +37,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo), RMAXINT(LONG_MAX), d_notify( *this ), - d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings"), + d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings", false), d_conflict(c, false), d_infer(c), d_infer_exp(c), diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 9d91c096a..22bf37470 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -74,7 +74,7 @@ void TheoryEngine::finishInit() { if (d_logicInfo.isQuantified()) { d_quantEngine->finishInit(); Assert(d_masterEqualityEngine == 0); - d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master"); + d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master", false); for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { if (d_theoryTable[theoryId]) { @@ -1201,7 +1201,7 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { } Node TheoryEngine::getModelValue(TNode var) { - if(var.isConst()) return var; // FIXME: HACK!!! + if (var.isConst()) return var; // FIXME: HACK!!! Assert(d_sharedTerms.isShared(var)); return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var); } diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index cb50bf355..7d385c398 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -34,7 +34,7 @@ TheoryModel::TheoryModel(context::Context* c, std::string name, bool enableFuncM d_false = NodeManager::currentNM()->mkConst( false ); d_eeContext = new context::Context(); - d_equalityEngine = new eq::EqualityEngine(d_eeContext, name); + d_equalityEngine = new eq::EqualityEngine(d_eeContext, name, false); // The kinds we are treating as function application in congruence d_equalityEngine->addFunctionKind(kind::APPLY_UF); diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 3b19270a4..42736a59b 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -79,7 +79,7 @@ EqualityEngine::~EqualityEngine() throw(AssertionException) { } -EqualityEngine::EqualityEngine(context::Context* context, std::string name) +EqualityEngine::EqualityEngine(context::Context* context, std::string name, bool constantsAreTriggers) : ContextNotifyObj(context) , d_masterEqualityEngine(0) , d_context(context) @@ -93,6 +93,7 @@ EqualityEngine::EqualityEngine(context::Context* context, std::string name) , d_subtermEvaluatesSize(context, 0) , d_stats(name) , d_inPropagate(false) +, d_constantsAreTriggers(constantsAreTriggers) , d_triggerDatabaseSize(context, 0) , d_triggerTermSetUpdatesSize(context, 0) , d_deducedDisequalitiesSize(context, 0) @@ -103,7 +104,7 @@ EqualityEngine::EqualityEngine(context::Context* context, std::string name) init(); } -EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name) +EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name, bool constantsAreTriggers) : ContextNotifyObj(context) , d_masterEqualityEngine(0) , d_context(context) @@ -117,6 +118,7 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c , d_subtermEvaluatesSize(context, 0) , d_stats(name) , d_inPropagate(false) +, d_constantsAreTriggers(constantsAreTriggers) , d_triggerDatabaseSize(context, 0) , d_triggerTermSetUpdatesSize(context, 0) , d_deducedDisequalitiesSize(context, 0) @@ -308,7 +310,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) { // We set this here as this only applies to actual terms, not the // intermediate application terms d_isBoolean[result] = true; - } else if (d_isConstant[result]) { + } else if (d_constantsAreTriggers && d_isConstant[result]) { // Non-Boolean constants are trigger terms for all tags EqualityNodeId tId = getNodeId(t); // Setup the new set diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 25092f37f..a26947ed1 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -165,12 +165,12 @@ public: /** * Initialize the equality engine, given the notification class. */ - EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name); + EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name, bool constantsAreTriggers); /** * Initialize the equality engine with no notification class. */ - EqualityEngine(context::Context* context, std::string name); + EqualityEngine(context::Context* context, std::string name, bool constantsAreTriggers); /** * Just a destructor. @@ -554,6 +554,9 @@ private: } };/* struct EqualityEngine::TriggerTermSet */ + /** Are the constants triggers */ + bool d_constantsAreTriggers; + /** The information about trigger terms is stored in this easily maintained memory. */ char* d_triggerDatabase; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 8fa7d2dbc..11242569a 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -34,7 +34,7 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& /* 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"), + d_equalityEngine(d_notify, c, "theory::uf::TheoryUF", false), d_conflict(c, false), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), -- 2.30.2