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
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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
Node TermDbSygus::evaluateBuiltin(TypeNode tn,
Node bn,
- std::vector<Node>& args,
+ const std::vector<Node>& args,
bool tryEval)
{
if (args.empty())
*/
Node evaluateBuiltin(TypeNode tn,
Node bn,
- std::vector<Node>& args,
+ const std::vector<Node>& args,
bool tryEval = true);
/** evaluate with unfolding
*
projects / cvc5.git / commitdiff