diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-16 11:23:54 -0600 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-16 09:23:54 -0800 |
commit | d15d44b3c91b5be2c19adac292f137d2a67eb848 (patch) | |
tree | 67f8cac1485c833970929ab10e216a1d69e8b48d /src/theory/evaluator.cpp | |
parent | 5ee3c8d02e21b1c20bfe56538c4cbe4fed0481eb (diff) |
Fix evaluator for non-evaluatable nodes (#3575)
This ensures that the Evaluator always returns the result of substitution + rewriting for constant substitutions.
This requires a few further extensions to the code, namely:
(1) Applying substutitions to operators,
(2) Reconstructing all nodes that fail to evaluate by taking into account evaluation of their children.
Diffstat (limited to 'src/theory/evaluator.cpp')
-rw-r--r-- | src/theory/evaluator.cpp | 166 |
1 files changed, 127 insertions, 39 deletions
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index 406fb5ead..b5fa79cd0 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -121,7 +121,21 @@ Node Evaluator::eval(TNode n, Trace("evaluator") << "Evaluating " << n << " under substitution " << args << " " << vals << std::endl; std::unordered_map<TNode, Node, NodeHashFunction> evalAsNode; - return evalInternal(n, args, vals, evalAsNode).toNode(); + Node ret = evalInternal(n, args, vals, evalAsNode).toNode(); + // if we failed to evaluate + if (ret.isNull()) + { + // should be stored in the evaluation-as-node map + std::unordered_map<TNode, Node, NodeHashFunction>::iterator itn = + evalAsNode.find(n); + Assert(itn != evalAsNode.end()); + ret = itn->second; + } + // should be the same as substitution + rewriting + Assert(ret + == Rewriter::rewrite( + n.substitute(args.begin(), args.end(), vals.begin(), vals.end()))); + return ret; } EvalResult Evaluator::evalInternal( @@ -133,9 +147,7 @@ EvalResult Evaluator::evalInternal( std::unordered_map<TNode, EvalResult, TNodeHashFunction> results; std::vector<TNode> queue; queue.emplace_back(n); - std::unordered_map<TNode, Node, NodeHashFunction>::iterator itn; std::unordered_map<TNode, EvalResult, TNodeHashFunction>::iterator itr; - NodeManager* nm = NodeManager::currentNM(); while (queue.size() != 0) { @@ -149,6 +161,20 @@ EvalResult Evaluator::evalInternal( bool doProcess = true; bool doEval = true; + if (currNode.getMetaKind() == kind::metakind::PARAMETERIZED) + { + TNode op = currNode.getOperator(); + itr = results.find(op); + if (itr == results.end()) + { + queue.emplace_back(op); + doProcess = false; + } + else if (itr->second.d_tag == EvalResult::INVALID) + { + doEval = false; + } + } for (const auto& currNodeChild : currNode) { itr = results.find(currNodeChild); @@ -172,6 +198,8 @@ EvalResult Evaluator::evalInternal( queue.pop_back(); Node currNodeVal = currNode; + // whether we need to reconstruct the current node in the case of failure + bool needsReconstruct = true; // The code below should either: // (1) store a valid EvalResult into results[currNode], or @@ -185,35 +213,8 @@ EvalResult Evaluator::evalInternal( // Reconstruct the node with a combination of the children that // successfully evaluated, and the children that did not. Trace("evaluator") << "Evaluator: collect arguments" << std::endl; - std::vector<Node> echildren; - if (currNode.getMetaKind() == kind::metakind::PARAMETERIZED) - { - echildren.push_back(currNode.getOperator()); - } - for (const auto& currNodeChild : currNode) - { - itr = results.find(currNodeChild); - if (itr->second.d_tag == EvalResult::INVALID) - { - // could not evaluate this child, look in the node cache - itn = evalAsNode.find(currNodeChild); - Assert(itn != evalAsNode.end()); - echildren.push_back(itn->second); - } - else - { - // otherwise, use the evaluation - echildren.push_back(itr->second.toNode()); - } - } - // The value is the result of our (partially) successful evaluation - // of the children. - currNodeVal = nm->mkNode(currNode.getKind(), echildren); - Trace("evaluator") << "Evaluator: partially evaluated " << currNodeVal - << std::endl; - // Use rewriting. Notice we do not need to substitute here since - // all substitutions should already have been applied recursively. - currNodeVal = Rewriter::rewrite(currNodeVal); + currNodeVal = reconstruct(currNodeVal, results, evalAsNode); + needsReconstruct = false; Trace("evaluator") << "Evaluator: now after substitution + rewriting: " << currNodeVal << std::endl; if (currNodeVal.getNumChildren() > 0) @@ -235,16 +236,34 @@ EvalResult Evaluator::evalInternal( const auto& it = std::find(args.begin(), args.end(), currNode); if (it == args.end()) { + // variable with no substitution is itself evalAsNode[currNode] = currNode; results[currNode] = EvalResult(); continue; } ptrdiff_t pos = std::distance(args.begin(), it); currNodeVal = vals[pos]; + // Don't need to reconstruct since range of substitution should already + // be normalized. + Assert(vals[pos] == Rewriter::rewrite(vals[pos])); + needsReconstruct = false; } - else if (currNode.getKind() == kind::APPLY_UF - && currNode.getOperator().getKind() == kind::LAMBDA) + else if (currNode.getKind() == kind::APPLY_UF) { + Trace("evaluator") << "Evaluate " << currNode << std::endl; + TNode op = currNode.getOperator(); + Assert(evalAsNode.find(op) != evalAsNode.end()); + // no function can be a valid EvalResult + op = evalAsNode[op]; + Trace("evaluator") << "Operator evaluated to " << op << std::endl; + if (op.getKind() != kind::LAMBDA) + { + // this node is not evaluatable due to operator, must add to + // evalAsNode + results[currNode] = EvalResult(); + evalAsNode[currNode] = reconstruct(currNode, results, evalAsNode); + continue; + } // Create a copy of the current substitutions std::vector<Node> lambdaArgs(args); std::vector<Node> lambdaVals(vals); @@ -252,7 +271,6 @@ EvalResult Evaluator::evalInternal( // Add the values for the arguments of the lambda as substitutions at // the beginning of the vector to shadow variables from outer scopes // with the same name - Node op = currNode.getOperator(); for (const auto& lambdaArg : op[0]) { lambdaArgs.insert(lambdaArgs.begin(), lambdaArg); @@ -271,10 +289,14 @@ EvalResult Evaluator::evalInternal( std::unordered_map<TNode, Node, NodeHashFunction> evalAsNodeC; results[currNode] = evalInternal(op[1], lambdaArgs, lambdaVals, evalAsNodeC); + Trace("evaluator") << "Evaluated via arguments to " + << results[currNode].d_tag << std::endl; if (results[currNode].d_tag == EvalResult::INVALID) { // evaluation was invalid, we take the node of op[1] as the result evalAsNode[currNode] = evalAsNodeC[op[1]]; + Trace("evaluator") + << "Take node evaluation: " << evalAsNodeC[op[1]] << std::endl; } continue; } @@ -667,7 +689,9 @@ EvalResult Evaluator::evalInternal( else { results[currNode] = EvalResult(); - evalAsNode[currNode] = currNodeVal; + evalAsNode[currNode] = + needsReconstruct ? reconstruct(currNode, results, evalAsNode) + : currNodeVal; } break; } @@ -684,7 +708,9 @@ EvalResult Evaluator::evalInternal( else { results[currNode] = EvalResult(); - evalAsNode[currNode] = currNodeVal; + evalAsNode[currNode] = + needsReconstruct ? reconstruct(currNode, results, evalAsNode) + : currNodeVal; } break; } @@ -725,7 +751,9 @@ EvalResult Evaluator::evalInternal( Trace("evaluator") << "Theory " << Theory::theoryOf(currNode[0]) << " not supported" << std::endl; results[currNode] = EvalResult(); - evalAsNode[currNode] = currNodeVal; + evalAsNode[currNode] = + needsReconstruct ? reconstruct(currNode, results, evalAsNode) + : currNodeVal; break; } } @@ -751,7 +779,9 @@ EvalResult Evaluator::evalInternal( Trace("evaluator") << "Kind " << currNodeVal.getKind() << " not supported" << std::endl; results[currNode] = EvalResult(); - evalAsNode[currNode] = currNodeVal; + evalAsNode[currNode] = + needsReconstruct ? reconstruct(currNode, results, evalAsNode) + : currNodeVal; } } } @@ -760,5 +790,63 @@ EvalResult Evaluator::evalInternal( return results[n]; } +Node Evaluator::reconstruct( + TNode n, + std::unordered_map<TNode, EvalResult, TNodeHashFunction>& eresults, + std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode) +{ + if (n.getNumChildren() == 0) + { + return n; + } + Trace("evaluator") << "Evaluator: reconstruct " << n << std::endl; + NodeManager* nm = NodeManager::currentNM(); + std::unordered_map<TNode, EvalResult, TNodeHashFunction>::iterator itr; + std::unordered_map<TNode, Node, NodeHashFunction>::iterator itn; + std::vector<Node> echildren; + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) + { + TNode op = n.getOperator(); + itr = eresults.find(op); + Assert(itr != eresults.end()); + if (itr->second.d_tag == EvalResult::INVALID) + { + // could not evaluate the operator, look in the node cache + itn = evalAsNode.find(op); + Assert(itn != evalAsNode.end()); + echildren.push_back(itn->second); + } + else + { + // otherwise, use the evaluation of the operator + echildren.push_back(itr->second.toNode()); + } + } + for (const auto& currNodeChild : n) + { + itr = eresults.find(currNodeChild); + Assert(itr != eresults.end()); + if (itr->second.d_tag == EvalResult::INVALID) + { + // could not evaluate this child, look in the node cache + itn = evalAsNode.find(currNodeChild); + Assert(itn != evalAsNode.end()); + echildren.push_back(itn->second); + } + else + { + // otherwise, use the evaluation + echildren.push_back(itr->second.toNode()); + } + } + // The value is the result of our (partially) successful evaluation + // of the children. + Node nn = nm->mkNode(n.getKind(), echildren); + Trace("evaluator") << "Evaluator: reconstructed " << nn << std::endl; + // Use rewriting. Notice we do not need to substitute here since + // all substitutions should already have been applied recursively. + return Rewriter::rewrite(nn); +} + } // namespace theory } // namespace CVC4 |