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_model.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_model.cpp')
| -rw-r--r-- | src/theory/theory_model.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index cb50bf355..7d385c398 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -34,7 +34,7 @@ TheoryModel::TheoryModel(context::Context* c, std::string name, bool enableFuncM d_false = NodeManager::currentNM()->mkConst( false ); d_eeContext = new context::Context(); - d_equalityEngine = new eq::EqualityEngine(d_eeContext, name); + d_equalityEngine = new eq::EqualityEngine(d_eeContext, name, false); // The kinds we are treating as function application in congruence d_equalityEngine->addFunctionKind(kind::APPLY_UF); |