From 7d7f4d0aba7330bcc79766b6f885e746cacee81d Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sat, 9 Jun 2018 18:51:31 -0700 Subject: Evaluator --- src/Makefile.am | 2 + src/theory/evaluator.cpp | 206 +++++++++++++++++++++ src/theory/evaluator.h | 118 ++++++++++++ .../quantifiers/sygus/term_database_sygus.cpp | 20 +- test/unit/Makefile.am | 1 + 5 files changed, 346 insertions(+), 1 deletion(-) create mode 100644 src/theory/evaluator.cpp create mode 100644 src/theory/evaluator.h diff --git a/src/Makefile.am b/src/Makefile.am index aa4487c42..9e7762af4 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -179,6 +179,8 @@ libcvc4_la_SOURCES = \ theory/atom_requests.cpp \ theory/atom_requests.h \ theory/care_graph.h \ + theory/evaluator.cpp \ + theory/evaluator.h \ theory/interrupted.h \ theory/ite_utilities.cpp \ theory/ite_utilities.h \ diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp new file mode 100644 index 000000000..df35775f6 --- /dev/null +++ b/src/theory/evaluator.cpp @@ -0,0 +1,206 @@ +/********************* */ +/*! \file evaluator.cpp + ** \verbatim + ** 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 + ** 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" + +namespace CVC4 { +namespace theory { + +Node Evaluator::eval(TNode n, + const std::vector& args, + const std::vector& vals) +{ + d_results.clear(); + d_hasResult = true; + + std::vector queue; + queue.emplace_back(n); + + while (queue.size() != 0) + { + TNode currNode = queue.back(); + + bool doEval = true; + for (const auto& currNodeChild : currNode) + { + if (d_results.find(currNodeChild) == d_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 Node::null(); + } + + ptrdiff_t pos = std::distance(it, args.begin()); + currNodeVal = vals[pos]; + } + else if (currNode.getKind() == kind::APPLY_UF + && currNode.getOperator().getKind() == kind::LAMBDA) + { + std::vector lambdaArgs(args); + std::vector lambdaVals(vals); + + Node op = currNode.getOperator(); + for (const auto& lambdaArg : op[0]) + { + lambdaArgs.insert(lambdaArgs.begin(), lambdaArg); + } + + for (const auto& lambdaVal : currNode) + { + lambdaVals.insert(lambdaVals.begin(), d_results[lambdaVal].toNode()); + } + + currNodeVal = eval(op[1], lambdaArgs, lambdaVals); + } + + switch (currNodeVal.getKind()) + { + case kind::CONST_BITVECTOR: + d_results[currNode] = Result(currNodeVal.getConst()); + break; + + case kind::BITVECTOR_NOT: + d_results[currNode] = Result(~d_results[currNode[0]].d_bv); + break; + + case kind::BITVECTOR_NEG: + d_results[currNode] = Result(-d_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)); + break; + } + + case kind::BITVECTOR_CONCAT: + { + BitVector res = d_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); + } + d_results[currNode] = Result(res); + break; + } + + case kind::BITVECTOR_PLUS: + { + BitVector res = d_results[currNode[0]].d_bv; + for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) + { + res = res + d_results[currNode[i]].d_bv; + } + d_results[currNode] = Result(res); + break; + } + + case kind::BITVECTOR_MULT: + { + BitVector res = d_results[currNode[0]].d_bv; + for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) + { + res = res * d_results[currNode[i]].d_bv; + } + d_results[currNode] = Result(res); + break; + } + case kind::BITVECTOR_AND: + { + BitVector res = d_results[currNode[0]].d_bv; + for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) + { + res = res & d_results[currNode[i]].d_bv; + } + d_results[currNode] = Result(res); + break; + } + + case kind::BITVECTOR_OR: + { + BitVector res = d_results[currNode[0]].d_bv; + for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) + { + res = res | d_results[currNode[i]].d_bv; + } + d_results[currNode] = Result(res); + break; + } + + case kind::BITVECTOR_XOR: + { + BitVector res = d_results[currNode[0]].d_bv; + for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) + { + res = res ^ d_results[currNode[i]].d_bv; + } + d_results[currNode] = Result(res); + break; + } + + case kind::EQUAL: + { + Result lhs = d_results[currNode[0]]; + Result rhs = d_results[currNode[1]]; + + d_results[currNode] = Result(lhs.d_bv == rhs.d_bv); + break; + } + + case kind::ITE: + { + if (d_results[currNode[0]].d_bool) + { + d_results[currNode] = d_results[currNode[1]]; + } + else + { + d_results[currNode] = d_results[currNode[2]]; + } + break; + } + + default: + std::cout << "Not supported: " << currNodeVal << std::endl; + std::exit(1); + } + } + } + + return d_results[n].toNode(); +} + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h new file mode 100644 index 000000000..35ba2b3d9 --- /dev/null +++ b/src/theory/evaluator.h @@ -0,0 +1,118 @@ +/********************* */ +/*! \file evaluator.h + ** \verbatim + ** 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 + ** 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 "cvc4_private.h" + +#pragma once + +#include +#include + +#include "expr/node.h" +#include "util/bitvector.h" + +namespace CVC4 { +namespace theory { + +struct Result +{ + enum + { + BITVECTOR, + BOOL, + INVALID + } d_tag; + union + { + bool d_bool; + BitVector d_bv; + }; + + Result(const Result& other) + { + d_tag = other.d_tag; + switch (d_tag) + { + case BITVECTOR: + new (&d_bv) BitVector; + d_bv = other.d_bv; + break; + case BOOL: d_bool = other.d_bool; break; + case INVALID: break; + } + } + + Result() : d_tag(INVALID) {} + + Result(bool b) : d_tag(BOOL), d_bool(b) {} + + Result(const BitVector& bv) : d_tag(BITVECTOR), d_bv(bv) {} + + Result& operator=(const Result& other) + { + if (this != &other) + { + d_tag = other.d_tag; + switch (d_tag) + { + case BITVECTOR: + new (&d_bv) BitVector; + d_bv = other.d_bv; + break; + case BOOL: d_bool = other.d_bool; break; + case INVALID: break; + } + } + return *this; + } + + ~Result() + { + if (d_tag == BITVECTOR) + { + d_bv.~BitVector(); + } + } + + Node toNode() + { + NodeManager* nm = NodeManager::currentNM(); + switch (d_tag) + { + case Result::BITVECTOR: return nm->mkConst(d_bv); + default: + std::cout << "Not supported:( " << d_tag << std::endl; + std::exit(1); + } + + return Node(); + } +}; + +class Evaluator +{ + public: + Node eval(TNode n, + const std::vector& args, + const std::vector& vals); + + private: + bool d_hasResult; + std::unordered_map d_results; +}; + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 416e9825b..0d09b20d8 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -18,6 +18,7 @@ #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" #include "theory/datatypes/datatypes_rewriter.h" +#include "theory/evaluator.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" @@ -1635,7 +1636,24 @@ Node TermDbSygus::evaluateBuiltin( TypeNode tn, Node bn, std::vector< Node >& ar std::map< TypeNode, std::vector< Node > >::iterator it = d_var_list.find( tn ); Assert( it!=d_var_list.end() ); Assert( it->second.size()==args.size() ); - return Rewriter::rewrite( bn.substitute( it->second.begin(), it->second.end(), args.begin(), args.end() ) ); + + Evaluator eval; + Node res = eval.eval(bn, it->second, args); + //Node res; + if (!res.isNull()) + { + Assert(res + == Rewriter::rewrite(bn.substitute(it->second.begin(), + it->second.end(), + args.begin(), + args.end()))); + return res; + } + else + { + return Rewriter::rewrite(bn.substitute( + it->second.begin(), it->second.end(), args.begin(), args.end())); + } }else{ return Rewriter::rewrite( bn ); } diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index cc9f6fb1b..a17687101 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -11,6 +11,7 @@ UNIT_TESTS += \ theory/theory_black \ theory/theory_bv_white \ theory/theory_engine_white \ + theory/theory_evaluator_white \ theory/theory_quantifiers_bv_instantiator_white \ theory/theory_quantifiers_bv_inverter_white \ theory/theory_strings_rewriter_white \ -- cgit v1.2.3