diff options
| -rw-r--r-- | src/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/example_min_eval.cpp | 87 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/example_min_eval.h | 123 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.h | 2 |
5 files changed, 214 insertions, 2 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index af29a761c..271ceb045 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -564,6 +564,8 @@ libcvc4_add_sources( theory/quantifiers/sygus/cegis_unif.h theory/quantifiers/sygus/enum_stream_substitution.cpp theory/quantifiers/sygus/enum_stream_substitution.h + theory/quantifiers/sygus/example_min_eval.cpp + theory/quantifiers/sygus/example_min_eval.h theory/quantifiers/sygus/sygus_abduct.cpp theory/quantifiers/sygus/sygus_abduct.h theory/quantifiers/sygus/sygus_enumerator.cpp diff --git a/src/theory/quantifiers/sygus/example_min_eval.cpp b/src/theory/quantifiers/sygus/example_min_eval.cpp new file mode 100644 index 000000000..8af63c97f --- /dev/null +++ b/src/theory/quantifiers/sygus/example_min_eval.cpp @@ -0,0 +1,87 @@ +/********************* */ +/*! \file example_min_eval.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Implementation of utility for minimizing the number of calls to + ** evaluate a term on substitutions with a fixed domain. + **/ + +#include "theory/quantifiers/sygus/example_min_eval.h" + +#include "expr/node_algorithm.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +ExampleMinEval::ExampleMinEval(Node n, + const std::vector<Node>& vars, + EmeEval* ece) +{ + AlwaysAssert(d_evalNode.isNull()); + d_evalNode = n; + d_vars.insert(d_vars.end(), vars.begin(), vars.end()); + + // compute its free variables + std::unordered_set<Node, NodeHashFunction> fvs; + expr::getFreeVariables(n, fvs); + for (size_t i = 0, vsize = vars.size(); i < vsize; i++) + { + if (fvs.find(vars[i]) != fvs.end()) + { + // will use this index + d_indices.push_back(i); + } + } + Trace("example-cache") << "For " << n << ", " << d_indices.size() << " / " + << d_vars.size() << " variables are relevant" + << std::endl; + d_ece = ece; +} + +Node ExampleMinEval::evaluate(const std::vector<Node>& subs) +{ + Assert(d_vars.size() == subs.size()); + + if (d_indices.size() == d_vars.size()) + { + // no sharing is possible since all variables are relevant, just evaluate + return d_ece->eval(d_evalNode, d_vars, subs); + } + + // get the subsequence of subs that is relevant + std::vector<Node> relSubs; + for (unsigned i = 0, ssize = d_indices.size(); i < ssize; i++) + { + relSubs.push_back(subs[d_indices[i]]); + } + Node res = d_trie.existsTerm(relSubs); + if (res.isNull()) + { + // not already cached, must evaluate + res = d_ece->eval(d_evalNode, d_vars, subs); + + // add to trie + d_trie.addTerm(res, relSubs); + } + return res; +} + +Node EmeEvalTds::eval(TNode n, + const std::vector<Node>& args, + const std::vector<Node>& vals) +{ + return d_tds->evaluateBuiltin(d_tn, n, vals); +} + +} // namespace quantifiers +} // namespace theory +} /* namespace CVC4 */ diff --git a/src/theory/quantifiers/sygus/example_min_eval.h b/src/theory/quantifiers/sygus/example_min_eval.h new file mode 100644 index 000000000..28fd849de --- /dev/null +++ b/src/theory/quantifiers/sygus/example_min_eval.h @@ -0,0 +1,123 @@ +/********************* */ +/*! \file example_min_eval.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 utility for minimizing the number of calls to evaluate a term + ** on substitutions with a fixed domain. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H +#define CVC4__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H + +#include <vector> + +#include "expr/node.h" +#include "expr/node_trie.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** + * Virtual evaluator class for Example Minimize Eval. + */ +class EmeEval +{ + public: + EmeEval() {} + virtual ~EmeEval() {} + /** Evaluate n given substitution { args -> vals }. */ + virtual Node eval(TNode n, + const std::vector<Node>& args, + const std::vector<Node>& vals) = 0; +}; + +/** + * Example Minimize Eval + * + * This class is designed to evaluate a term on a set of substitutions + * with a fixed domain. + * + * Its key feature is that substitutions that are identical over the free + * variables of the term are not recomputed. For example, say I wish to evaluate + * x+5 on substitutions having the domain { x, y }. Then, for the substitutions: + * { x -> 0, y -> 1 } + * { x -> 0, y -> 2 } + * { x -> 0, y -> 3 } + * { x -> 1, y -> 3 } + * I would only compute the result of 0+5 once. On the other hand, evaluating + * x+y for the above substitutions would require 4 evaluations. + * + * To use this class, call initialize(n,vars) first and then + * evaluate(subs_1) ... evaluate(subs_n) as desired. Details on these methods + * can be found below. + */ +class ExampleMinEval +{ + public: + /** + * Initialize this cache to evaluate n on substitutions with domain vars. + * Argument ece is the evaluator object. + */ + ExampleMinEval(Node n, const std::vector<Node>& vars, EmeEval* ece); + ~ExampleMinEval() {} + /** + * Return the result of evaluating n * { vars -> subs } where vars is the + * set of variables passed to initialize above. + */ + Node evaluate(const std::vector<Node>& subs); + + private: + /** The node to evaluate */ + Node d_evalNode; + /** The domain of substitutions */ + std::vector<Node> d_vars; + /** The indices in d_vars that occur free in n */ + std::vector<size_t> d_indices; + /** + * The trie of results. This maps subs[d_indices[0]] .. subs[d_indices[j]] + * to the result of the evaluation. For the example at the top of this class, + * this trie would map (0) -> 5, (1) -> 6. + */ + NodeTrie d_trie; + /** Pointer to the evaluator object */ + EmeEval* d_ece; +}; + +class TermDbSygus; + +/** An example cache evaluator based on the term database sygus utility */ +class EmeEvalTds : public EmeEval +{ + public: + EmeEvalTds(TermDbSygus* tds, TypeNode tn) : d_tds(tds), d_tn(tn) {} + virtual ~EmeEvalTds() {} + /** + * Evaluate n given substitution { args -> vals } using the term database + * sygus evaluateBuiltin function. + */ + Node eval(TNode n, + const std::vector<Node>& args, + const std::vector<Node>& vals) override; + + private: + /** Pointer to the sygus term database */ + TermDbSygus* d_tds; + /** The sygus type of the node we will be evaluating */ + TypeNode d_tn; +}; + +} // namespace quantifiers +} // namespace theory +} /* namespace CVC4 */ + +#endif diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index b096b2430..0b3428c9d 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -952,7 +952,7 @@ unsigned TermDbSygus::getAnchorDepth( Node n ) { Node TermDbSygus::evaluateBuiltin(TypeNode tn, Node bn, - std::vector<Node>& args, + const std::vector<Node>& args, bool tryEval) { if (args.empty()) diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index b9f8bf987..516515c05 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -266,7 +266,7 @@ class TermDbSygus { */ Node evaluateBuiltin(TypeNode tn, Node bn, - std::vector<Node>& args, + const std::vector<Node>& args, bool tryEval = true); /** evaluate with unfolding * |