diff options
author | Dejan Jovanovic <dejan.jovanovic@gmail.com> | 2014-12-26 19:15:13 -0800 |
---|---|---|
committer | Dejan Jovanovic <dejan.jovanovic@gmail.com> | 2014-12-26 19:15:13 -0800 |
commit | 0c624b4f57c5f1bc3c94058fe5b1da4bdd724041 (patch) | |
tree | d582a79203d9cc8f6ace757b8f9a729102d9f657 /src/theory/theory_engine.cpp | |
parent | 9e50f189118d5f8bb0f7eb54f19677e52f5a3852 (diff) |
Adding an option to the equality engine constructor to treat all constants as
trigger terms. I've disabled constants as triggers for all equality engines
except for the shared terms engine where it is needed.
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 9d91c096a..22bf37470 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -74,7 +74,7 @@ void TheoryEngine::finishInit() { if (d_logicInfo.isQuantified()) { d_quantEngine->finishInit(); Assert(d_masterEqualityEngine == 0); - d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master"); + d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master", false); for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { if (d_theoryTable[theoryId]) { @@ -1201,7 +1201,7 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { } Node TheoryEngine::getModelValue(TNode var) { - if(var.isConst()) return var; // FIXME: HACK!!! + if (var.isConst()) return var; // FIXME: HACK!!! Assert(d_sharedTerms.isShared(var)); return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var); } |