From: Andrew Reynolds Date: Tue, 27 Feb 2018 19:58:45 +0000 (-0600) Subject: Improvements to sygus sampling (#1621) X-Git-Tag: cvc5-1.0.0~5268 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0ab8cf84132ea19e6c7a37ab0d11398b2e16e654;p=cvc5.git Improvements to sygus sampling (#1621) --- diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index e97f11db9..6552b9157 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -306,7 +306,7 @@ 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 :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 +option sygusSamples --sygus-samples=N int :read-write :default 1000 :read-write number of points to consider when doing sygus rewriter sample testing option sygusSampleGrammar --sygus-sample-grammar bool :default true when applicable, use grammar for choosing sample points diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 556b07f7f..728cd8135 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -790,60 +790,63 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d, if (options::sygusRewVerify()) { // add to the sampler database object - std::map::iterator its = - d_sampler.find(a); - if (its == d_sampler.end()) + std::map::iterator its = + d_sampler[a].find(tn); + if (its == d_sampler[a].end()) { - d_sampler[a].initializeSygus(d_tds, a, options::sygusSamples()); - its = d_sampler.find(a); + d_sampler[a][tn].initializeSygus(d_tds, nv, options::sygusSamples()); + its = d_sampler[a].find(tn); } + Node bvr_sample_ret; + std::map::iterator itsv = + d_cache[a].d_search_val_sample[tn].find(bvr); + if (itsv == d_cache[a].d_search_val_sample[tn].end()) + { + // initialize the sampler for the rewritten form of this node + bvr_sample_ret = its->second.registerTerm(bvr); + d_cache[a].d_search_val_sample[tn][bvr] = bvr_sample_ret; + } + else + { + bvr_sample_ret = itsv->second; + } + + // register the current node with the sampler Node sample_ret = its->second.registerTerm(bv); - d_cache[a].d_search_val_sample[nv] = sample_ret; - if (itsv != d_cache[a].d_search_val[tn].end()) + + // bv and bvr should be equivalent under examples + if (sample_ret != bvr_sample_ret) { - // if the analog of this term and another term were rewritten to the - // same term, then they should be equivalent under examples. - Node prev = itsv->second; - Node prev_sample_ret = d_cache[a].d_search_val_sample[prev]; - if (sample_ret != prev_sample_ret) + // we have detected unsoundness in the rewriter + Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); + std::ostream* out = nodeManagerOptions.getOut(); + (*out) << "(unsound-rewrite " << bv << " " << bvr << ")" << std::endl; + // debugging information + if (Trace.isOn("sygus-rr-debug")) { - Node prev_bv = d_tds->sygusToBuiltin(prev, tn); - // we have detected unsoundness in the rewriter - Options& nodeManagerOptions = - NodeManager::currentNM()->getOptions(); - 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, bvr); + if (pt_index >= 0) { - int pt_index = its->second.getDiffSamplePointIndex(bv, prev_bv); - if (pt_index >= 0) + Trace("sygus-rr-debug") + << "; unsound: 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") - << "; unsound: both ext-rewrite to : " << bvr << std::endl; - Trace("sygus-rr-debug") - << "; unsound: 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") << "; unsound: " << 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") << "; unsound: where they evaluate to " - << pbv_e << " and " << bv_e - << std::endl; - } - else - { - Assert(false); + Trace("sygus-rr-debug") << "; unsound: " << vars[i] << " -> " + << pt[i] << std::endl; } + Node bv_e = its->second.evaluate(bv, pt_index); + Node pbv_e = its->second.evaluate(bvr, pt_index); + Assert(bv_e != pbv_e); + Trace("sygus-rr-debug") << "; unsound: where they evaluate to " + << pbv_e << " and " << bv_e << std::endl; + } + else + { + Assert(false); } } } diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index 2c1f85deb..fa3918270 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -54,10 +54,37 @@ private: NodeSet d_active_terms; IntMap d_currTermSize; Node d_zero; -private: + + private: + /** + * Map from terms (selector chains) to their anchors. The anchor of a + * selector chain S1( ... Sn( x ) ... ) is x. + */ std::map< Node, Node > d_term_to_anchor; + /** + * Map from terms (selector chains) to the conjecture that their anchor is + * associated with. + */ std::map d_term_to_anchor_conj; + /** + * Map from terms (selector chains) to their depth. The depth of a selector + * chain S1( ... Sn( x ) ... ) is: + * weight( S1 ) + ... + weight( Sn ), + * where weight is the selector weight of Si + * (see SygusTermDatabase::getSelectorWeight). + */ std::map< Node, unsigned > d_term_to_depth; + /** + * Map from terms (selector chains) to whether they are the topmost term + * of their type. For example, if: + * S1 : T1 -> T2 + * S2 : T2 -> T2 + * S3 : T2 -> T1 + * S4 : T1 -> T3 + * Then, x, S1( x ), and S4( S3( S2( S1( x ) ) ) ) are top-level terms, + * whereas S2( S1( x ) ) and S3( S2( S1( x ) ) ) are not. + * + */ std::map< Node, bool > d_is_top_level; void registerTerm( Node n, std::vector< Node >& lemmas ); bool computeTopLevel( TypeNode tn, Node n ); @@ -80,22 +107,24 @@ private: std::map< TypeNode, std::map< Node, unsigned > > d_search_val_sz; /** search value sample * - * This is used for the sygusRewVerify() option. For each sygus term we - * register in this cache, this stores the value returned by calling - * SygusSample::registerTerm(...) on its analog. + * This is used for the sygusRewVerify() option. For each sygus term t + * of type tn with anchor a that we register with this cache, we set: + * d_search_val_sample[tn][r] = r' + * where r is the rewritten form of the builtin equivalent of t, and r' + * is the term returned by d_sampler[a][tn].registerTerm( r ). */ - std::map d_search_val_sample; + std::map> d_search_val_sample; /** For each term, whether this cache has processed that term */ std::map< Node, bool > d_search_val_proc; }; // anchor -> cache std::map< Node, SearchCache > d_cache; - /** a sygus sampler object for each anchor + /** a sygus sampler object for each (anchor, sygus type) pair * * This is used for the sygusRewVerify() option to verify the correctness of * the rewriter. */ - std::map d_sampler; + std::map> d_sampler; Node d_null; void assertTesterInternal( int tindex, TNode n, Node exp, std::vector< Node >& lemmas ); // register search term diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index aa0a4b778..fa0478ac7 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -100,6 +100,7 @@ void SygusSampler::initialize(TypeNode tn, << "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_type_ids[sv] = tnid; } initializeSamples(nsamples); } @@ -176,6 +177,7 @@ void SygusSampler::initializeSygus(TermDbSygus* tds, Node f, unsigned nsamples) << "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_type_ids[sv] = tnid; } initializeSamples(nsamples); @@ -666,6 +668,8 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep) // one of eq_n or n must be ordered bool eqor = isOrdered(eq_n); bool nor = isOrdered(n); + Trace("sygus-synth-rr-debug") + << "Ordered? : " << nor << " " << eqor << std::endl; bool isUnique = false; if (eqor || nor) {