diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/congruence_manager.cpp | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 6 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 2 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 2 | ||||
-rwxr-xr-x | src/theory/quantifiers/conjecture_generator.cpp | 2 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 2 | ||||
-rw-r--r-- | src/theory/shared_terms_database.cpp | 2 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 4 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 2 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 8 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 7 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 2 |
13 files changed, 24 insertions, 19 deletions
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<bool>(true)), d_falseNode(NodeManager::currentNM()->mkConst<bool>(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), |