summaryrefslogtreecommitdiff
path: root/src/theory/evaluator.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/evaluator.cpp')
-rw-r--r--src/theory/evaluator.cpp95
1 files changed, 51 insertions, 44 deletions
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index e029dd57c..a45855254 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -26,9 +26,16 @@ Node Evaluator::eval(TNode n,
const std::vector<Node>& args,
const std::vector<Node>& vals)
{
- d_results.clear();
- d_hasResult = true;
+ Trace("evaluator") << "Evaluating " << n << " under substitution " << args
+ << " " << vals << std::endl;
+ return evalInternal(n, args, vals).toNode();
+}
+Result Evaluator::evalInternal(TNode n,
+ const std::vector<Node>& args,
+ const std::vector<Node>& vals)
+{
+ std::unordered_map<TNode, Result, TNodeHashFunction> results;
std::vector<TNode> queue;
queue.emplace_back(n);
@@ -36,7 +43,7 @@ Node Evaluator::eval(TNode n,
{
TNode currNode = queue.back();
- if (d_results.find(currNode) != d_results.end())
+ if (results.find(currNode) != results.end())
{
queue.pop_back();
continue;
@@ -45,7 +52,7 @@ Node Evaluator::eval(TNode n,
bool doEval = true;
for (const auto& currNodeChild : currNode)
{
- if (d_results.find(currNodeChild) == d_results.end())
+ if (results.find(currNodeChild) == results.end())
{
queue.emplace_back(currNodeChild);
doEval = false;
@@ -63,7 +70,7 @@ Node Evaluator::eval(TNode n,
if (it == args.end())
{
- return Node::null();
+ return Result();
}
ptrdiff_t pos = std::distance(args.begin(), it);
@@ -83,116 +90,116 @@ Node Evaluator::eval(TNode n,
for (const auto& lambdaVal : currNode)
{
- lambdaVals.insert(lambdaVals.begin(), d_results[lambdaVal].toNode());
+ lambdaVals.insert(lambdaVals.begin(), results[lambdaVal].toNode());
}
- currNodeVal = eval(op[1], lambdaArgs, lambdaVals);
+ results[currNode] = evalInternal(op[1], lambdaArgs, lambdaVals);
+ continue;
}
switch (currNodeVal.getKind())
{
case kind::CONST_BITVECTOR:
- d_results[currNode] = Result(currNodeVal.getConst<BitVector>());
+ results[currNode] = Result(currNodeVal.getConst<BitVector>());
break;
case kind::BITVECTOR_NOT:
- d_results[currNode] = Result(~d_results[currNode[0]].d_bv);
+ results[currNode] = Result(~results[currNode[0]].d_bv);
break;
case kind::BITVECTOR_NEG:
- d_results[currNode] = Result(-d_results[currNode[0]].d_bv);
+ results[currNode] = Result(-results[currNode[0]].d_bv);
break;
case kind::BITVECTOR_EXTRACT:
{
unsigned lo = bv::utils::getExtractLow(currNodeVal);
unsigned hi = bv::utils::getExtractHigh(currNodeVal);
- d_results[currNode] =
- Result(d_results[currNode[0]].d_bv.extract(hi, lo));
+ results[currNode] = Result(results[currNode[0]].d_bv.extract(hi, lo));
break;
}
case kind::BITVECTOR_CONCAT:
{
- BitVector res = d_results[currNode[0]].d_bv;
+ BitVector res = results[currNode[0]].d_bv;
for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
{
- res = res.concat(d_results[currNode[i]].d_bv);
+ res = res.concat(results[currNode[i]].d_bv);
}
- d_results[currNode] = Result(res);
+ results[currNode] = Result(res);
break;
}
case kind::BITVECTOR_PLUS:
{
- BitVector res = d_results[currNode[0]].d_bv;
+ BitVector res = results[currNode[0]].d_bv;
for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
{
- res = res + d_results[currNode[i]].d_bv;
+ res = res + results[currNode[i]].d_bv;
}
- d_results[currNode] = Result(res);
+ results[currNode] = Result(res);
break;
}
case kind::BITVECTOR_MULT:
{
- BitVector res = d_results[currNode[0]].d_bv;
+ BitVector res = results[currNode[0]].d_bv;
for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
{
- res = res * d_results[currNode[i]].d_bv;
+ res = res * results[currNode[i]].d_bv;
}
- d_results[currNode] = Result(res);
+ results[currNode] = Result(res);
break;
}
case kind::BITVECTOR_AND:
{
- BitVector res = d_results[currNode[0]].d_bv;
+ BitVector res = results[currNode[0]].d_bv;
for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
{
- res = res & d_results[currNode[i]].d_bv;
+ res = res & results[currNode[i]].d_bv;
}
- d_results[currNode] = Result(res);
+ results[currNode] = Result(res);
break;
}
case kind::BITVECTOR_OR:
{
- BitVector res = d_results[currNode[0]].d_bv;
+ BitVector res = results[currNode[0]].d_bv;
for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
{
- res = res | d_results[currNode[i]].d_bv;
+ res = res | results[currNode[i]].d_bv;
}
- d_results[currNode] = Result(res);
+ results[currNode] = Result(res);
break;
}
case kind::BITVECTOR_XOR:
{
- BitVector res = d_results[currNode[0]].d_bv;
+ BitVector res = results[currNode[0]].d_bv;
for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
{
- res = res ^ d_results[currNode[i]].d_bv;
+ res = res ^ results[currNode[i]].d_bv;
}
- d_results[currNode] = Result(res);
+ results[currNode] = Result(res);
break;
}
case kind::EQUAL:
{
- Result lhs = d_results[currNode[0]];
- Result rhs = d_results[currNode[1]];
+ Result lhs = results[currNode[0]];
+ Result rhs = results[currNode[1]];
- switch (Theory::theoryOf(currNode[0]))
+ switch (lhs.d_tag)
{
- case THEORY_BOOL:
+ case Result::BOOL:
{
- d_results[currNode] = Result(lhs.d_bool == rhs.d_bool);
+ results[currNode] = Result(lhs.d_bool == rhs.d_bool);
break;
}
- case THEORY_BV:
+ case Result::BITVECTOR:
{
- d_results[currNode] = Result(lhs.d_bv == rhs.d_bv);
+ results[currNode] = Result(lhs.d_bv == rhs.d_bv);
break;
}
@@ -200,7 +207,7 @@ Node Evaluator::eval(TNode n,
{
Trace("evaluator") << "Theory " << Theory::theoryOf(currNode[0])
<< " not supported" << std::endl;
- d_results[currNode] = Result();
+ results[currNode] = Result();
break;
}
}
@@ -210,20 +217,20 @@ Node Evaluator::eval(TNode n,
case kind::ITE:
{
- if (d_results[currNode[0]].d_bool)
+ if (results[currNode[0]].d_bool)
{
- d_results[currNode] = d_results[currNode[1]];
+ results[currNode] = results[currNode[1]];
}
else
{
- d_results[currNode] = d_results[currNode[2]];
+ results[currNode] = results[currNode[2]];
}
break;
}
case kind::NOT:
{
- d_results[currNode] = Result(!(d_results[currNode[0]].d_bool));
+ results[currNode] = Result(!(results[currNode[0]].d_bool));
break;
}
@@ -231,13 +238,13 @@ Node Evaluator::eval(TNode n,
{
Trace("evaluator") << "Kind " << currNodeVal.getKind()
<< " not supported" << std::endl;
- d_results[currNode] = Result();
+ results[currNode] = Result();
}
}
}
}
- return d_results[n].toNode();
+ return results[n];
}
} // namespace theory
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback