X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Ftheory%2Fevaluator.cpp;h=516fb1d05a36872280425309d093ce69f922806c;hb=39e82b212bd2f957805884c24e6414289a7ec987;hp=0a0176f25b5a28a1b8281b709206d02766783a07;hpb=7b0efcd75f471b4252c65b8d18aa4c3266649626;p=cvc5.git diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index 0a0176f25..516fb1d05 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -2,10 +2,10 @@ /*! \file evaluator.cpp ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli + ** Andres Noetzli, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 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 ** @@ -17,6 +17,8 @@ #include "theory/evaluator.h" #include "theory/bv/theory_bv_utils.h" +#include "theory/rewriter.h" +#include "theory/strings/theory_strings_utils.h" #include "theory/theory.h" #include "util/integer.h" @@ -41,6 +43,10 @@ EvalResult::EvalResult(const EvalResult& other) 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; } } @@ -65,6 +71,10 @@ EvalResult& EvalResult::operator=(const EvalResult& other) 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; } } @@ -89,9 +99,13 @@ EvalResult::~EvalResult() { d_str.~String(); break; - - default: break; } + case UCONST: + { + d_uc.~UninterpretedConstant(); + break; + } + default: break; } } @@ -104,6 +118,7 @@ Node EvalResult::toNode() const 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" @@ -115,20 +130,74 @@ Node EvalResult::toNode() const Node Evaluator::eval(TNode n, const std::vector& args, - const std::vector& vals) + const std::vector& vals, + bool useRewriter) const +{ + std::unordered_map visited; + return eval(n, args, vals, visited, useRewriter); +} +Node Evaluator::eval( + TNode n, + const std::vector& args, + const std::vector& vals, + const std::unordered_map& visited, + bool useRewriter) const { Trace("evaluator") << "Evaluating " << n << " under substitution " << args - << " " << vals << std::endl; - return evalInternal(n, args, vals).toNode(); + << " " << vals << " with visited size = " << visited.size() + << std::endl; + std::unordered_map evalAsNode; + std::unordered_map results; + // add visited to results + for (const std::pair& p : visited) + { + Trace("evaluator") << "Add " << p.first << " == " << p.second << std::endl; + 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 + std::unordered_map::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, useRewriter).toNode(); + // if we failed to evaluate + if (ret.isNull() && useRewriter) + { + // should be stored in the evaluation-as-node map + std::unordered_map::iterator itn = + evalAsNode.find(n); + Assert(itn != evalAsNode.end()); + ret = Rewriter::rewrite(itn->second); + } + // 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; } -EvalResult Evaluator::evalInternal(TNode n, - const std::vector& args, - const std::vector& vals) +EvalResult Evaluator::evalInternal( + TNode n, + const std::vector& args, + const std::vector& vals, + std::unordered_map& evalAsNode, + std::unordered_map& results, + bool useRewriter) const { - std::unordered_map results; std::vector queue; queue.emplace_back(n); + std::unordered_map::iterator itr; while (queue.size() != 0) { @@ -140,67 +209,178 @@ EvalResult Evaluator::evalInternal(TNode n, continue; } + bool doProcess = true; + bool isVar = false; bool doEval = true; + 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 + // bitvector extract. These operators do not need to be evaluated. + if (!op.isConst()) + { + itr = results.find(op); + if (itr == results.end()) + { + queue.emplace_back(op); + doProcess = false; + } + else if (itr->second.d_tag == EvalResult::INVALID) + { + doEval = false; + } + } + } for (const auto& currNodeChild : currNode) { - if (results.find(currNodeChild) == results.end()) + itr = results.find(currNodeChild); + if (itr == results.end()) { queue.emplace_back(currNodeChild); + doProcess = false; + } + else if (itr->second.d_tag == EvalResult::INVALID) + { + // we cannot evaluate since there was an invalid child doEval = false; } } + Trace("evaluator") << "Evaluator: visit " << currNode + << ", process = " << doProcess + << ", evaluate = " << doEval << std::endl; - if (doEval) + if (doProcess) { queue.pop_back(); Node currNodeVal = currNode; - if (currNode.isVar()) - { - const auto& it = std::find(args.begin(), args.end(), currNode); + // whether we need to reconstruct the current node in the case of failure + bool needsReconstruct = true; - if (it == args.end()) - { - return EvalResult(); - } + // The code below should either: + // (1) store a valid EvalResult into results[currNode], or + // (2) store an invalid EvalResult into results[currNode] and + // store the result of substitution + rewriting currNode { args -> vals } + // into evalAsNode[currNode]. - ptrdiff_t pos = std::distance(args.begin(), it); - currNodeVal = vals[pos]; - } - else if (currNode.getKind() == kind::APPLY_UF - && currNode.getOperator().getKind() == kind::LAMBDA) + // If we did not successfully evaluate all children, or are a variable + if (!doEval) { - // 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 - Node op = currNode.getOperator(); - for (const auto& lambdaArg : op[0]) - { - lambdaArgs.insert(lambdaArgs.begin(), lambdaArg); - } - - for (const auto& lambdaVal : currNode) + if (isVar) { - 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); - if (results[currNode].d_tag == EvalResult::INVALID) - { - // evaluation was invalid, we fail - return results[currNode]; + 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); + } } - continue; + needsReconstruct = false; + Trace("evaluator") << "Evaluator: now after substitution + rewriting: " + << currNodeVal << std::endl; + if (currNodeVal.getNumChildren() > 0) + { + // We may continue with a valid EvalResult at this point only if + // we have no children. We must otherwise fail here since some of + // our children may not have successful evaluations. + results[currNode] = EvalResult(); + evalAsNode[currNode] = currNodeVal; + continue; + } + // Otherwise, we may be able to turn the overall result into an + // valid EvalResult and continue. We fallthrough and continue with the + // block of code below. } + Trace("evaluator") << "Current node val : " << currNodeVal << std::endl; + switch (currNodeVal.getKind()) { + // 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); + } + + 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; + } + } + break; case kind::CONST_BOOLEAN: results[currNode] = EvalResult(currNodeVal.getConst()); break; @@ -239,7 +419,13 @@ EvalResult Evaluator::evalInternal(TNode n, results[currNode] = EvalResult(r); break; } - + case kind::UNINTERPRETED_CONSTANT: + { + const UninterpretedConstant& uc = + currNodeVal.getConst(); + results[currNode] = EvalResult(uc); + break; + } case kind::PLUS: { Rational res = results[currNode[0]].d_rat; @@ -259,7 +445,14 @@ EvalResult Evaluator::evalInternal(TNode n, break; } + case kind::UMINUS: + { + const Rational& x = results[currNode[0]].d_rat; + results[currNode] = EvalResult(-x); + break; + } case kind::MULT: + case kind::NONLINEAR_MULT: { Rational res = results[currNode[0]].d_rat; for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) @@ -277,7 +470,33 @@ EvalResult Evaluator::evalInternal(TNode n, results[currNode] = EvalResult(x >= y); break; } - + case kind::LEQ: + { + const Rational& x = results[currNode[0]].d_rat; + const Rational& y = results[currNode[1]].d_rat; + results[currNode] = EvalResult(x <= y); + break; + } + case kind::GT: + { + const Rational& x = results[currNode[0]].d_rat; + const Rational& y = results[currNode[1]].d_rat; + results[currNode] = EvalResult(x > y); + break; + } + case kind::LT: + { + const Rational& x = results[currNode[0]].d_rat; + const Rational& y = results[currNode[1]].d_rat; + results[currNode] = EvalResult(x < y); + break; + } + case kind::ABS: + { + const Rational& x = results[currNode[0]].d_rat; + results[currNode] = EvalResult(x.abs()); + break; + } case kind::CONST_STRING: results[currNode] = EvalResult(currNodeVal.getConst()); break; @@ -324,6 +543,23 @@ EvalResult Evaluator::evalInternal(TNode n, 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; @@ -441,13 +677,27 @@ EvalResult Evaluator::evalInternal(TNode n, break; } - case kind::STRING_CODE: + case kind::STRING_FROM_CODE: + { + Integer i = results[currNode[0]].d_rat.getNumerator(); + if (i >= 0 && i < strings::utils::getAlphabetCardinality()) + { + std::vector svec = {i.toUnsignedInt()}; + results[currNode] = EvalResult(String(svec)); + } + else + { + results[currNode] = EvalResult(String("")); + } + break; + } + + case kind::STRING_TO_CODE: { const String& s = results[currNode[0]].d_str; if (s.size() == 1) { - results[currNode] = EvalResult( - Rational(String::convertUnsignedIntToCode(s.getVec()[0]))); + results[currNode] = EvalResult(Rational(s.getVec()[0])); } else { @@ -541,6 +791,44 @@ EvalResult Evaluator::evalInternal(TNode n, results[currNode] = EvalResult(res); break; } + case kind::BITVECTOR_UDIV: + case kind::BITVECTOR_UDIV_TOTAL: + { + if (currNodeVal.getKind() == kind::BITVECTOR_UDIV_TOTAL + || results[currNode[1]].d_bv.getValue() != 0) + { + BitVector res = results[currNode[0]].d_bv; + res = res.unsignedDivTotal(results[currNode[1]].d_bv); + results[currNode] = EvalResult(res); + } + else + { + results[currNode] = EvalResult(); + evalAsNode[currNode] = + needsReconstruct ? reconstruct(currNode, results, evalAsNode) + : currNodeVal; + } + break; + } + case kind::BITVECTOR_UREM: + case kind::BITVECTOR_UREM_TOTAL: + { + if (currNodeVal.getKind() == kind::BITVECTOR_UREM_TOTAL + || results[currNode[1]].d_bv.getValue() != 0) + { + BitVector res = results[currNode[0]].d_bv; + res = res.unsignedRemTotal(results[currNode[1]].d_bv); + results[currNode] = EvalResult(res); + } + else + { + results[currNode] = EvalResult(); + evalAsNode[currNode] = + needsReconstruct ? reconstruct(currNode, results, evalAsNode) + : currNodeVal; + } + break; + } case kind::EQUAL: { @@ -572,12 +860,20 @@ EvalResult Evaluator::evalInternal(TNode n, results[currNode] = EvalResult(lhs.d_str == rhs.d_str); break; } + case EvalResult::UCONST: + { + results[currNode] = EvalResult(lhs.d_uc == rhs.d_uc); + break; + } default: { Trace("evaluator") << "Theory " << Theory::theoryOf(currNode[0]) << " not supported" << std::endl; - return EvalResult(); + results[currNode] = EvalResult(); + evalAsNode[currNode] = + needsReconstruct ? reconstruct(currNode, results, evalAsNode) + : currNodeVal; break; } } @@ -602,7 +898,10 @@ EvalResult Evaluator::evalInternal(TNode n, { Trace("evaluator") << "Kind " << currNodeVal.getKind() << " not supported" << std::endl; - return EvalResult(); + results[currNode] = EvalResult(); + evalAsNode[currNode] = + needsReconstruct ? reconstruct(currNode, results, evalAsNode) + : currNodeVal; } } } @@ -611,5 +910,70 @@ EvalResult Evaluator::evalInternal(TNode n, return results[n]; } +Node Evaluator::reconstruct( + TNode n, + std::unordered_map& eresults, + std::unordered_map& evalAsNode) const +{ + if (n.getNumChildren() == 0) + { + return n; + } + Trace("evaluator") << "Evaluator: reconstruct " << n << std::endl; + NodeManager* nm = NodeManager::currentNM(); + std::unordered_map::iterator itr; + std::unordered_map::iterator itn; + std::vector echildren; + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) + { + TNode op = n.getOperator(); + if (op.isConst()) + { + echildren.push_back(op); + } + else + { + itr = eresults.find(op); + Assert(itr != eresults.end()); + if (itr->second.d_tag == EvalResult::INVALID) + { + // could not evaluate the operator, look in the node cache + itn = evalAsNode.find(op); + Assert(itn != evalAsNode.end()); + echildren.push_back(itn->second); + } + else + { + // otherwise, use the evaluation of the operator + echildren.push_back(itr->second.toNode()); + } + } + } + for (const auto& currNodeChild : n) + { + itr = eresults.find(currNodeChild); + Assert(itr != eresults.end()); + if (itr->second.d_tag == EvalResult::INVALID) + { + // could not evaluate this child, look in the node cache + itn = evalAsNode.find(currNodeChild); + Assert(itn != evalAsNode.end()); + echildren.push_back(itn->second); + } + else + { + // otherwise, use the evaluation + echildren.push_back(itr->second.toNode()); + } + } + // The value is the result of our (partially) successful evaluation + // of the children. + Node nn = nm->mkNode(n.getKind(), echildren); + Trace("evaluator") << "Evaluator: reconstructed " << nn << std::endl; + // 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 } // namespace CVC4