--- /dev/null
+/********************* */
+/*! \file evaluator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andres Noetzli
+ ** 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.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The Evaluator class
+ **
+ ** The Evaluator class.
+ **/
+
+#include "theory/evaluator.h"
+
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/theory.h"
+#include "util/integer.h"
+
+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)
+{
+ Trace("evaluator") << "Evaluating " << n << " under substitution " << args
+ << " " << vals << std::endl;
+ return evalInternal(n, args, vals).toNode();
+}
+
+EvalResult Evaluator::evalInternal(TNode n,
+ const std::vector<Node>& args,
+ const std::vector<Node>& vals)
+{
+ std::unordered_map<TNode, EvalResult, TNodeHashFunction> results;
+ std::vector<TNode> queue;
+ queue.emplace_back(n);
+
+ while (queue.size() != 0)
+ {
+ TNode currNode = queue.back();
+
+ if (results.find(currNode) != results.end())
+ {
+ queue.pop_back();
+ continue;
+ }
+
+ bool doEval = true;
+ for (const auto& currNodeChild : currNode)
+ {
+ if (results.find(currNodeChild) == results.end())
+ {
+ queue.emplace_back(currNodeChild);
+ doEval = false;
+ }
+ }
+
+ if (doEval)
+ {
+ queue.pop_back();
+
+ Node currNodeVal = currNode;
+ if (currNode.isVar())
+ {
+ const auto& it = std::find(args.begin(), args.end(), currNode);
+
+ if (it == args.end())
+ {
+ return EvalResult();
+ }
+
+ ptrdiff_t pos = std::distance(args.begin(), it);
+ currNodeVal = vals[pos];
+ }
+ 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])
+ {
+ 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
+ results[currNode] = evalInternal(op[1], lambdaArgs, lambdaVals);
+ continue;
+ }
+
+ switch (currNodeVal.getKind())
+ {
+ case kind::CONST_BOOLEAN:
+ results[currNode] = EvalResult(currNodeVal.getConst<bool>());
+ break;
+
+ case kind::NOT:
+ {
+ results[currNode] = EvalResult(!(results[currNode[0]].d_bool));
+ break;
+ }
+
+ case kind::AND:
+ {
+ bool res = results[currNode[0]].d_bool;
+ for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
+ {
+ res = res && results[currNode[i]].d_bool;
+ }
+ results[currNode] = EvalResult(res);
+ break;
+ }
+
+ case kind::OR:
+ {
+ bool res = results[currNode[0]].d_bool;
+ for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
+ {
+ res = res || results[currNode[i]].d_bool;
+ }
+ results[currNode] = EvalResult(res);
+ break;
+ }
+
+ case kind::CONST_RATIONAL:
+ {
+ const Rational& r = currNodeVal.getConst<Rational>();
+ results[currNode] = EvalResult(r);
+ break;
+ }
+
+ case kind::PLUS:
+ {
+ Rational res = results[currNode[0]].d_rat;
+ for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
+ {
+ res = res + results[currNode[i]].d_rat;
+ }
+ results[currNode] = EvalResult(res);
+ break;
+ }
+
+ case kind::MINUS:
+ {
+ const Rational& x = results[currNode[0]].d_rat;
+ const Rational& y = results[currNode[1]].d_rat;
+ results[currNode] = EvalResult(x - y);
+ break;
+ }
+
+ case kind::MULT:
+ {
+ Rational res = results[currNode[0]].d_rat;
+ for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
+ {
+ res = res * results[currNode[i]].d_rat;
+ }
+ results[currNode] = EvalResult(res);
+ break;
+ }
+
+ case kind::GEQ:
+ {
+ const Rational& x = results[currNode[0]].d_rat;
+ const Rational& y = results[currNode[1]].d_rat;
+ results[currNode] = EvalResult(x >= y);
+ break;
+ }
+
+ case kind::CONST_STRING:
+ results[currNode] = EvalResult(currNodeVal.getConst<String>());
+ break;
+
+ case kind::STRING_CONCAT:
+ {
+ String res = results[currNode[0]].d_str;
+ for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
+ {
+ res = res.concat(results[currNode[i]].d_str);
+ }
+ results[currNode] = EvalResult(res);
+ break;
+ }
+
+ case kind::STRING_LENGTH:
+ {
+ const String& s = results[currNode[0]].d_str;
+ results[currNode] = EvalResult(Rational(s.size()));
+ break;
+ }
+
+ case kind::STRING_SUBSTR:
+ {
+ const String& s = results[currNode[0]].d_str;
+ Integer s_len(s.size());
+ Integer i = results[currNode[1]].d_rat.getNumerator();
+ Integer j = results[currNode[2]].d_rat.getNumerator();
+
+ if (i.strictlyNegative() || j.strictlyNegative() || i >= s_len)
+ {
+ results[currNode] = EvalResult(String(""));
+ }
+ else if (i + j > s_len)
+ {
+ results[currNode] =
+ EvalResult(s.suffix((s_len - i).toUnsignedInt()));
+ }
+ else
+ {
+ results[currNode] =
+ EvalResult(s.substr(i.toUnsignedInt(), j.toUnsignedInt()));
+ }
+ break;
+ }
+
+ case kind::STRING_CHARAT:
+ {
+ const String& s = results[currNode[0]].d_str;
+ Integer s_len(s.size());
+ Integer i = results[currNode[1]].d_rat.getNumerator();
+ if (i.strictlyNegative() || i >= s_len)
+ {
+ results[currNode] = EvalResult(String(""));
+ }
+ else
+ {
+ results[currNode] = EvalResult(s.substr(i.toUnsignedInt(), 1));
+ }
+ break;
+ }
+
+ case kind::STRING_STRCTN:
+ {
+ const String& s = results[currNode[0]].d_str;
+ const String& t = results[currNode[1]].d_str;
+ results[currNode] = EvalResult(s.find(t) != std::string::npos);
+ break;
+ }
+
+ case kind::STRING_STRIDOF:
+ {
+ const String& s = results[currNode[0]].d_str;
+ Integer s_len(s.size());
+ const String& x = results[currNode[1]].d_str;
+ Integer i = results[currNode[2]].d_rat.getNumerator();
+
+ if (i.strictlyNegative() || i >= s_len)
+ {
+ results[currNode] = EvalResult(Rational(-1));
+ }
+ else
+ {
+ size_t r = s.find(x, i.toUnsignedInt());
+ if (r == std::string::npos)
+ {
+ results[currNode] = EvalResult(Rational(-1));
+ }
+ else
+ {
+ results[currNode] = EvalResult(Rational(r));
+ }
+ }
+ break;
+ }
+
+ case kind::STRING_STRREPL:
+ {
+ const String& s = results[currNode[0]].d_str;
+ const String& x = results[currNode[1]].d_str;
+ const String& y = results[currNode[2]].d_str;
+ results[currNode] = EvalResult(s.replace(x, y));
+ break;
+ }
+
+ case kind::STRING_PREFIX:
+ {
+ const String& t = results[currNode[0]].d_str;
+ const String& s = results[currNode[1]].d_str;
+ if (s.size() < t.size())
+ {
+ results[currNode] = EvalResult(false);
+ }
+ else
+ {
+ results[currNode] = EvalResult(s.prefix(t.size()) == t);
+ }
+ break;
+ }
+
+ case kind::STRING_SUFFIX:
+ {
+ const String& t = results[currNode[0]].d_str;
+ const String& s = results[currNode[1]].d_str;
+ if (s.size() < t.size())
+ {
+ results[currNode] = EvalResult(false);
+ }
+ else
+ {
+ results[currNode] = EvalResult(s.suffix(t.size()) == t);
+ }
+ break;
+ }
+
+ case kind::STRING_ITOS:
+ {
+ Integer i = results[currNode[0]].d_rat.getNumerator();
+ if (i.strictlyNegative())
+ {
+ results[currNode] = EvalResult(String(""));
+ }
+ else
+ {
+ results[currNode] = EvalResult(String(i.toString()));
+ }
+ break;
+ }
+
+ case kind::STRING_STOI:
+ {
+ const String& s = results[currNode[0]].d_str;
+ if (s.isNumber())
+ {
+ results[currNode] = EvalResult(Rational(-1));
+ }
+ else
+ {
+ results[currNode] = EvalResult(Rational(s.toNumber()));
+ }
+ break;
+ }
+
+ case kind::CONST_BITVECTOR:
+ results[currNode] = EvalResult(currNodeVal.getConst<BitVector>());
+ break;
+
+ case kind::BITVECTOR_NOT:
+ results[currNode] = EvalResult(~results[currNode[0]].d_bv);
+ break;
+
+ case kind::BITVECTOR_NEG:
+ results[currNode] = EvalResult(-results[currNode[0]].d_bv);
+ break;
+
+ case kind::BITVECTOR_EXTRACT:
+ {
+ unsigned lo = bv::utils::getExtractLow(currNodeVal);
+ unsigned hi = bv::utils::getExtractHigh(currNodeVal);
+ results[currNode] =
+ EvalResult(results[currNode[0]].d_bv.extract(hi, lo));
+ break;
+ }
+
+ case kind::BITVECTOR_CONCAT:
+ {
+ BitVector res = results[currNode[0]].d_bv;
+ for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
+ {
+ res = res.concat(results[currNode[i]].d_bv);
+ }
+ results[currNode] = EvalResult(res);
+ break;
+ }
+
+ case kind::BITVECTOR_PLUS:
+ {
+ BitVector res = results[currNode[0]].d_bv;
+ for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
+ {
+ res = res + results[currNode[i]].d_bv;
+ }
+ results[currNode] = EvalResult(res);
+ break;
+ }
+
+ case kind::BITVECTOR_MULT:
+ {
+ BitVector res = results[currNode[0]].d_bv;
+ for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
+ {
+ res = res * results[currNode[i]].d_bv;
+ }
+ results[currNode] = EvalResult(res);
+ break;
+ }
+ case kind::BITVECTOR_AND:
+ {
+ BitVector res = results[currNode[0]].d_bv;
+ for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
+ {
+ res = res & results[currNode[i]].d_bv;
+ }
+ results[currNode] = EvalResult(res);
+ break;
+ }
+
+ case kind::BITVECTOR_OR:
+ {
+ BitVector res = results[currNode[0]].d_bv;
+ for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
+ {
+ res = res | results[currNode[i]].d_bv;
+ }
+ results[currNode] = EvalResult(res);
+ break;
+ }
+
+ case kind::BITVECTOR_XOR:
+ {
+ BitVector res = results[currNode[0]].d_bv;
+ for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
+ {
+ res = res ^ results[currNode[i]].d_bv;
+ }
+ results[currNode] = EvalResult(res);
+ break;
+ }
+
+ case kind::EQUAL:
+ {
+ EvalResult lhs = results[currNode[0]];
+ EvalResult rhs = results[currNode[1]];
+
+ switch (lhs.d_tag)
+ {
+ case EvalResult::BOOL:
+ {
+ results[currNode] = EvalResult(lhs.d_bool == rhs.d_bool);
+ break;
+ }
+
+ case EvalResult::BITVECTOR:
+ {
+ results[currNode] = EvalResult(lhs.d_bv == rhs.d_bv);
+ break;
+ }
+
+ case EvalResult::RATIONAL:
+ {
+ results[currNode] = EvalResult(lhs.d_rat == rhs.d_rat);
+ break;
+ }
+
+ case EvalResult::STRING:
+ {
+ results[currNode] = EvalResult(lhs.d_str == rhs.d_str);
+ break;
+ }
+
+ default:
+ {
+ Trace("evaluator") << "Theory " << Theory::theoryOf(currNode[0])
+ << " not supported" << std::endl;
+ return EvalResult();
+ break;
+ }
+ }
+
+ break;
+ }
+
+ case kind::ITE:
+ {
+ if (results[currNode[0]].d_bool)
+ {
+ results[currNode] = results[currNode[1]];
+ }
+ else
+ {
+ results[currNode] = results[currNode[2]];
+ }
+ break;
+ }
+
+ default:
+ {
+ Trace("evaluator") << "Kind " << currNodeVal.getKind()
+ << " not supported" << std::endl;
+ return EvalResult();
+ }
+ }
+ }
+ }
+
+ return results[n];
+}
+
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file evaluator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andres Noetzli
+ ** 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.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The Evaluator class
+ **
+ ** The Evaluator class can be used to evaluate terms with constant leaves
+ ** quickly, without going through the rewriter.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__EVALUATOR_H
+#define __CVC4__THEORY__EVALUATOR_H
+
+#include <utility>
+#include <vector>
+
+#include "base/output.h"
+#include "expr/node.h"
+#include "util/bitvector.h"
+#include "util/rational.h"
+#include "util/regexp.h"
+
+namespace CVC4 {
+namespace theory {
+
+/**
+ * Struct that holds the result of an evaluation. The actual value is stored in
+ * a union to avoid the overhead of a class hierarchy with virtual methods.
+ */
+struct EvalResult
+{
+ /* Describes which type of result is being stored */
+ enum
+ {
+ BOOL,
+ BITVECTOR,
+ RATIONAL,
+ STRING,
+ INVALID
+ } d_tag;
+
+ /* Stores the actual result */
+ union
+ {
+ bool d_bool;
+ BitVector d_bv;
+ Rational d_rat;
+ String d_str;
+ };
+
+ EvalResult(const EvalResult& other);
+ EvalResult() : d_tag(INVALID) {}
+ EvalResult(bool b) : d_tag(BOOL), d_bool(b) {}
+ EvalResult(const BitVector& bv) : d_tag(BITVECTOR), d_bv(bv) {}
+ EvalResult(const Rational& i) : d_tag(RATIONAL), d_rat(i) {}
+ EvalResult(const String& str) : d_tag(STRING), d_str(str) {}
+
+ EvalResult& operator=(const EvalResult& other);
+
+ ~EvalResult();
+
+ /**
+ * Converts the result to a Node. If the result is not valid, this function
+ * returns the null node.
+ */
+ Node toNode() const;
+};
+
+/**
+ * The class that performs the actual evaluation of a term under a
+ * substitution. Right now, the class does not cache anything between different
+ * calls to `eval` but this might change in the future.
+ */
+class Evaluator
+{
+ public:
+ /**
+ * Evaluates node `n` under the substitution described by the variable names
+ * `args` and the corresponding values `vals`. The function returns a null
+ * node if there is a subterm that is not constant under the substitution or
+ * if an operator is not supported by the evaluator.
+ */
+ Node eval(TNode n,
+ const std::vector<Node>& args,
+ const std::vector<Node>& vals);
+
+ private:
+ /**
+ * Evaluates node `n` under the substitution described by the variable names
+ * `args` and the corresponding values `vals`. The internal version returns
+ * an EvalResult which has slightly less overhead for recursive calls. The
+ * function returns an invalid result if there is a subterm that is not
+ * constant under the substitution or if an operator is not supported by the
+ * evaluator.
+ */
+ EvalResult evalInternal(TNode n,
+ const std::vector<Node>& args,
+ const std::vector<Node>& vals);
+};
+
+} // namespace theory
+} // namespace CVC4
+
+#endif /* __CVC4__THEORY__EVALUATOR_H */
--- /dev/null
+/********************* */
+/*! \file evaluator_white.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andres Noetzli
+ ** 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.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include <cxxtest/TestSuite.h>
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/evaluator.h"
+#include "theory/rewriter.h"
+#include "theory/theory_test_utils.h"
+
+using namespace CVC4;
+using namespace CVC4::smt;
+using namespace CVC4::theory;
+
+using namespace std;
+
+class TheoryEvaluatorWhite : public CxxTest::TestSuite
+{
+ ExprManager *d_em;
+ NodeManager *d_nm;
+ SmtEngine *d_smt;
+ SmtScope *d_scope;
+
+ public:
+ TheoryEvaluatorWhite() {}
+
+ void setUp()
+ {
+ Options opts;
+ opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
+ d_em = new ExprManager(opts);
+ d_nm = NodeManager::fromExprManager(d_em);
+ d_smt = new SmtEngine(d_em);
+ d_scope = new SmtScope(d_smt);
+ }
+
+ void tearDown()
+ {
+ delete d_scope;
+ delete d_smt;
+ delete d_em;
+ }
+
+ void testSimple()
+ {
+ TypeNode bv64Type = d_nm->mkBitVectorType(64);
+
+ Node w = d_nm->mkVar("w", bv64Type);
+ Node x = d_nm->mkVar("x", bv64Type);
+ Node y = d_nm->mkVar("y", bv64Type);
+ Node z = d_nm->mkVar("z", bv64Type);
+
+ Node zero = d_nm->mkConst(BitVector(64, (unsigned int)0));
+ Node one = d_nm->mkConst(BitVector(64, (unsigned int)1));
+ Node c1 = d_nm->mkConst(BitVector(
+ 64,
+ (unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111));
+ Node c2 = d_nm->mkConst(BitVector(
+ 64,
+ (unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111));
+
+ Node t = d_nm->mkNode(kind::ITE, d_nm->mkNode(kind::EQUAL, y, one), x, w);
+
+ std::vector<Node> args = {w, x, y, z};
+ std::vector<Node> vals = {c1, zero, one, c1};
+
+ Evaluator eval;
+ Node r = eval.eval(t, args, vals);
+ TS_ASSERT_EQUALS(r,
+ Rewriter::rewrite(t.substitute(
+ args.begin(), args.end(), vals.begin(), vals.end())));
+ }
+
+ void testLoop()
+ {
+ TypeNode bv64Type = d_nm->mkBitVectorType(64);
+
+ Node w = d_nm->mkBoundVar(bv64Type);
+ Node x = d_nm->mkVar("x", bv64Type);
+
+ Node zero = d_nm->mkConst(BitVector(1, (unsigned int)0));
+ Node one = d_nm->mkConst(BitVector(64, (unsigned int)1));
+ Node c = d_nm->mkConst(BitVector(
+ 64,
+ (unsigned int)0b0001111000010111110000110110001101011110111001101100000101010100));
+
+ Node largs = d_nm->mkNode(kind::BOUND_VAR_LIST, w);
+ Node lbody = d_nm->mkNode(
+ kind::BITVECTOR_CONCAT, bv::utils::mkExtract(w, 62, 0), zero);
+ Node lambda = d_nm->mkNode(kind::LAMBDA, largs, lbody);
+ Node t = d_nm->mkNode(kind::BITVECTOR_AND,
+ d_nm->mkNode(kind::APPLY_UF, lambda, one),
+ d_nm->mkNode(kind::APPLY_UF, lambda, x));
+
+ std::vector<Node> args = {x};
+ std::vector<Node> vals = {c};
+ Evaluator eval;
+ Node r = eval.eval(t, args, vals);
+ TS_ASSERT_EQUALS(r,
+ Rewriter::rewrite(t.substitute(
+ args.begin(), args.end(), vals.begin(), vals.end())));
+ }
+};
projects / cvc5.git / commitdiff