From: Andrew Reynolds Date: Fri, 7 Feb 2020 16:23:47 +0000 (-0600) Subject: Example evaluation cache utility (#3698) X-Git-Tag: cvc5-1.0.0~3676 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=841ef93ea04d4e5434d62ecf18adb85e8255c4ed;p=cvc5.git Example evaluation cache utility (#3698) --- 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 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 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& 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& exOut, + bool doCache) +{ + // is it in the cache? + std::map>::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& eocv = d_exOutCache[bv]; + eocv.insert(eocv.end(), exOut.begin(), exOut.end()); + } +} + +void ExampleEvalCache::evaluateVecInternal(Node bv, + std::vector& exOut) const +{ + // use ExampleMinEval + SygusTypeInfo& ti = d_tds->getTypeInfo(d_stn); + const std::vector& 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& 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& exOut) const; + /** Pointer to the sygus term database */ + TermDbSygus* d_tds; + /** pointer to the example inference class */ + std::vector> 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> d_exOutCache; +}; + +} // namespace quantifiers +} // namespace theory +} /* namespace CVC4 */ + +#endif