diff options
Diffstat (limited to 'src/theory/quantifiers/sygus')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 52 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.h | 62 |
2 files changed, 81 insertions, 33 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 5c0985f7e..0fa857c91 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -313,13 +313,16 @@ Node SygusPbe::PbeTrie::addTerm(Node b, const std::vector<Node>& exOut) bool SygusPbe::hasExamples(Node e) { - if (isPbe()) { - e = d_tds->getSynthFunForEnumerator(e); - Assert(!e.isNull()); - std::map<Node, bool>::iterator itx = d_examples_invalid.find(e); - if (itx == d_examples_invalid.end()) { - return d_examples.find(e) != d_examples.end(); - } + e = d_tds->getSynthFunForEnumerator(e); + if (e.isNull()) + { + // enumerator is not associated with synthesis function? + return false; + } + std::map<Node, bool>::iterator itx = d_examples_invalid.find(e); + if (itx == d_examples_invalid.end()) + { + return d_examples.find(e) != d_examples.end(); } return false; } @@ -367,7 +370,6 @@ Node SygusPbe::getExampleOut(Node e, unsigned i) Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr) { - Assert(isPbe()); Assert(!e.isNull()); if (d_tds->isVariableAgnosticEnumerator(e)) { @@ -379,20 +381,44 @@ Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr) Assert(!e.isNull()); std::map<Node, bool>::iterator itx = d_examples_invalid.find(ee); if (itx == d_examples_invalid.end()) { - // compute example values with the I/O utility std::vector<Node> vals; Trace("sygus-pbe-debug") << "Compute examples " << bvr << "..." << std::endl; - d_sygus_unif[ee].computeExamples(e, bvr, vals); + if (d_is_pbe) + { + // Compute example values with the I/O utility, which ensures they are + // not later recomputed when the enumerated term is given the I/O utility. + d_sygus_unif[ee].computeExamples(e, bvr, vals); + } + else + { + // If the I/O utility is not enabled (if the conjecture is not PBE), + // compute them separately. This handles the case when all applications + // of a function-to-synthesize are applied to constant arguments but + // the conjecture is not PBE. + TypeNode etn = e.getType(); + std::vector<std::vector<Node>>& exs = d_examples[ee]; + for (size_t i = 0, esize = exs.size(); i < esize; i++) + { + Node res = d_tds->evaluateBuiltin(etn, bvr, exs[i]); + vals.push_back(res); + } + } Assert(vals.size() == d_examples[ee].size()); Trace("sygus-pbe-debug") << "...got " << vals << std::endl; Trace("sygus-pbe-debug") << "Add to trie..." << std::endl; Node ret = d_pbe_trie[e][tn].addTerm(bvr, vals); Trace("sygus-pbe-debug") << "...got " << ret << std::endl; - if (ret != bvr) + if (d_is_pbe) { - Trace("sygus-pbe-debug") << "...clear example cache" << std::endl; - d_sygus_unif[ee].clearExampleCache(e, bvr); + // Clean up the cache data if necessary: if the enumerated term + // is redundant, its cached data will not be used later and thus should + // be cleared now. + if (ret != bvr) + { + Trace("sygus-pbe-debug") << "...clear example cache" << std::endl; + d_sygus_unif[ee].clearExampleCache(e, bvr); + } } Assert(ret.getType() == bvr.getType()); return ret; diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index 258fe017b..2e6ca2659 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -153,32 +153,54 @@ class SygusPbe : public SygusModule std::vector<Node>& lems) override; /** is PBE enabled for any enumerator? */ bool isPbe() { return d_is_pbe; } - /** is the enumerator e associated with I/O example pairs? */ + /** + * Is the enumerator e associated with examples? This is true if the + * function-to-synthesize associated with e is only applied to concrete + * arguments. Notice that the conjecture need not be in PBE form for this + * to be the case. For example, f has examples in: + * exists f. f( 1 ) = 3 ^ f( 2 ) = 4 + * exists f. f( 45 ) > 0 ^ f( 99 ) > 0 + * exists f. forall x. ( x > 5 => f( 4 ) < x ) + * It does not have examples in: + * exists f. forall x. f( x ) > 5 + * exists f. f( f( 4 ) ) = 5 + * This class implements techniques for functions-to-synthesize that + * have examples. In particular, the method addSearchVal below can be + * called. + */ bool hasExamples(Node e); - /** get number of I/O example pairs for enumerator e */ + /** get number of examples for enumerator e */ unsigned getNumExamples(Node e); - /** get the input arguments for i^th I/O example for e, which is added to the - * vector ex */ + /** + * Get the input arguments for i^th example for e, which is added to the + * vector ex + */ void getExample(Node e, unsigned i, std::vector<Node>& ex); - /** get the output value of the i^th I/O example for enumerator e */ + /** + * Get the output value of the i^th example for enumerator e, or null if + * it does not exist (an example does not have an associate output if it is + * not a top-level equality). + */ Node getExampleOut(Node e, unsigned i); /** add the search val - * This function is called by the extension of quantifier-free datatypes - * procedure for SyGuS datatypes when we are considering a value of - * enumerator e of sygus type tn whose analog in the signature of builtin - * theory is bvr. - * - * For example, bvr = x + 1 when e is the datatype value Plus( x(), One() ) and - * tn is a sygus datatype that encodes a subsignature of the integers. - * - * This returns either: - * - A SyGuS term whose analog is equivalent to bvr up to examples - * In the above example, - * it may return a term t of the form Plus( One(), x() ), such that this - * function was previously called with t as input. - * - e, indicating that no previous terms are equivalent to e up to examples. - */ + * This function is 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 of sygus type tn whose analog in the + * signature of builtin theory is bvr. + * + * For example, bvr = x + 1 when e is the datatype value Plus( x(), One() ) + * and tn is a sygus datatype that encodes a subsignature of the integers. + * + * This returns either: + * - A SyGuS term whose analog is equivalent to bvr up to examples + * In the above example, + * it may return a term t of the form Plus( One(), x() ), such that this + * function was previously called with t as input. + * - e, indicating that no previous terms are equivalent to e up to examples. + * + * This method should only be called if hasExamples(e) returns true. + */ Node addSearchVal(TypeNode tn, Node e, Node bvr); /** evaluate builtin * This returns the evaluation of bn on the i^th example for the |