summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/theory/evaluator.cpp171
1 files 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<Node> lambdaArgs(args);
- std::vector<Node> 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<Node> lambdaArgs(args);
+ std::vector<Node> 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<TNode, Node, NodeHashFunction> evalAsNodeC;
- std::unordered_map<TNode, EvalResult, TNodeHashFunction> 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<TNode, Node, NodeHashFunction> evalAsNodeC;
+ std::unordered_map<TNode, EvalResult, TNodeHashFunction> 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<bool>());
break;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback