From 8a64433caffd3bedd99c0e73dac0941b87060778 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 8 Feb 2018 14:01:17 -0600 Subject: [PATCH] Minor improvements to sygus sampling. (#1577) --- src/options/quantifiers_options | 6 +- src/smt/smt_engine.cpp | 7 +- src/theory/datatypes/datatypes_sygus.cpp | 30 ++++ .../quantifiers/ce_guided_conjecture.cpp | 57 ++----- src/theory/quantifiers/ce_guided_conjecture.h | 2 +- src/theory/quantifiers/sygus_sampler.cpp | 159 ++++++++++++++++-- src/theory/quantifiers/sygus_sampler.h | 78 ++++++--- 7 files changed, 257 insertions(+), 82 deletions(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 48a577faf..e97f11db9 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -300,9 +300,11 @@ option cegisSample --cegis-sample=MODE CVC4::theory::quantifiers::CegisSampleMod mode for using samples in the counterexample-guided inductive synthesis loop # internal uses of sygus -option sygusRewSynth --sygus-rr-synth bool :default false +option sygusRew --sygus-rr bool :default false + use sygus to enumerate and verify correctness of rewrite rules via sampling +option sygusRewSynth --sygus-rr-synth bool :read-write :default false use sygus to enumerate candidate rewrite rules via sampling -option sygusRewVerify --sygus-rr-verify bool :default false +option sygusRewVerify --sygus-rr-verify bool :read-write :default false use sygus to verify the correctness of rewrite rules via sampling option sygusSamples --sygus-samples=N int :read-write :default 100 :read-write number of points to consider when doing sygus rewriter sample testing diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6af5e38d5..fdd72ba2e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1885,7 +1885,12 @@ void SmtEngine::setDefaults() { if( !options::instNoEntail.wasSetByUser() ){ options::instNoEntail.set( false ); } - if (options::sygusRewSynth()) + if (options::sygusRew()) + { + options::sygusRewSynth.set(true); + options::sygusRewVerify.set(true); + } + if (options::sygusRewSynth() || options::sygusRewVerify()) { // rewrite rule synthesis implies that sygus stream must be true options::sygusStream.set(true); diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 5198b44d0..c0f7f0ac2 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -814,6 +814,36 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d, std::ostream* out = nodeManagerOptions.getOut(); (*out) << "(unsound-rewrite " << prev_bv << " " << bv << ")" << std::endl; + // debugging information + if (Trace.isOn("sygus-rr-debug")) + { + int pt_index = its->second.getDiffSamplePointIndex(bv, prev_bv); + if (pt_index >= 0) + { + Trace("sygus-rr-debug") + << "; both ext-rewrite to : " << bvr << std::endl; + Trace("sygus-rr-debug") + << "; but are not equivalent for : " << std::endl; + std::vector vars; + std::vector pt; + its->second.getSamplePoint(pt_index, vars, pt); + Assert(vars.size() == pt.size()); + for (unsigned i = 0, size = pt.size(); i < size; i++) + { + Trace("sygus-rr-debug") + << "; " << vars[i] << " -> " << pt[i] << std::endl; + } + Node bv_e = its->second.evaluate(bv, pt_index); + Node pbv_e = its->second.evaluate(prev_bv, pt_index); + Assert(bv_e != pbv_e); + Trace("sygus-rr-debug") << "; where they evaluate to " << pbv_e + << " and " << bv_e << std::endl; + } + else + { + Assert(false); + } + } } } } diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp index 889a80879..d325f3f36 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/ce_guided_conjecture.cpp @@ -626,7 +626,7 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation if (status != 0 && options::sygusRewSynth()) { TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus(); - std::map::iterator its = d_sampler.find(prog); + std::map::iterator its = d_sampler.find(prog); if (its == d_sampler.end()) { d_sampler[prog].initializeSygus( @@ -638,45 +638,21 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation // eq_sol is a candidate solution that is equivalent to sol if (eq_sol != solb) { - // one of eq_sol or solb must be ordered - bool eqor = its->second.isOrdered(eq_sol); - bool sor = its->second.isOrdered(solb); - bool outputRewrite = false; - if (eqor || sor) + // Terms solb and eq_sol are equivalent under sample points but do + // not rewrite to the same term. Hence, this indicates a candidate + // rewrite. + out << "(candidate-rewrite " << solb << " " << eq_sol << ")" + << std::endl; + // debugging information + if (Trace.isOn("sygus-rr-debug")) { - outputRewrite = true; - // if only one is ordered, then the ordered one must contain the - // free variables of the other - if (!eqor) - { - outputRewrite = its->second.containsFreeVariables(solb, eq_sol); - } - else if (!sor) - { - outputRewrite = its->second.containsFreeVariables(eq_sol, solb); - } - } - - if (outputRewrite) - { - // Terms solb and eq_sol are equivalent under sample points but do - // not rewrite to the same term. Hence, this indicates a candidate - // rewrite. - out << "(candidate-rewrite " << solb << " " << eq_sol << ")" - << std::endl; - // if the previous value stored was unordered, but this is - // ordered, we prefer this one. Thus, we force its addition to the - // sampler database. - if (!eqor) - { - its->second.registerTerm(solb, true); - } - } - else - { - Trace("sygus-synth-rr") - << "Alpha equivalent candidate rewrite : " << eq_sol << " " - << solb << std::endl; + ExtendedRewriter* er = sygusDb->getExtRewriter(); + Node solbr = er->extendedRewrite(solb); + Node eq_solr = er->extendedRewrite(eq_sol); + Trace("sygus-rr-debug") + << "; candidate #1 ext-rewrites to: " << solbr << std::endl; + Trace("sygus-rr-debug") + << "; candidate #2 ext-rewrites to: " << eq_solr << std::endl; } } } @@ -865,8 +841,9 @@ bool CegConjecture::sampleAddRefinementLemma(std::vector& vals, Trace("cegis-sample-debug") << "...false for point #" << i << std::endl; // mark this as a CEGIS point (no longer sampled) d_cegis_sample_refine.insert(i); + std::vector vars; std::vector pt; - d_cegis_sampler.getSamplePoint(i, pt); + d_cegis_sampler.getSamplePoint(i, vars, pt); Assert(d_base_vars.size() == pt.size()); Node rlem = d_base_body.substitute( d_base_vars.begin(), d_base_vars.end(), pt.begin(), pt.end()); diff --git a/src/theory/quantifiers/ce_guided_conjecture.h b/src/theory/quantifiers/ce_guided_conjecture.h index dae261111..ebcecbe0f 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.h +++ b/src/theory/quantifiers/ce_guided_conjecture.h @@ -261,7 +261,7 @@ private: * This is used for the sygusRewSynth() option to synthesize new candidate * rewrite rules. */ - std::map d_sampler; + std::map d_sampler; /** sampler object for the option cegisSample() * * This samples points of the type of the inner variables of the synthesis diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index f824cd6f7..c7c322132 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -74,16 +74,33 @@ void SygusSampler::initialize(TypeNode tn, d_is_valid = true; d_tn = tn; d_ftn = TypeNode::null(); + d_type_vars.clear(); + d_vars.clear(); + d_rvalue_cindices.clear(); + d_rvalue_null_cindices.clear(); + d_var_sygus_types.clear(); d_vars.insert(d_vars.end(), vars.begin(), vars.end()); - for (const Node& sv : vars) + std::map type_to_type_id; + unsigned type_id_counter = 0; + for (const Node& sv : d_vars) { TypeNode svt = sv.getType(); - d_var_index[sv] = d_type_vars[svt].size(); - d_type_vars[svt].push_back(sv); + unsigned tnid; + std::map::iterator itt = type_to_type_id.find(svt); + if (itt == type_to_type_id.end()) + { + type_to_type_id[svt] = type_id_counter; + type_id_counter++; + } + else + { + tnid = itt->second; + } + Trace("sygus-sample-debug") + << "Type id for " << sv << " is " << tnid << std::endl; + d_var_index[sv] = d_type_vars[tnid].size(); + d_type_vars[tnid].push_back(sv); } - d_rvalue_cindices.clear(); - d_rvalue_null_cindices.clear(); - d_var_sygus_types.clear(); initializeSamples(nsamples); } @@ -99,24 +116,68 @@ void SygusSampler::initializeSygus(TermDbSygus* tds, Node f, unsigned nsamples) Trace("sygus-sample") << "Register sampler for " << f << std::endl; + d_vars.clear(); + d_type_vars.clear(); d_var_index.clear(); d_type_vars.clear(); + d_rvalue_cindices.clear(); + d_rvalue_null_cindices.clear(); + d_var_sygus_types.clear(); // get the sygus variable list Node var_list = Node::fromExpr(dt.getSygusVarList()); if (!var_list.isNull()) { for (const Node& sv : var_list) { - TypeNode svt = sv.getType(); - d_var_index[sv] = d_type_vars[svt].size(); d_vars.push_back(sv); - d_type_vars[svt].push_back(sv); } } - d_rvalue_cindices.clear(); - d_rvalue_null_cindices.clear(); - d_var_sygus_types.clear(); + // register sygus type registerSygusType(d_ftn); + // Variables are associated with type ids based on the set of sygus types they + // appear in. + std::map var_to_type_id; + unsigned type_id_counter = 0; + for (const Node& sv : d_vars) + { + TypeNode svt = sv.getType(); + // is it equivalent to a previous variable? + for (const std::pair& v : var_to_type_id) + { + Node svc = v.first; + if (svc.getType() == svt) + { + if (d_var_sygus_types[sv].size() == d_var_sygus_types[svc].size()) + { + bool success = true; + for (unsigned t = 0, size = d_var_sygus_types[sv].size(); t < size; + t++) + { + if (d_var_sygus_types[sv][t] != d_var_sygus_types[svc][t]) + { + success = false; + break; + } + } + if (success) + { + var_to_type_id[sv] = var_to_type_id[svc]; + } + } + } + } + if (var_to_type_id.find(sv) == var_to_type_id.end()) + { + var_to_type_id[sv] = type_id_counter; + type_id_counter++; + } + unsigned tnid = var_to_type_id[sv]; + Trace("sygus-sample-debug") + << "Type id for " << sv << " is " << tnid << std::endl; + d_var_index[sv] = d_type_vars[tnid].size(); + d_type_vars[tnid].push_back(sv); + } + initializeSamples(nsamples); } @@ -231,7 +292,7 @@ bool SygusSampler::isContiguous(Node n) std::vector fvs; computeFreeVariables(n, fvs); // compute contiguous condition - for (const std::pair >& p : d_type_vars) + for (const std::pair >& p : d_type_vars) { bool foundNotFv = false; for (const Node& v : p.second) @@ -282,7 +343,7 @@ void SygusSampler::computeFreeVariables(Node n, std::vector& fvs) bool SygusSampler::isOrdered(Node n) { // compute free variables in n for each type - std::map > fvs; + std::map > fvs; std::unordered_set visited; std::unordered_set::iterator it; @@ -301,13 +362,13 @@ bool SygusSampler::isOrdered(Node n) std::map::iterator itv = d_var_index.find(cur); if (itv != d_var_index.end()) { - TypeNode tn = cur.getType(); + unsigned tnid = d_type_ids[cur]; // if this variable is out of order - if (itv->second != fvs[tn].size()) + if (itv->second != fvs[tnid].size()) { return false; } - fvs[tn].push_back(cur); + fvs[tnid].push_back(cur); } } for (unsigned j = 0, nchildren = cur.getNumChildren(); j < nchildren; j++) @@ -353,9 +414,12 @@ bool SygusSampler::containsFreeVariables(Node a, Node b) return true; } -void SygusSampler::getSamplePoint(unsigned index, std::vector& pt) +void SygusSampler::getSamplePoint(unsigned index, + std::vector& vars, + std::vector& pt) { Assert(index < d_samples.size()); + vars.insert(vars.end(), d_vars.begin(), d_vars.end()); std::vector& spt = d_samples[index]; pt.insert(pt.end(), spt.begin(), spt.end()); } @@ -372,6 +436,20 @@ Node SygusSampler::evaluate(Node n, unsigned index) return ev; } +int SygusSampler::getDiffSamplePointIndex(Node a, Node b) +{ + for (unsigned i = 0, nsamp = d_samples.size(); i < nsamp; i++) + { + Node ae = evaluate(a, i); + Node be = evaluate(b, i); + if (ae != be) + { + return i; + } + } + return -1; +} + Node SygusSampler::getRandomValue(TypeNode tn) { NodeManager* nm = NodeManager::currentNM(); @@ -562,6 +640,51 @@ void SygusSampler::registerSygusType(TypeNode tn) } } +Node SygusSamplerExt::registerTerm(Node n, bool forceKeep) +{ + Node eq_n = SygusSampler::registerTerm(n, forceKeep); + if (eq_n == n) + { + return n; + } + // one of eq_n or n must be ordered + bool eqor = isOrdered(eq_n); + bool nor = isOrdered(n); + bool isUnique = false; + if (eqor || nor) + { + isUnique = true; + // if only one is ordered, then the ordered one must contain the + // free variables of the other + if (!eqor) + { + isUnique = containsFreeVariables(n, eq_n); + } + else if (!nor) + { + isUnique = containsFreeVariables(eq_n, n); + } + } + + if (isUnique) + { + // if the previous value stored was unordered, but this is + // ordered, we prefer this one. Thus, we force its addition to the + // sampler database. + if (!eqor) + { + registerTerm(n, true); + } + return eq_n; + } + else + { + Trace("sygus-synth-rr") << "Alpha equivalent candidate rewrite : " << eq_n + << " " << n << std::endl; + } + return n; +} + } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 02b60d155..d8f2244c7 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -155,22 +155,40 @@ class SygusSampler : public LazyTrieEvaluator * forceKeep is whether we wish to force that n is chosen as a representative * value in the trie. */ - Node registerTerm(Node n, bool forceKeep = false); + virtual Node registerTerm(Node n, bool forceKeep = false); + /** get number of sample points */ + unsigned getNumSamplePoints() const { return d_samples.size(); } + /** get sample point + * + * Appends sample point #index to the vector pt, d_vars to vars. + */ + void getSamplePoint(unsigned index, + std::vector& vars, + std::vector& pt); + /** evaluate n on sample point index */ + Node evaluate(Node n, unsigned index); + /** + * Returns the index of a sample point such that the evaluation of a and b + * diverge, or -1 if no such sample point exists. + */ + int getDiffSamplePointIndex(Node a, Node b); + + protected: /** is contiguous * * This returns whether n's free variables (terms occurring in the range of * d_type_vars) are a prefix of the list of variables in d_type_vars for each - * type. For instance, if d_type_vars[Int] = { x, y }, then 0, x, x+y, y+x are - * contiguous but y is not. This is useful for excluding terms from - * consideration that are alpha-equivalent to others. + * type id. For instance, if d_type_vars[id] = { x, y } for some id, then + * 0, x, x+y, y+x are contiguous but y is not. This is useful for excluding + * terms from consideration that are alpha-equivalent to others. */ bool isContiguous(Node n); /** is ordered * * This returns whether n's free variables are in order with respect to * variables in d_type_vars for each type. For instance, if - * d_type_vars[Int] = { x, y }, then 0, x, x+y are ordered but y and y+x - * are not. + * d_type_vars[id] = { x, y } for some id, then 0, x, x+y are ordered but + * y and y+x are not. */ bool isOrdered(Node n); /** contains free variables @@ -179,16 +197,6 @@ class SygusSampler : public LazyTrieEvaluator * are those that occur in the range d_type_vars. */ bool containsFreeVariables(Node a, Node b); - /** get number of sample points */ - unsigned getNumSamplePoints() const { return d_samples.size(); } - /** get sample point - * - * Appends sample point #index to the vector pt. - */ - void getSamplePoint(unsigned index, std::vector& pt); - /** evaluate n on sample point index */ - Node evaluate(Node n, unsigned index); - private: /** sygus term database of d_qe */ TermDbSygus* d_tds; @@ -211,20 +219,33 @@ class SygusSampler : public LazyTrieEvaluator TypeNode d_tn; /** the sygus type for this sampler (if applicable). */ TypeNode d_ftn; - /** all variables */ + /** all variables we are sampling values for */ std::vector d_vars; /** type variables * - * For each type, a list of variables in the grammar we are considering, for - * that type. These typically correspond to the arguments of the + * We group variables according to "type ids". Two variables have the same + * type id if they have indistinguishable status according to this sampler. + * This is a finer-grained grouping than types. For example, two variables + * of the same type may have different type ids if they occur as constructors + * of a different set of sygus types in the grammar we are considering. + * For instance, we assign x and y different type ids in this grammar: + * A -> B + C + * B -> x | 0 | 1 + * C -> y + * Type ids are computed for each variable in d_vars during initialize(...). + * + * For each type id, a list of variables in the grammar we are considering, + * for that type. These typically correspond to the arguments of the * function-to-synthesize whose grammar we are considering. */ - std::map > d_type_vars; + std::map > d_type_vars; /** * A map all variables in the grammar we are considering to their index in * d_type_vars. */ std::map d_var_index; + /** Map from variables to the id (the domain of d_type_vars). */ + std::map d_type_ids; /** constants * * For each type, a list of constants in the grammar we are considering, for @@ -300,6 +321,23 @@ class SygusSampler : public LazyTrieEvaluator void registerSygusType(TypeNode tn); }; +/** Version of the above class with some additional features */ +class SygusSamplerExt : public SygusSampler +{ + public: + /** register term n with this sampler database + * + * This returns a term ret with the same guarantees as + * SygusSampler::registerTerm, with the additional guarantee + * that for all ret' returned by a previous call to registerTerm( n' ), + * we have that ret = n is not alpha-equivalent to ret' = n, + * modulo symmetry of equality. For example, + * (t+0), t and (s+0), s + * will not be input/output pairs of this function. + */ + virtual Node registerTerm(Node n, bool forceKeep = false) override; +}; + } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ -- 2.30.2