diff options
| -rw-r--r-- | src/theory/theory_engine.cpp | 1 | ||||
| -rw-r--r-- | src/theory/uf/equality_engine.cpp | 16 |
2 files changed, 17 insertions, 0 deletions
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 |