From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 28 Jun 2018 23:11:23 +0000 (-0500)
Subject: Remove comment about model value hack (#2118)
X-Git-Tag: cvc5-1.0.0~4934
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=040f30fe51dd767011af728d4d8ab83b75e4efd9;p=cvc5.git

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 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);
 }