From 219fb439a1a5ac8f8c53f0d287a259fa82c30ee2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 14 Dec 2020 08:35:28 -0600 Subject: [PATCH] Fix and improve evaluator (#5563) This fixes a segfault in the evaluator for substitutions of the form x -> t where t is not constant. This consolidates 2 cases where we did not evaluate children (when we are variable or are an application term with an unevaluated child). This was problematic previously since we would access children of currNode instead of currNodeVal. This also makes our handling of APPLY_UF more consistent, so that it is added to the main switch statement. --- src/theory/evaluator.cpp | 171 +++++++++++++++++++++------------------ 1 file changed, 94 insertions(+), 77 deletions(-) diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index fb7034d2c..516fb1d05 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -210,8 +210,16 @@ EvalResult Evaluator::evalInternal( } bool doProcess = true; + bool isVar = false; bool doEval = true; - if (currNode.getMetaKind() == kind::metakind::PARAMETERIZED) + if (currNode.isVar()) + { + // we do not evaluate if we are a variable, instead we look for the + // variable in args below + isVar = true; + doEval = false; + } + else if (currNode.getMetaKind() == kind::metakind::PARAMETERIZED) { TNode op = currNode.getOperator(); // Certain nodes are parameterized with constant operators, including @@ -262,18 +270,36 @@ EvalResult Evaluator::evalInternal( // store the result of substitution + rewriting currNode { args -> vals } // into evalAsNode[currNode]. - // If we did not successfully evaluate all children + // If we did not successfully evaluate all children, or are a variable if (!doEval) { - // 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; - currNodeVal = reconstruct(currNodeVal, results, evalAsNode); - if (useRewriter) + if (isVar) + { + 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 rewrite since range of substitution should already + // be normalized. + } + else { - // Rewrite the result now, if we use the rewriter. We will see below - // if we are able to turn it into a valid EvalResult. - currNodeVal = Rewriter::rewrite(currNodeVal); + // 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; + currNodeVal = reconstruct(currNodeVal, results, evalAsNode); + if (useRewriter) + { + // Rewrite the result now, if we use the rewriter. We will see below + // if we are able to turn it into a valid EvalResult. + currNodeVal = Rewriter::rewrite(currNodeVal); + } } needsReconstruct = false; Trace("evaluator") << "Evaluator: now after substitution + rewriting: " @@ -292,78 +318,69 @@ EvalResult Evaluator::evalInternal( // block of code below. } - if (currNode.isVar()) - { - 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. - needsReconstruct = false; - } - else if (currNode.getKind() == kind::APPLY_UF) + Trace("evaluator") << "Current node val : " << currNodeVal << std::endl; + + switch (currNodeVal.getKind()) { - 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); + // APPLY_UF is a special case where we look up the operator and apply + // beta reduction if possible + case 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); - // 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 - for (const auto& lambdaArg : op[0]) - { - lambdaArgs.insert(lambdaArgs.begin(), lambdaArg); - } + // 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 + for (const auto& lambdaArg : op[0]) + { + lambdaArgs.insert(lambdaArgs.begin(), lambdaArg); + } - for (const auto& lambdaVal : currNode) - { - lambdaVals.insert(lambdaVals.begin(), results[lambdaVal].toNode()); - } + for (const auto& lambdaVal : currNode) + { + lambdaVals.insert(lambdaVals.begin(), results[lambdaVal].toNode()); + } - // Lambdas are evaluated in a recursive fashion because each evaluation - // requires different substitutions. We use a fresh cache since the - // evaluation of op[1] is under a new substitution and thus should not - // be cached. We could alternatively copy evalAsNode to evalAsNodeC but - // favor avoiding this copy for performance reasons. - std::unordered_map evalAsNodeC; - std::unordered_map resultsC; - results[currNode] = - evalInternal(op[1], lambdaArgs, lambdaVals, evalAsNodeC, resultsC, useRewriter); - 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; + // Lambdas are evaluated in a recursive fashion because each + // evaluation requires different substitutions. We use a fresh cache + // since the evaluation of op[1] is under a new substitution and thus + // should not be cached. We could alternatively copy evalAsNode to + // evalAsNodeC but favor avoiding this copy for performance reasons. + std::unordered_map evalAsNodeC; + std::unordered_map resultsC; + results[currNode] = evalInternal(op[1], + lambdaArgs, + lambdaVals, + evalAsNodeC, + resultsC, + useRewriter); + 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; - } - - switch (currNodeVal.getKind()) - { + break; case kind::CONST_BOOLEAN: results[currNode] = EvalResult(currNodeVal.getConst()); break; -- 2.30.2