diff options
| author | Dejan Jovanovic <dejan.jovanovic@gmail.com> | 2014-12-26 19:15:13 -0800 |
|---|---|---|
| committer | Dejan Jovanovic <dejan.jovanovic@gmail.com> | 2014-12-26 19:15:13 -0800 |
| commit | 0c624b4f57c5f1bc3c94058fe5b1da4bdd724041 (patch) | |
| tree | d582a79203d9cc8f6ace757b8f9a729102d9f657 /src/theory/uf/equality_engine.cpp | |
| parent | 9e50f189118d5f8bb0f7eb54f19677e52f5a3852 (diff) | |
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.
Diffstat (limited to 'src/theory/uf/equality_engine.cpp')
| -rw-r--r-- | src/theory/uf/equality_engine.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
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 |