Node bad_val_bvr;
bool by_examples = false;
if( itsv==d_cache[a].d_search_val[tn].end() ){
- // TODO (github #1210) conjecture-specific symmetry breaking
- // this should be generalized and encapsulated within the
- // SynthConjecture class.
// Is it equivalent under examples?
Node bvr_equiv;
if (options::sygusSymBreakPbe())
{
- if (aconj->getPbe()->hasExamples(a))
+ // If the enumerator has examples, see if it is equivalent up to its
+ // examples with a previous term.
+ quantifiers::ExampleEvalCache* eec = aconj->getExampleEvalCache(a);
+ if (eec != nullptr)
{
- bvr_equiv = aconj->getPbe()->addSearchVal(tn, a, bvr);
+ bvr_equiv = eec->addSearchVal(bvr);
}
}
if( !bvr_equiv.isNull() ){
#include "options/base_options.h"
#include "options/quantifiers_options.h"
#include "printer/printer.h"
+#include "theory/quantifiers/sygus/example_min_eval.h"
#include "theory/quantifiers/sygus/synth_conjecture.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers_engine.h"
: "")
<< "..." << std::endl;
// see if any refinement lemma is refuted by evaluation
- std::vector<Node> cre_lems;
- bool ret =
- getRefinementEvalLemmas(candidates, candidate_values, cre_lems, doGen);
- if (ret && !doGen)
+ if (doGen)
{
- Trace("cegqi-engine") << "...(actively enumerated) candidate failed "
- "refinement lemma evaluation."
- << std::endl;
- return true;
- }
- if (!cre_lems.empty())
- {
- lems.insert(lems.end(), cre_lems.begin(), cre_lems.end());
- addedEvalLemmas = true;
- if (Trace.isOn("cegqi-lemma"))
+ std::vector<Node> cre_lems;
+ getRefinementEvalLemmas(candidates, candidate_values, cre_lems);
+ if (!cre_lems.empty())
{
- for (const Node& lem : cre_lems)
+ lems.insert(lems.end(), cre_lems.begin(), cre_lems.end());
+ addedEvalLemmas = true;
+ if (Trace.isOn("cegqi-lemma"))
{
- Trace("cegqi-lemma")
- << "Cegqi::Lemma : ref evaluation : " << lem << std::endl;
+ for (const Node& lem : cre_lems)
+ {
+ Trace("cegqi-lemma")
+ << "Cegqi::Lemma : ref evaluation : " << lem << std::endl;
+ }
}
+ /* we could, but do not return here. experimentally, it is better to
+ add the lemmas below as well, in parallel. */
+ }
+ }
+ else
+ {
+ // just check whether the refinement lemmas are satisfied, fail if not
+ if (checkRefinementEvalLemmas(candidates, candidate_values))
+ {
+ Trace("cegqi-engine") << "...(actively enumerated) candidate failed "
+ "refinement lemma evaluation."
+ << std::endl;
+ return true;
}
- /* we could, but do not return here. experimentally, it is better to
- add the lemmas below as well, in parallel. */
}
}
// we only do evaluation unfolding for passive enumerators
bool Cegis::usingRepairConst() { return true; }
bool Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs,
const std::vector<Node>& ms,
- std::vector<Node>& lems,
- bool doGen)
+ std::vector<Node>& lems)
{
Trace("sygus-cref-eval") << "Cref eval : conjecture has "
<< d_refinement_lemma_unit.size() << " unit and "
Node nfalse = nm->mkConst(false);
Node neg_guard = d_parent->getGuard().negate();
bool ret = false;
+
for (unsigned r = 0; r < 2; r++)
{
std::unordered_set<Node, NodeHashFunction>& rlemmas =
<< "...after unfolding is : " << lemcsu << std::endl;
if (lemcsu.isConst() && !lemcsu.getConst<bool>())
{
- if (!doGen)
- {
- // we are not generating the lemmas, instead just return
- return true;
- }
ret = true;
std::vector<Node> msu;
std::vector<Node> mexp;
* to lems based on evaluating the conjecture, instantiated for ms, on lemmas
* for previous refinements (d_refinement_lemmas).
*
- * Returns true if any such lemma exists. If doGen is false, then the
- * lemmas are not generated or added to lems.
+ * Returns true if any such lemma exists.
*/
bool getRefinementEvalLemmas(const std::vector<Node>& vs,
const std::vector<Node>& ms,
- std::vector<Node>& lems,
- bool doGen);
+ std::vector<Node>& lems);
/** Check refinement evaluation lemmas
*
* This method is similar to above, but does not perform any generalization
return Node::null();
}
std::vector<Node> vals;
- evaluateVec(bv, vals, false);
+ evaluateVec(bv, vals, true);
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)
+ // be discarded. This applies also to the case where the evaluation
+ // was cached prior to this call.
+ if (ret != bv)
{
- std::vector<Node>& eocv = d_exOutCache[bv];
- eocv.insert(eocv.end(), vals.begin(), vals.end());
+ clearEvaluationCache(bv);
}
Assert(ret.getType().isComparableTo(bv.getType()));
return ret;
#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/quantifiers/sygus/synth_engine.h"
using namespace CVC4::kind;
SygusEnumerator::TermCache::TermCache()
: d_tds(nullptr),
- d_pbe(nullptr),
+ d_eec(nullptr),
d_isSygusType(false),
d_numConClasses(0),
d_sizeEnum(0),
d_sampleRrVInit(false)
{
}
-void SygusEnumerator::TermCache::initialize(
- SygusStatistics* s, Node e, TypeNode tn, TermDbSygus* tds, SygusPbe* pbe)
+
+void SygusEnumerator::TermCache::initialize(SygusStatistics* s,
+ Node e,
+ TypeNode tn,
+ TermDbSygus* tds,
+ ExampleEvalCache* eec)
{
Trace("sygus-enum-debug") << "Init term cache " << tn << "..." << std::endl;
d_stats = s;
d_enum = e;
d_tn = tn;
d_tds = tds;
- d_pbe = pbe;
+ d_eec = eec;
d_sizeStartIndex[0] = 0;
d_isSygusType = false;
return false;
}
// if we are doing PBE symmetry breaking
- if (d_pbe != nullptr)
+ if (d_eec != nullptr)
{
++(d_stats->d_enumTermsExampleEval);
// Is it equivalent under examples?
- Node bne = d_pbe->addSearchVal(d_tn, d_enum, bnr);
+ Node bne = d_eec->addSearchVal(bnr);
if (!bne.isNull())
{
if (bnr != bne)
void SygusEnumerator::initializeTermCache(TypeNode tn)
{
// initialize the term cache
- // see if we use sygus PBE for symmetry breaking
- SygusPbe* pbe = nullptr;
+ // see if we use an example evaluation cache for symmetry breaking
+ ExampleEvalCache* eec = nullptr;
if (options::sygusSymBreakPbe())
{
- pbe = d_parent->getPbe();
- if (!pbe->hasExamples(d_enum))
- {
- pbe = nullptr;
- }
+ eec = d_parent->getExampleEvalCache(d_enum);
}
- d_tcache[tn].initialize(&d_stats, d_enum, tn, d_tds, pbe);
+ d_tcache[tn].initialize(&d_stats, d_enum, tn, d_tds, eec);
}
SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn)
Node e,
TypeNode tn,
TermDbSygus* tds,
- SygusPbe* pbe = nullptr);
+ ExampleEvalCache* ece = nullptr);
/** get last constructor class index for weight
*
* This returns a minimal index n such that all constructor classes at
TypeNode d_tn;
/** pointer to term database sygus */
TermDbSygus* d_tds;
- /** pointer to the PBE utility (used for symmetry breaking) */
- SygusPbe* d_pbe;
+ /**
+ * Pointer to the example evaluation cache utility (used for symmetry
+ * breaking).
+ */
+ ExampleEvalCache* d_eec;
//-------------------------static information about type
/** is d_tn a sygus type? */
bool d_isSygusType;
{
// compute the current examples
d_bvr = bvr;
- if (aconj->getPbe()->hasExamples(e))
+ Assert(tds != nullptr);
+ ExampleEvalCache* eec = aconj->getExampleEvalCache(e);
+ if (eec != nullptr)
{
+ // get the result of evaluating bvr on the examples of enumerator e.
+ eec->evaluateVec(bvr, d_exo, false);
d_conj = aconj;
d_enum = e;
- unsigned nex = aconj->getPbe()->getNumExamples(e);
- for (unsigned i = 0; i < nex; i++)
- {
- d_exo.push_back(d_conj->getPbe()->evaluateBuiltin(tn, bvr, e, i));
- }
}
}
if (!d_enum.isNull())
{
bool ex_equiv = true;
- for (unsigned j = 0; j < d_exo.size(); j++)
+ ExampleEvalCache* eec = d_conj->getExampleEvalCache(d_enum);
+ Assert(eec != nullptr);
+ for (unsigned j = 0, esize = d_exo.size(); j < esize; j++)
{
- Node nbvr_ex = d_conj->getPbe()->evaluateBuiltin(tn, nbvr, d_enum, j);
+ Node nbvr_ex = eec->evaluate(nbvr, j);
if (nbvr_ex != d_exo[j])
{
ex_equiv = false;
#include "expr/datatype.h"
#include "options/quantifiers_options.h"
+#include "theory/quantifiers/sygus/example_infer.h"
#include "theory/quantifiers/sygus/synth_conjecture.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
SygusPbe::~SygusPbe() {}
-//--------------------------------- collecting finite input/output domain information
-
-bool SygusPbe::collectExamples(Node n,
- std::map<Node, bool>& visited,
- bool hasPol,
- bool pol)
-{
- if( visited.find( n )==visited.end() ){
- visited[n] = true;
- Node neval;
- Node n_output;
- bool neval_is_evalapp = false;
- if (n.getKind() == DT_SYGUS_EVAL)
- {
- neval = n;
- if( hasPol ){
- n_output = pol ? d_true : d_false;
- }
- neval_is_evalapp = true;
- }
- else if (n.getKind() == EQUAL && hasPol && pol)
- {
- for( unsigned r=0; r<2; r++ ){
- if (n[r].getKind() == DT_SYGUS_EVAL)
- {
- neval = n[r];
- if( n[1-r].isConst() ){
- n_output = n[1-r];
- }
- neval_is_evalapp = true;
- }
- }
- }
- // is it an evaluation function?
- if (neval_is_evalapp && d_examples.find(neval[0]) != d_examples.end())
- {
- Trace("sygus-pbe-debug")
- << "Process head: " << n << " == " << n_output << std::endl;
- // If n_output is null, then neval does not have a constant value
- // If n_output is non-null, then neval is constrained to always be
- // that value.
- if (!n_output.isNull())
- {
- std::map<Node, Node>::iterator itet = d_exampleTermMap.find(neval);
- if (itet == d_exampleTermMap.end())
- {
- d_exampleTermMap[neval] = n_output;
- }
- else if (itet->second != n_output)
- {
- // We have a conflicting pair f( c ) = d1 ^ f( c ) = d2 for d1 != d2,
- // the conjecture is infeasible.
- return false;
- }
- }
- // get the evaluation head
- Node eh = neval[0];
- std::map<Node, bool>::iterator itx = d_examples_invalid.find(eh);
- if (itx == d_examples_invalid.end())
- {
- // collect example
- bool success = true;
- std::vector<Node> ex;
- for (unsigned j = 1, nchild = neval.getNumChildren(); j < nchild; j++)
- {
- if (!neval[j].isConst())
- {
- success = false;
- break;
- }
- ex.push_back(neval[j]);
- }
- if (success)
- {
- d_examples[eh].push_back(ex);
- d_examples_out[eh].push_back(n_output);
- d_examples_term[eh].push_back(neval);
- if (n_output.isNull())
- {
- d_examples_out_invalid[eh] = true;
- }
- else
- {
- Assert(n_output.isConst());
- // finished processing this node if it was an I/O pair
- return true;
- }
- }
- else
- {
- d_examples_invalid[eh] = true;
- d_examples_out_invalid[eh] = true;
- }
- }
- }
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- bool newHasPol;
- bool newPol;
- QuantPhaseReq::getEntailPolarity(n, i, hasPol, pol, newHasPol, newPol);
- if (!collectExamples(n[i], visited, newHasPol, newPol))
- {
- return false;
- }
- }
- }
- return true;
-}
-
bool SygusPbe::initialize(Node conj,
Node n,
const std::vector<Node>& candidates,
Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
NodeManager* nm = NodeManager::currentNM();
- for (unsigned i = 0; i < candidates.size(); i++)
- {
- Node v = candidates[i];
- d_examples[v].clear();
- d_examples_out[v].clear();
- d_examples_term[v].clear();
- }
-
- std::map<Node, bool> visited;
- // n is negated conjecture
- if (!collectExamples(n, visited, true, false))
- {
- Trace("sygus-pbe") << "...conflicting examples" << std::endl;
- Node infeasible = d_parent->getGuard().negate();
- lemmas.push_back(infeasible);
- return false;
- }
-
- for (unsigned i = 0; i < candidates.size(); i++)
- {
- Node v = candidates[i];
- Trace("sygus-pbe") << " examples for " << v << " : ";
- if (d_examples_invalid.find(v) != d_examples_invalid.end())
- {
- Trace("sygus-pbe") << "INVALID" << std::endl;
- }
- else
- {
- Trace("sygus-pbe") << std::endl;
- for (unsigned j = 0; j < d_examples[v].size(); j++)
- {
- Trace("sygus-pbe") << " ";
- for (unsigned k = 0; k < d_examples[v][j].size(); k++)
- {
- Trace("sygus-pbe") << d_examples[v][j][k] << " ";
- }
- if (!d_examples_out[v][j].isNull())
- {
- Trace("sygus-pbe") << " -> " << d_examples_out[v][j];
- }
- Trace("sygus-pbe") << std::endl;
- }
- }
- }
-
if (!options::sygusUnifPbe())
{
// we are not doing unification
}
// check if all candidates are valid examples
+ ExampleInfer* ei = d_parent->getExampleInfer();
d_is_pbe = true;
for (const Node& c : candidates)
{
- if (d_examples[c].empty()
- || d_examples_out_invalid.find(c) != d_examples_out_invalid.end())
+ // if it has no examples or the output of the examples is invalid
+ if (ei->getNumExamples(c) == 0 || !ei->hasExamplesOut(c))
{
d_is_pbe = false;
return false;
}
for (const Node& c : candidates)
{
- Assert(d_examples.find(c) != d_examples.end());
+ Assert(ei->hasExamples(c));
+ d_sygus_unif[c].reset(new SygusUnifIo(d_parent));
Trace("sygus-pbe") << "Initialize unif utility for " << c << "..."
<< std::endl;
std::map<Node, std::vector<Node>> strategy_lemmas;
- d_sygus_unif[c].initializeCandidate(
+ d_sygus_unif[c]->initializeCandidate(
d_qe, c, d_candidate_to_enum[c], strategy_lemmas);
Assert(!d_candidate_to_enum[c].empty());
Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size()
d_tds->registerSymBreakLemma(e, lem, etn, 0, false);
}
}
- Trace("sygus-pbe") << "Initialize " << d_examples[c].size()
- << " example points for " << c << "..." << std::endl;
- // initialize the examples
- for (unsigned i = 0, nex = d_examples[c].size(); i < nex; i++)
- {
- d_sygus_unif[c].addExample(d_examples[c][i], d_examples_out[c][i]);
- }
}
return true;
}
-Node SygusPbe::PbeTrie::addTerm(Node b, const std::vector<Node>& exOut)
-{
- PbeTrie* curr = this;
- for (const Node& eo : exOut)
- {
- curr = &(curr->d_children[eo]);
- }
- if (!curr->d_children.empty())
- {
- return curr->d_children.begin()->first;
- }
- curr->d_children.insert(std::pair<Node, PbeTrie>(b, PbeTrie()));
- return b;
-}
-
-bool SygusPbe::hasExamples(Node e)
-{
- 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;
-}
-
-unsigned SygusPbe::getNumExamples(Node e)
-{
- e = d_tds->getSynthFunForEnumerator(e);
- Assert(!e.isNull());
- std::map<Node, std::vector<std::vector<Node> > >::iterator it =
- d_examples.find(e);
- if (it != d_examples.end()) {
- return it->second.size();
- } else {
- return 0;
- }
-}
-
-void SygusPbe::getExample(Node e, unsigned i, std::vector<Node>& ex)
-{
- e = d_tds->getSynthFunForEnumerator(e);
- Assert(!e.isNull());
- std::map<Node, std::vector<std::vector<Node> > >::iterator it =
- d_examples.find(e);
- if (it != d_examples.end()) {
- Assert(i < it->second.size());
- ex.insert(ex.end(), it->second[i].begin(), it->second[i].end());
- } else {
- Assert(false);
- }
-}
-
-Node SygusPbe::getExampleOut(Node e, unsigned i)
-{
- e = d_tds->getSynthFunForEnumerator(e);
- Assert(!e.isNull());
- std::map<Node, std::vector<Node> >::iterator it = d_examples_out.find(e);
- if (it != d_examples_out.end()) {
- Assert(i < it->second.size());
- return it->second[i];
- } else {
- Assert(false);
- return Node::null();
- }
-}
-
-Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr)
-{
- Assert(!e.isNull());
- if (d_tds->isVariableAgnosticEnumerator(e))
- {
- // we cannot apply conjecture-specific symmetry breaking on variable
- // agnostic enumerators
- return Node::null();
- }
- Node ee = d_tds->getSynthFunForEnumerator(e);
- Assert(!e.isNull());
- std::map<Node, bool>::iterator itx = d_examples_invalid.find(ee);
- if (itx == d_examples_invalid.end()) {
- std::vector<Node> vals;
- Trace("sygus-pbe-debug")
- << "Compute examples " << bvr << "..." << std::endl;
- 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 (d_is_pbe)
- {
- // 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().isComparableTo(bvr.getType()));
- return ret;
- }
- return Node::null();
-}
-
-Node SygusPbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i)
-{
- 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()) {
- std::map<Node, std::vector<std::vector<Node> > >::iterator it =
- d_examples.find(e);
- if (it != d_examples.end()) {
- Assert(i < it->second.size());
- return d_tds->evaluateBuiltin(tn, bn, it->second[i]);
- }
- }
- return Rewriter::rewrite(bn);
-}
-
// ------------------------------------------- solution construction from enumeration
void SygusPbe::getTermList(const std::vector<Node>& candidates,
Assert(d_enum_to_candidate.find(e) != d_enum_to_candidate.end());
Node c = d_enum_to_candidate[e];
std::vector<Node> enum_lems;
- d_sygus_unif[c].notifyEnumeration(e, v, enum_lems);
+ d_sygus_unif[c]->notifyEnumeration(e, v, enum_lems);
if (!enum_lems.empty())
{
// the lemmas must be guarded by the active guard of the enumerator
Node c = candidates[i];
//build decision tree for candidate
std::vector<Node> sol;
- if (d_sygus_unif[c].constructSolution(sol, lems))
+ if (d_sygus_unif[c]->constructSolution(sol, lems))
{
Assert(sol.size() == 1);
candidate_values.push_back(sol[0]);
*
* [EX#1] An example of a synthesis conjecture in PBE form is :
* exists f. forall x.
- * ( x = 0 => f( x ) = 2 ) ^ ( x = 5 => f( x ) = 7 ) ^ ( x = 6 => f( x ) = 8 )
+ * ( f( 0 ) = 2 ) ^ ( f( 5 ) = 7 ) ^ ( f( 6 ) = 8 )
*
* We say that the above conjecture has I/O examples (0)->2, (5)->7, (6)->8.
*
* Internally, this class does the following for SyGuS inputs:
*
- * (1) Infers whether the input conjecture is in PBE form or not.
+ * (1) Infers whether the input conjecture is in PBE form or not, which
+ * is based on looking up information in the ExampleInfer utility.
* (2) Based on this information and on the syntactic restrictions, it
* devises a strategy for enumerating terms and construction solutions,
* which is inspired by Alur et al. "Scaling Enumerative Program Synthesis
* syntactic restrictions for it. The search may continue unless all enumerators
* become inactive.
*
- * (4) 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 the above conjecture, 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
- * SygusPbe::addSearchVal(...).
- * For details, see Reynolds et al. SYNT 2017.
- *
- * (5) When the extension of quantifier-free datatypes procedure for SyGuS
+ * (4) When the extension of quantifier-free datatypes procedure for SyGuS
* datatypes terminates with a model, the parent of this class calls
* SygusPbe::getCandidateList(...), where this class returns the list
* of active enumerators.
- * (6) The parent class subsequently calls
+ * (5) The parent class subsequently calls
* SygusPbe::constructValues(...), which informs this class that new
* values have been enumerated for active enumerators, as indicated by the
* current model. This call also requests that based on these
std::vector<Node>& lems) override;
/** is PBE enabled for any enumerator? */
bool isPbe() { return d_is_pbe; }
- /**
- * 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 examples for enumerator e */
- unsigned getNumExamples(Node e);
- /**
- * 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 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 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
- * 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 above example
- * [EX#1], then
- * evaluateBuiltin( tn, bn, e, 0 ) = 7
- * evaluateBuiltin( tn, bn, e, 1 ) = 9
- * evaluateBuiltin( tn, bn, e, 2 ) = 10
- */
- Node evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i);
private:
/** true and false nodes */
Node d_false;
/** is this a PBE conjecture for any function? */
bool d_is_pbe;
- /** for each candidate variable f (a function-to-synthesize), whether the
- * conjecture is purely PBE for that variable
- * In other words, all occurrences of f are guarded by equalities that
- * constraint its arguments to constants.
- */
- std::map<Node, bool> d_examples_invalid;
- /** for each candidate variable (function-to-synthesize), whether the
- * conjecture is purely PBE for that variable.
- * An example of a conjecture for which d_examples_invalid is false but
- * d_examples_out_invalid is true is:
- * exists f. forall x. ( x = 0 => f( x ) > 2 )
- * another example is:
- * exists f. forall x. ( ( x = 0 => f( x ) = 2 ) V ( x = 3 => f( x ) = 3 ) )
- * since the formula is not a conjunction (the example values are not
- * entailed).
- * However, the domain of f in both cases is finite, which can be used for
- * search space pruning.
- */
- std::map<Node, bool> d_examples_out_invalid;
/**
* Map from candidates to sygus unif utility. This class implements
* the core algorithm (e.g. decision tree learning) that this module relies
* upon.
*/
- std::map<Node, SygusUnifIo> d_sygus_unif;
+ std::map<Node, std::unique_ptr<SygusUnifIo> > d_sygus_unif;
/**
* map from candidates to the list of enumerators that are being used to
* build solutions for that candidate by the above utility.
std::map<Node, std::vector<Node> > d_candidate_to_enum;
/** reverse map of above */
std::map<Node, Node> d_enum_to_candidate;
- /** for each candidate variable (function-to-synthesize), input of I/O
- * examples */
- std::map<Node, std::vector<std::vector<Node> > > d_examples;
- /** for each candidate variable (function-to-synthesize), output of I/O
- * examples */
- std::map<Node, std::vector<Node> > d_examples_out;
- /** the list of example terms
- * For the example [EX#1] above, this is f( 0 ), f( 5 ), f( 6 )
- */
- std::map<Node, std::vector<Node> > d_examples_term;
- /**
- * Map from example input terms to their output, for example [EX#1] above,
- * this is { f( 0 ) -> 2, f( 5 ) -> 7, f( 6 ) -> 8 }.
- */
- std::map<Node, Node> d_exampleTermMap;
- /** collect the PBE examples in n
- * This is called on the input conjecture, and will populate the above
- * vectors, where hasPol/pol denote the polarity of n in the conjecture. This
- * function returns false if it finds two examples that are contradictory.
- */
- bool collectExamples(Node n,
- std::map<Node, bool>& visited,
- bool hasPol,
- bool pol);
-
- //--------------------------------- PBE search values
- /**
- * This class 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.
- */
- class PbeTrie
- {
- public:
- PbeTrie() {}
- ~PbeTrie() {}
- /** the children for this node in the trie */
- std::map<Node, PbeTrie> d_children;
- /** clear this trie */
- void clear() { d_children.clear(); }
- /**
- * Add term b whose value on examples is exOut to the trie. Return
- * the first term registered to this trie whose evaluation was exOut.
- */
- Node addTerm(Node b, const std::vector<Node>& exOut);
- };
- /** trie of candidate solutions tried
- * This stores information for each (enumerator, type),
- * where type is a type in the grammar of the space of solutions for a subterm
- * of e. This is used for symmetry breaking in quantifier-free reasoning
- * about SyGuS datatypes.
- */
- std::map<Node, std::map<TypeNode, PbeTrie> > d_pbe_trie;
- //--------------------------------- end PBE search values
};
} /* namespace CVC4::theory::quantifiers */
#include "options/quantifiers_options.h"
#include "theory/evaluator.h"
+#include "theory/quantifiers/sygus/example_infer.h"
+#include "theory/quantifiers/sygus/synth_conjecture.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
#include "util/random.h"
#include <math.h>
getLeavesInternal(vals, pol, v, 0, -2);
}
-SygusUnifIo::SygusUnifIo()
- : d_check_sol(false),
+SygusUnifIo::SygusUnifIo(SynthConjecture* p)
+ : d_parent(p),
+ d_check_sol(false),
d_cond_count(0),
d_sol_term_size(0),
d_sol_cons_nondet(false),
}
SygusUnifIo::~SygusUnifIo() {}
+
void SygusUnifIo::initializeCandidate(
QuantifiersEngine* qe,
Node f,
std::vector<Node>& enums,
std::map<Node, std::vector<Node>>& strategy_lemmas)
{
+ d_candidate = f;
+ // copy the examples from the parent
+ ExampleInfer* ei = d_parent->getExampleInfer();
d_examples.clear();
d_examples_out.clear();
+ // copy the examples
+ if (ei->hasExamples(f))
+ {
+ for (unsigned i = 0, nex = ei->getNumExamples(f); i < nex; i++)
+ {
+ std::vector<Node> input;
+ ei->getExample(f, i, input);
+ Node output = ei->getExampleOut(f, i);
+ d_examples.push_back(input);
+ d_examples_out.push_back(output);
+ }
+ }
d_ecache.clear();
- d_candidate = f;
SygusUnif::initializeCandidate(qe, f, enums, strategy_lemmas);
// learn redundant operators based on the strategy
d_strategy[f].staticLearnRedundantOps(strategy_lemmas);
}
-void SygusUnifIo::addExample(const std::vector<Node>& input, Node output)
-{
- d_examples.push_back(input);
- d_examples_out.push_back(output);
-}
-
-void SygusUnifIo::computeExamples(Node e, Node bv, std::vector<Node>& exOut)
-{
- std::map<Node, std::vector<Node>>& eoc = d_exOutCache[e];
- std::map<Node, std::vector<Node>>::iterator it = eoc.find(bv);
- if (it != eoc.end())
- {
- exOut.insert(exOut.end(), it->second.begin(), it->second.end());
- return;
- }
- TypeNode xtn = e.getType();
- std::vector<Node>& eocv = eoc[bv];
- for (size_t j = 0, size = d_examples.size(); j < size; j++)
- {
- Node res = d_tds->evaluateBuiltin(xtn, bv, d_examples[j]);
- exOut.push_back(res);
- eocv.push_back(res);
- }
-}
-
-void SygusUnifIo::clearExampleCache(Node e, Node bv)
-{
- std::map<Node, std::vector<Node>>& eoc = d_exOutCache[e];
- Assert(eoc.find(bv) != eoc.end());
- eoc.erase(bv);
-}
-
void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
{
Trace("sygus-sui-enum") << "Notify enumeration for " << e << " : " << v
bv = d_tds->getExtRewriter()->extendedRewrite(bv);
Trace("sygus-sui-enum") << "PBE Compute Examples for " << bv << std::endl;
// compte the results (should be cached)
- computeExamples(e, bv, base_results);
- // don't need it after this
- clearExampleCache(e, bv);
+ ExampleEvalCache* eec = d_parent->getExampleEvalCache(e);
+ Assert(eec != nullptr);
+ // Evaluate, which should be cached (assuming we have performed example-based
+ // symmetry breaking on bv). Moreover don't cache the result in the case it
+ // is not there already, since we won't need this evaluation anywhere outside
+ // of this class.
+ eec->evaluateVec(bv, base_results);
// get the results for each slave enumerator
std::map<Node, std::vector<Node>> srmap;
Evaluator* ev = d_tds->getEvaluator();
int status);
};
+class SynthConjecture;
+
/** Sygus unification I/O utility
*
* This class implement synthesis-by-unification, where the specification is
- * I/O examples. With respect to SygusUnif, it's main interface function is
- * addExample, which adds an I/O example to the specification.
+ * I/O examples.
*
* Since I/O specifications for multiple functions can be fully separated, we
* assume that this class is used only for a single function to synthesize.
*
* In addition to the base class which maintains a strategy tree, this class
* maintains:
- * (1) A set of input/output examples that are the specification for f. This
- * can be updated via calls to resetExmaples/addExamples,
+ * (1) A set of input/output examples that are the specification for f.
* (2) A set of terms that have been enumerated for enumerators (d_ecache). This
* can be updated via calls to notifyEnumeration.
*/
friend class UnifContextIo;
public:
- SygusUnifIo();
+ SygusUnifIo(SynthConjecture* p);
~SygusUnifIo();
/** initialize
+ *
+ * This initializes this class for solving PBE conjectures for
+ * function-to-synthesize f.
*
* We only initialize for one function f, since I/O specifications across
* multiple functions can be separated.
/** Construct solution */
bool constructSolution(std::vector<Node>& sols,
std::vector<Node>& lemmas) override;
-
- /** add example
- *
- * This adds input -> output to the specification for f. The arity of
- * input should be equal to the number of arguments in the sygus variable
- * list of the grammar of f. That is, if we are searching for solutions for f
- * of the form (lambda v1...vn. t), then the arity of input should be n.
- */
- void addExample(const std::vector<Node>& input, Node output);
-
- /** compute examples
- *
- * This adds the result of evaluating bv on the set of input examples managed
- * by this class. Term bv is the builtin version of a term generated for
- * enumerator e. It stores the resulting output for each example in exOut.
- */
- void computeExamples(Node e, Node bv, std::vector<Node>& exOut);
-
- /** clear example cache */
- void clearExampleCache(Node e, Node bv);
-
protected:
- /** the candidate */
+ /** The synthesis conjecture */
+ SynthConjecture* d_parent;
+ /** the function-to-synthesize */
Node d_candidate;
/**
* Whether we will try to construct solution on the next call to
/** output of I/O examples */
std::vector<Node> d_examples_out;
- /** cache for computeExamples */
- std::map<Node, std::map<Node, std::vector<Node>>> d_exOutCache;
-
/**
* This class stores information regarding an enumerator, including:
* a database of values that have been enumerated for this enumerator.
projects / cvc5.git / commitdiff