** Top contributors (to current version):
** Andres Noetzli, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
new (&d_str) String;
d_str = other.d_str;
break;
+ case UCONST:
+ new (&d_uc)
+ UninterpretedConstant(other.d_uc.getType(), other.d_uc.getIndex());
+ break;
case INVALID: break;
}
}
new (&d_str) String;
d_str = other.d_str;
break;
+ case UCONST:
+ new (&d_uc)
+ UninterpretedConstant(other.d_uc.getType(), other.d_uc.getIndex());
+ break;
case INVALID: break;
}
}
{
d_str.~String();
break;
-
- default: break;
}
+ case UCONST:
+ {
+ d_uc.~UninterpretedConstant();
+ break;
+ }
+ default: break;
}
}
case EvalResult::BITVECTOR: return nm->mkConst(d_bv);
case EvalResult::RATIONAL: return nm->mkConst(d_rat);
case EvalResult::STRING: return nm->mkConst(d_str);
+ case EvalResult::UCONST: return nm->mkConst(d_uc);
default:
{
Trace("evaluator") << "Missing conversion from " << d_tag << " to node"
Node Evaluator::eval(TNode n,
const std::vector<Node>& args,
- const std::vector<Node>& vals) const
+ const std::vector<Node>& vals,
+ bool useRewriter) const
{
std::unordered_map<Node, Node, NodeHashFunction> visited;
- return eval(n, args, vals, visited);
+ return eval(n, args, vals, visited, useRewriter);
}
Node Evaluator::eval(
TNode n,
const std::vector<Node>& args,
const std::vector<Node>& vals,
- const std::unordered_map<Node, Node, NodeHashFunction>& visited) const
+ const std::unordered_map<Node, Node, NodeHashFunction>& visited,
+ bool useRewriter) const
{
Trace("evaluator") << "Evaluating " << n << " under substitution " << args
<< " " << vals << " with visited size = " << visited.size()
for (const std::pair<const Node, Node>& p : visited)
{
Trace("evaluator") << "Add " << p.first << " == " << p.second << std::endl;
- results[p.first] = evalInternal(p.second, args, vals, evalAsNode, results);
+ results[p.first] = evalInternal(p.second, args, vals, evalAsNode, results, useRewriter);
if (results[p.first].d_tag == EvalResult::INVALID)
{
// could not evaluate, use the evalAsNode map
- evalAsNode[p.first] = evalAsNode[p.second];
+ std::unordered_map<TNode, Node, NodeHashFunction>::iterator itn =
+ evalAsNode.find(p.second);
+ Assert(itn != evalAsNode.end());
+ Node val = itn->second;
+ if (useRewriter)
+ {
+ val = Rewriter::rewrite(val);
+ }
+ evalAsNode[p.first] = val;
}
}
Trace("evaluator") << "Run eval internal..." << std::endl;
- Node ret = evalInternal(n, args, vals, evalAsNode, results).toNode();
+ Node ret = evalInternal(n, args, vals, evalAsNode, results, useRewriter).toNode();
// if we failed to evaluate
- if (ret.isNull())
+ if (ret.isNull() && useRewriter)
{
// 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;
+ ret = Rewriter::rewrite(itn->second);
}
- // should be the same as substitution + rewriting
- Assert(ret
- == Rewriter::rewrite(
- n.substitute(args.begin(), args.end(), vals.begin(), vals.end())));
+ // should be the same as substitution + rewriting, or possibly null if
+ // useRewriter is false
+ Assert((ret.isNull() && !useRewriter)
+ || ret
+ == Rewriter::rewrite(n.substitute(
+ args.begin(), args.end(), vals.begin(), vals.end())));
return ret;
}
const std::vector<Node>& args,
const std::vector<Node>& vals,
std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode,
- std::unordered_map<TNode, EvalResult, TNodeHashFunction>& results) const
+ std::unordered_map<TNode, EvalResult, TNodeHashFunction>& results,
+ bool useRewriter) const
{
std::vector<TNode> queue;
queue.emplace_back(n);
}
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
// 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 (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
+ {
+ // 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: "
<< currNodeVal << std::endl;
// 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.
- Assert(vals[pos] == Rewriter::rewrite(vals[pos]));
- 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);
- 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;
results[currNode] = EvalResult(r);
break;
}
-
+ case kind::UNINTERPRETED_CONSTANT:
+ {
+ const UninterpretedConstant& uc =
+ currNodeVal.getConst<UninterpretedConstant>();
+ results[currNode] = EvalResult(uc);
+ break;
+ }
case kind::PLUS:
{
Rational res = results[currNode[0]].d_rat;
break;
}
+ case kind::STRING_UPDATE:
+ {
+ const String& s = results[currNode[0]].d_str;
+ Integer s_len(s.size());
+ Integer i = results[currNode[1]].d_rat.getNumerator();
+ const String& t = results[currNode[2]].d_str;
+
+ if (i.strictlyNegative() || i >= s_len)
+ {
+ results[currNode] = EvalResult(s);
+ }
+ else
+ {
+ results[currNode] = EvalResult(s.update(i.toUnsignedInt(), t));
+ }
+ break;
+ }
case kind::STRING_CHARAT:
{
const String& s = results[currNode[0]].d_str;
results[currNode] = EvalResult(lhs.d_str == rhs.d_str);
break;
}
+ case EvalResult::UCONST:
+ {
+ results[currNode] = EvalResult(lhs.d_uc == rhs.d_uc);
+ break;
+ }
default:
{
// 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);
+ // Return node, without rewriting. Notice we do not need to substitute here
+ // since all substitutions should already have been applied recursively.
+ return nn;
}
} // namespace theory
projects / cvc5.git / blobdiff