From: Andrew Reynolds Date: Mon, 16 Dec 2019 17:23:54 +0000 (-0600) Subject: Fix evaluator for non-evaluatable nodes (#3575) X-Git-Tag: cvc5-1.0.0~3760 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d15d44b3c91b5be2c19adac292f137d2a67eb848;p=cvc5.git 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. --- 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 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::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 results; std::vector queue; queue.emplace_back(n); - std::unordered_map::iterator itn; std::unordered_map::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 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 lambdaArgs(args); std::vector 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 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& eresults, + std::unordered_map& evalAsNode) +{ + if (n.getNumChildren() == 0) + { + return n; + } + Trace("evaluator") << "Evaluator: reconstruct " << n << std::endl; + NodeManager* nm = NodeManager::currentNM(); + std::unordered_map::iterator itr; + std::unordered_map::iterator itn; + std::vector 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 diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h index a65ffdf19..94e6fc518 100644 --- a/src/theory/evaluator.h +++ b/src/theory/evaluator.h @@ -118,6 +118,19 @@ class Evaluator const std::vector& args, const std::vector& vals, std::unordered_map& evalAsNode); + /** reconstruct + * + * This function reconstructs the result of evaluating n using a combination + * of evaluation results (eresults) and substitution+rewriting (evalAsNode). + * + * Arguments eresults and evalAsNode are built within the context of the + * above method for some args and vals. This method ensures that the return + * value is equivalent to the rewritten form of n * { args -> vals }. + */ + Node reconstruct( + TNode n, + std::unordered_map& eresults, + std::unordered_map& evalAsNode); }; } // namespace theory diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index bce46fb6b..0279ca531 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -981,14 +981,12 @@ Node TermDbSygus::evaluateBuiltin(TypeNode tn, // supported by the evaluator res = d_eval->eval(bn, varlist, args); } - if (!res.isNull()) + if (res.isNull()) { - Assert(res - == Rewriter::rewrite(bn.substitute( - varlist.begin(), varlist.end(), args.begin(), args.end()))); - return res; + // must do substitution + res = + bn.substitute(varlist.begin(), varlist.end(), args.begin(), args.end()); } - res = bn.substitute(varlist.begin(), varlist.end(), args.begin(), args.end()); // Call the rewrite node function, which may involve recursive function // evaluation. return rewriteNode(res);