diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-23 20:45:01 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-24 01:45:01 +0000 |
commit | 8f50a5600e0664330128d2ac824092a685ef965e (patch) | |
tree | ce3e08fbaa21cee663604e3da5981374d5b8da1a /src | |
parent | 47c9c2f42696a1e04577c1a79ac78f4186657818 (diff) |
Improve getValue for non-evaluated operators (#6436)
This makes it so that we attempt evaluation + rewriting on applications of operators that do not always evaluate, and return constants in case the evaluation was successful.
This fixes warnings for check-models on 43 of our regressions, and also uncovered one regression where our model was wrong but check-models silently succeeded. I've opened CVC4/cvc4-projects#276 for fixing the latter.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/theory_model.cpp | 35 |
1 files changed, 27 insertions, 8 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index d894ca571..40a64cb35 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -200,10 +200,13 @@ Node TheoryModel::getModelValue(TNode n) const Node ret = n; NodeManager* nm = NodeManager::currentNM(); - // if it is an evaluated kind, compute model values for children and evaluate - if (n.getNumChildren() > 0 - && d_unevaluated_kinds.find(nk) == d_unevaluated_kinds.end() - && d_semi_evaluated_kinds.find(nk) == d_semi_evaluated_kinds.end()) + // If it has children, evaluate them. We do this even if n is an unevaluatable + // or semi-unevaluatable operator. Notice this includes quantified + // formulas. It may not be possible in general to evaluate bodies of + // quantified formulas, because they have free variables. Regardless, we + // may often be able to evaluate the body of a quantified formula to true, + // e.g. forall x. P(x) where P = lambda x. true. + if (n.getNumChildren() > 0) { Debug("model-getvalue-debug") << "Get model value children " << n << std::endl; @@ -219,9 +222,17 @@ Node TheoryModel::getModelValue(TNode n) const children.push_back(n.getOperator()); } // evaluate the children - for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; ++i) + for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; ++i) { - ret = getModelValue(n[i]); + if (n.isClosure() && i==0) + { + // do not evaluate bound variable lists + ret = n[0]; + } + else + { + ret = getModelValue(n[i]); + } Debug("model-getvalue-debug") << " " << n << "[" << i << "] is " << ret << std::endl; children.push_back(ret); @@ -245,8 +256,16 @@ Node TheoryModel::getModelValue(TNode n) const ret = nm->mkConst( Rational(getCardinality(ret[0].getType()).getFiniteCardinality())); } - d_modelCache[n] = ret; - return ret; + // if the value was constant, we return it. If it was non-constant, + // we only return it if we an evaluated kind. This can occur if the + // children of n failed to evaluate. + if (ret.isConst() || ( + d_unevaluated_kinds.find(nk) == d_unevaluated_kinds.end() + && d_semi_evaluated_kinds.find(nk) == d_semi_evaluated_kinds.end())) + { + d_modelCache[n] = ret; + return ret; + } } // it might be approximate std::map<Node, Node>::const_iterator ita = d_approximations.find(n); |