From 040f30fe51dd767011af728d4d8ab83b75e4efd9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 28 Jun 2018 18:11:23 -0500 Subject: [PATCH] Remove comment about model value hack (#2118) This fixes #821. For some background, some special cases were added to equality engine and theory engine a few years ago to handle constants properly. As a result of these changes, a comment in the code was added about a HACK for getModelValue, but the code is completely reasonable looking to me (it says that the model value of a constant is itself). This PR removes that comment. From what I can tell issue #821 can be closed. --- src/theory/theory_engine.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 3977a9938..4aed35e75 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1483,7 +1483,11 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { } Node TheoryEngine::getModelValue(TNode var) { - if (var.isConst()) return var; // FIXME: HACK!!! + if (var.isConst()) + { + // the model value of a constant must be itself + return var; + } Assert(d_sharedTerms.isShared(var)); return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var); } -- 2.30.2