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.

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 3977a993812b58b36e065ad0766a03318857f317..4aed35e75161c9dae451121cb8490f3d0a692ce4 100644 (file)
--- 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);
 }