From 160134dc043c28308865d2b91648ba412d0749d4 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Wed, 3 Dec 2014 11:38:36 -0500 Subject: Revert "Disable constants sharing in eq engine, disable hack in theory engine." This partially reverts commit f70804a7159390fcb01d8c1ec208fbfd8e544fba. In particular, it DOES NOT revert "Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring. Fix assertion failure in quantifiers engine." which is part of the same commit. --- src/theory/theory_engine.cpp | 1 + src/theory/uf/equality_engine.cpp | 16 ++++++++++++++++ 2 files changed, 17 insertions(+) (limited to 'src') diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index eae76099e..9d91c096a 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1201,6 +1201,7 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { } Node TheoryEngine::getModelValue(TNode var) { + 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/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index d1f1e9ed3..3b19270a4 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -308,6 +308,22 @@ 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 -- cgit v1.2.3