diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-07-04 02:45:16 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-04 02:45:16 -0700 |
commit | 0cac8099cd69faa8d09bc726e33f71835bf8eec9 (patch) | |
tree | 371837bb6d3c8a17391f1ad1a69dd5334503f7af /src/theory/evaluator.cpp | |
parent | d517f186883e3397948099b7e80327e46b29b85b (diff) | |
parent | ad5a8f0eb67ebd698285a32a8e4101e971853741 (diff) |
Merge branch 'sygusComp2018-2' into replaceSubstitutereplaceSubstitute
Diffstat (limited to 'src/theory/evaluator.cpp')
-rw-r--r-- | src/theory/evaluator.cpp | 100 |
1 files changed, 99 insertions, 1 deletions
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index 0d1536084..ca2140ed5 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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 @@ -23,6 +23,98 @@ namespace CVC4 { namespace theory { +EvalResult::EvalResult(const EvalResult& other) +{ + d_tag = other.d_tag; + switch (d_tag) + { + case BOOL: d_bool = other.d_bool; break; + case BITVECTOR: + new (&d_bv) BitVector; + d_bv = other.d_bv; + break; + case RATIONAL: + new (&d_rat) Rational; + d_rat = other.d_rat; + break; + case STRING: + new (&d_str) String; + d_str = other.d_str; + break; + case INVALID: break; + } +} + +EvalResult& EvalResult::operator=(const EvalResult& other) +{ + if (this != &other) + { + d_tag = other.d_tag; + switch (d_tag) + { + case BOOL: d_bool = other.d_bool; break; + case BITVECTOR: + new (&d_bv) BitVector; + d_bv = other.d_bv; + break; + case RATIONAL: + new (&d_rat) Rational; + d_rat = other.d_rat; + break; + case STRING: + new (&d_str) String; + d_str = other.d_str; + break; + case INVALID: break; + } + } + return *this; +} + +EvalResult::~EvalResult() +{ + switch (d_tag) + { + case BITVECTOR: + { + d_bv.~BitVector(); + break; + } + case RATIONAL: + { + d_rat.~Rational(); + break; + } + case STRING: + { + d_str.~String(); + break; + + default: break; + } + } +} + +Node EvalResult::toNode() const +{ + NodeManager* nm = NodeManager::currentNM(); + switch (d_tag) + { + case EvalResult::BOOL: return nm->mkConst(d_bool); + case EvalResult::BITVECTOR: return nm->mkConst(d_bv); + case EvalResult::RATIONAL: return nm->mkConst(d_rat); + case EvalResult::STRING: return nm->mkConst(d_str); + default: + { + Trace("evaluator") << "Missing conversion from " << d_tag << " to node" + << std::endl; + return Node(); + } + } + + return Node(); +} + Node Evaluator::eval(TNode n, const std::vector<Node>& args, const std::vector<Node>& vals) @@ -80,9 +172,13 @@ EvalResult Evaluator::evalInternal(TNode n, else if (currNode.getKind() == kind::APPLY_UF && currNode.getOperator().getKind() == kind::LAMBDA) { + // 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 Node op = currNode.getOperator(); for (const auto& lambdaArg : op[0]) { @@ -94,6 +190,8 @@ EvalResult Evaluator::evalInternal(TNode n, lambdaVals.insert(lambdaVals.begin(), results[lambdaVal].toNode()); } + // Lambdas are evaluated in a recursive fashion because each evaluation + // requires different substitutions results[currNode] = evalInternal(op[1], lambdaArgs, lambdaVals); continue; } |