diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-05-19 21:48:01 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-19 21:48:01 -0500 |
commit | af874a5c7a2ff134da0d4c20d06a0626d3e36d9b (patch) | |
tree | 16ad9de2b0c5753d2cd4cd3fcdd43bf8fbd55a71 /src/theory/theory_model.cpp | |
parent | 9712a20e6585728c7d0453e64e1e3b06a7d37b7f (diff) |
Do not eliminate variables that are equal to unevaluatable terms (#4267)
When we eliminate a variable x -> v during simplification, it may be the case that v contains "unevaluated" operators like forall, choice, etc. Thus, we do not produce correct models for such inputs unless simplification is disabled.
This PR ensures we only eliminate variables when v contains only evaluated operators.
Additionally, the kinds registered as unevaluated were slightly modified so that when we are in a logic like QF_LIA, there are no registered unevaluated operators, hence the check above is unnecessary. This is to minimize the performance impact of this change.
Fixes #4500.
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index f24e4fc66..567b5c4e4 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -13,6 +13,7 @@ **/ #include "theory/theory_model.h" +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/uf_options.h" @@ -56,7 +57,6 @@ TheoryModel::TheoryModel(context::Context* c, { setSemiEvaluatedKind(kind::APPLY_UF); } - setUnevaluatedKind(kind::BOUND_VARIABLE); } TheoryModel::~TheoryModel() @@ -203,19 +203,20 @@ Node TheoryModel::getModelValue(TNode n) const } Debug("model-getvalue-debug") << "Get model value " << n << " ... "; Debug("model-getvalue-debug") << d_equalityEngine->hasTerm(n) << std::endl; - if (n.isConst()) + Kind nk = n.getKind(); + if (n.isConst() || nk == BOUND_VARIABLE) { d_modelCache[n] = n; return n; } Node ret = n; - Kind nk = n.getKind(); NodeManager* nm = NodeManager::currentNM(); // if it is an evaluated kind, compute model values for children and evaluate if (n.getNumChildren() > 0 - && d_not_evaluated_kinds.find(nk) == d_not_evaluated_kinds.end()) + && d_unevaluated_kinds.find(nk) == d_unevaluated_kinds.end() + && d_semi_evaluated_kinds.find(nk) == d_semi_evaluated_kinds.end()) { Debug("model-getvalue-debug") << "Get model value children " << n << std::endl; @@ -308,10 +309,8 @@ Node TheoryModel::getModelValue(TNode n) const } // if we are a evaluated or semi-evaluated kind, return an arbitrary value - // if we are not in the d_not_evaluated_kinds map, we are evaluated - // if we are in the d_semi_evaluated_kinds, we are semi-evaluated - if (d_not_evaluated_kinds.find(nk) == d_not_evaluated_kinds.end() - || d_semi_evaluated_kinds.find(nk) != d_semi_evaluated_kinds.end()) + // if we are not in the d_unevaluated_kinds map, we are evaluated + if (d_unevaluated_kinds.find(nk) == d_unevaluated_kinds.end()) { if (t.isFunction() || t.isPredicate()) { @@ -617,17 +616,18 @@ void TheoryModel::recordModelCoreSymbol(Expr sym) d_model_core.insert(Node::fromExpr(sym)); } -void TheoryModel::setUnevaluatedKind(Kind k) -{ - d_not_evaluated_kinds.insert(k); -} +void TheoryModel::setUnevaluatedKind(Kind k) { d_unevaluated_kinds.insert(k); } void TheoryModel::setSemiEvaluatedKind(Kind k) { - d_not_evaluated_kinds.insert(k); d_semi_evaluated_kinds.insert(k); } +bool TheoryModel::isLegalElimination(TNode x, TNode val) +{ + return !expr::hasSubtermKinds(d_unevaluated_kinds, val); +} + bool TheoryModel::hasTerm(TNode a) { return d_equalityEngine->hasTerm( a ); |