diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-28 18:11:23 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-28 16:11:23 -0700 |
commit | 040f30fe51dd767011af728d4d8ab83b75e4efd9 (patch) | |
tree | 60efd16412042671b1ce21a61ceed9fdd2f80960 /src/theory/theory_engine.cpp | |
parent | 3aae63919df61895d956f9cca5049bfac7980b9c (diff) |
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.
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 6 |
1 files changed, 5 insertions, 1 deletions
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); } |