diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-20 10:56:20 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-20 10:59:46 +0100 |
commit | f70804a7159390fcb01d8c1ec208fbfd8e544fba (patch) | |
tree | a16f6ae65eda646ab5f80ef4633b3199c648d853 /src/theory/uf/equality_engine.cpp | |
parent | eebaff108e57f15cf19c78d3b9eb27ac1d90dc11 (diff) |
Disable constants sharing in eq engine, disable hack in theory engine. Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring. Fix assertion failure in quantifiers engine.
Diffstat (limited to 'src/theory/uf/equality_engine.cpp')
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 3b19270a4..d1f1e9ed3 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -308,22 +308,6 @@ 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]) { - // Non-Boolean constants are trigger terms for all tags - EqualityNodeId tId = getNodeId(t); - // Setup the new set - Theory::Set newSetTags = 0; - EqualityNodeId newSetTriggers[THEORY_LAST]; - unsigned newSetTriggersSize = THEORY_LAST; - for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++ currentTheory) { - newSetTags = Theory::setInsert(currentTheory, newSetTags); - newSetTriggers[currentTheory] = tId; - } - // Add it to the list for backtracking - d_triggerTermSetUpdates.push_back(TriggerSetUpdate(tId, null_set_id)); - d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1; - // Mark the the new set as a trigger - d_nodeIndividualTrigger[tId] = newTriggerTermSet(newSetTags, newSetTriggers, newSetTriggersSize); } // If this is not an internal node, add it to the master |