Example evaluation cache utility (#3698)

2 files changed, 283 insertions, 0 deletions

diff --git a/src/theory/quantifiers/sygus/example_eval_cache.cpp b/src/theory/quantifiers/sygus/example_eval_cache.cpp
new file mode 100644
index 000000000..a7dd59900
--- /dev/null
+++ b/src/theory/quantifiers/sygus/example_eval_cache.cpp
@@ -0,0 +1,122 @@
+/*********************                                                        */
+/*! \file example_eval_cache.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
+ **
+ **/
+#include "theory/quantifiers/sygus/example_eval_cache.h"
+
+#include "theory/quantifiers/sygus/example_min_eval.h"
+#include "theory/quantifiers/sygus/synth_conjecture.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+ExampleEvalCache::ExampleEvalCache(TermDbSygus* tds,
+                                   SynthConjecture* p,
+                                   Node f,
+                                   Node e)
+    : d_tds(tds), d_stn(e.getType())
+{
+  ExampleInfer* ei = p->getExampleInfer();
+  Assert(ei->hasExamples(f));
+  for (unsigned i = 0, nex = ei->getNumExamples(f); i < nex; i++)
+  {
+    std::vector<Node> input;
+    ei->getExample(f, i, input);
+    d_examples.push_back(input);
+  }
+  d_indexSearchVals = !d_tds->isVariableAgnosticEnumerator(e);
+}
+
+ExampleEvalCache::~ExampleEvalCache() {}
+
+Node ExampleEvalCache::addSearchVal(Node bv)
+{
+  if (!d_indexSearchVals)
+  {
+    // not indexing search values
+    return Node::null();
+  }
+  std::vector<Node> vals;
+  evaluateVec(bv, vals, false);
+  Trace("sygus-pbe-debug") << "Add to trie..." << std::endl;
+  Node ret = d_trie.addOrGetTerm(bv, vals);
+  Trace("sygus-pbe-debug") << "...got " << ret << std::endl;
+  // Only save the cache data if necessary: if the enumerated term
+  // is redundant, its cached data will not be used later and thus should
+  // be discarded.
+  if (ret == bv)
+  {
+    std::vector<Node>& eocv = d_exOutCache[bv];
+    eocv.insert(eocv.end(), vals.begin(), vals.end());
+  }
+  Assert(ret.getType().isComparableTo(bv.getType()));
+  return ret;
+}
+
+void ExampleEvalCache::evaluateVec(Node bv,
+                                   std::vector<Node>& exOut,
+                                   bool doCache)
+{
+  // is it in the cache?
+  std::map<Node, std::vector<Node>>::iterator it = d_exOutCache.find(bv);
+  if (it != d_exOutCache.end())
+  {
+    exOut.insert(exOut.end(), it->second.begin(), it->second.end());
+    return;
+  }
+  // get the evaluation
+  evaluateVecInternal(bv, exOut);
+  // store in cache if necessary
+  if (doCache)
+  {
+    std::vector<Node>& eocv = d_exOutCache[bv];
+    eocv.insert(eocv.end(), exOut.begin(), exOut.end());
+  }
+}
+
+void ExampleEvalCache::evaluateVecInternal(Node bv,
+                                           std::vector<Node>& exOut) const
+{
+  // use ExampleMinEval
+  SygusTypeInfo& ti = d_tds->getTypeInfo(d_stn);
+  const std::vector<Node>& varlist = ti.getVarList();
+  EmeEvalTds emetds(d_tds, d_stn);
+  ExampleMinEval eme(bv, varlist, &emetds);
+  for (size_t j = 0, esize = d_examples.size(); j < esize; j++)
+  {
+    Node res = eme.evaluate(d_examples[j]);
+    exOut.push_back(res);
+  }
+}
+
+Node ExampleEvalCache::evaluate(Node bn, unsigned i) const
+{
+  Assert(i < d_examples.size());
+  return d_tds->evaluateBuiltin(d_stn, bn, d_examples[i]);
+}
+
+void ExampleEvalCache::clearEvaluationCache(Node bv)
+{
+  Assert(d_exOutCache.find(bv) != d_exOutCache.end());
+  d_exOutCache.erase(bv);
+}
+
+void ExampleEvalCache::clearEvaluationAll() { d_exOutCache.clear(); }
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/example_eval_cache.h b/src/theory/quantifiers/sygus/example_eval_cache.h
new file mode 100644
index 000000000..6aa78851f
--- /dev/null
+++ b/src/theory/quantifiers/sygus/example_eval_cache.h
@@ -0,0 +1,161 @@
+/*********************                                                        */
+/*! \file example_eval_cache.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
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H
+#define CVC4__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H
+
+#include "expr/node_trie.h"
+#include "theory/quantifiers/sygus/example_infer.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class SynthConjecture;
+class TermDbSygus;
+
+/** ExampleEvalCache
+ *
+ * This class caches the evaluation of nodes on a fixed list of examples. It
+ * serves two purposes:
+ * (1) To maintain a cache of the results of evaluation of nodes so that
+ * evaluation is not recomputed in different contexts, and
+ * (2) To maintain a trie of terms indexed by their evaluation on the list
+ * of examples to recognize when two terms are equivalent up to examples.
+ *
+ * This class is associated with a function to synthesize and an enumerator,
+ * which determine which examples are taken from the conjecture and how
+ * to evaluate builtin terms.
+ *
+ * The use of (1) is required since we may be interested in computing the
+ * evaluation of terms on a fixed set of points P, and reusing it in multiple
+ * contexts, including:
+ * - Computing whether a term evaluates the same as another one on P,
+ * - Computing which I/O pairs a term satisfies (for decision tree learning)
+ * whose inputs are P,
+ * - Checking whether the term satisfies refinement lemmas where the function
+ * to synthesize is solely applied to points in P.
+ *
+ * A typical use case of (2) is the following.
+ * During search, the extension of quantifier-free datatypes procedure for
+ * SyGuS datatypes may ask this class whether current candidates can be
+ * discarded based on inferring when two candidate solutions are equivalent
+ * up to examples. For example, the candidate solutions:
+ *     f = \x ite( x < 0, x+1, x ) and f = \x x
+ * are equivalent up to examples on a conjecture like:
+ *     exists f. f(0) = 1 ^ f(5) = 2 ^ f(6) = 3
+ * since they have the same value on the points x = 0,5,6. Hence, we need only
+ * consider one of them. The interface for querying this is
+ *       ExampleEvalCache::addSearchVal(...).
+ * For details, see Reynolds et al. SYNT 2017.
+ */
+class ExampleEvalCache
+{
+ public:
+  /** Construct this class
+   *
+   * This initializes this class for function-to-synthesize f and enumerator
+   * e. In particular, the terms that will be evaluated by this class
+   * are builtin terms that the analog of values taken by enumerator e that
+   * is associated with f.
+   */
+  ExampleEvalCache(TermDbSygus* tds, SynthConjecture* p, Node f, Node e);
+  ~ExampleEvalCache();
+
+  /** Add search value
+   *
+   * This function can be called by the extension of quantifier-free datatypes
+   * procedure for SyGuS datatypes or the SyGuS fast enumerator when we are
+   * considering a value of enumerator e passed to the constructor of this
+   * class whose analog in the signature of builtin theory is bvr.
+   *
+   * This returns either:
+   * - A term that is equivalent to bvr up to examples that was passed as the
+   * argument to a previous call to addSearchVal, or
+   * - bvr, indicating that no previous terms are equivalent to bvr up to
+   * examples,
+   * - null, indicating that symmetry breaking could not be applied (e.g.
+   * if the enumerator of this class is variable agnostic).
+   *
+   * If this method returns bvr (indicating it is not redundant), the
+   * result of the evaluation of bvr is cached by this class, and can be
+   * later accessed by evaluateVec below.
+   */
+  Node addSearchVal(Node bvr);
+  //----------------------------------- evaluating terms
+  /** Evaluate vector
+   *
+   * This adds to exOut the result of evaluating builtin term bv on the set of
+   * examples managed by this class. Term bv is the builtin version of a term
+   * generated for enumerator e that is associated with a
+   * function-to-synthesize f, which were passed to the constructor of this
+   * class. It stores the resulting output for each example in exOut.
+   *
+   * If doCache is true, the result of the evaluation is cached internally.
+   */
+  void evaluateVec(Node bv, std::vector<Node>& exOut, bool doCache = false);
+  /** evaluate builtin
+   *
+   * This returns the evaluation of bn on the i^th example for the
+   * function-to-synthesis associated with enumerator e. If there are not at
+   * least i examples, it returns the rewritten form of bn. For example, if bn =
+   * x+5, e is an enumerator for f in the example [EX#1] from SygusPbe, then
+   *   evaluateBuiltin( tn, bn, e, 0 ) = 7
+   *   evaluateBuiltin( tn, bn, e, 1 ) = 9
+   *   evaluateBuiltin( tn, bn, e, 2 ) = 10
+   */
+  Node evaluate(Node bv, unsigned i) const;
+  /** clear evaluation cache for bv */
+  void clearEvaluationCache(Node bv);
+  /** clear the entire evaluation cache */
+  void clearEvaluationAll();
+  //----------------------------------- end evaluating terms
+
+ private:
+  /** Version of evaluateVec that does not do caching */
+  void evaluateVecInternal(Node bv, std::vector<Node>& exOut) const;
+  /** Pointer to the sygus term database */
+  TermDbSygus* d_tds;
+  /** pointer to the example inference class */
+  std::vector<std::vector<Node>> d_examples;
+  /** The SyGuS type of the enumerator */
+  TypeNode d_stn;
+  /**
+   * Whether we should index search values. This flag is false if the enumerator
+   * of this class is variable agnostic.
+   */
+  bool d_indexSearchVals;
+  /** trie of search values
+   *
+   * This trie is an index of candidate solutions for PBE synthesis and their
+   * (concrete) evaluation on the set of input examples. For example, if the
+   * set of input examples for (x,y) is (0,1), (1,3), then:
+   *   term x is indexed by 0,1
+   *   term x+y is indexed by 1,4
+   *   term 0 is indexed by 0,0.
+   * This is used for symmetry breaking in quantifier-free reasoning
+   * about SyGuS datatypes.
+   */
+  NodeTrie d_trie;
+  /** cache for evaluate */
+  std::map<Node, std::vector<Node>> d_exOutCache;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+} /* namespace CVC4 */
+
+#endif