diff options
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 31b44aa70..869e9100e 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -72,6 +72,12 @@ void TheoryModel::finishInit() { setSemiEvaluatedKind(kind::APPLY_UF); } + // Equal and not terms are not relevant terms. In other words, asserted + // equalities and negations of predicates (as terms) do not need to be sent + // to the model. Regardless, theories should send information to the model + // that ensures that all assertions are satisfied. + setIrrelevantKind(EQUAL); + setIrrelevantKind(NOT); } void TheoryModel::reset(){ @@ -627,6 +633,13 @@ void TheoryModel::setSemiEvaluatedKind(Kind k) d_semi_evaluated_kinds.insert(k); } +void TheoryModel::setIrrelevantKind(Kind k) { d_irrKinds.insert(k); } + +const std::set<Kind>& TheoryModel::getIrrelevantKinds() const +{ + return d_irrKinds; +} + bool TheoryModel::isLegalElimination(TNode x, TNode val) { return !expr::hasSubtermKinds(d_unevaluated_kinds, val); |