summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/quantifiers_options2
-rw-r--r--src/theory/datatypes/datatypes_sygus.cpp95
-rw-r--r--src/theory/datatypes/datatypes_sygus.h43
-rw-r--r--src/theory/quantifiers/sygus_sampler.cpp4
4 files changed, 90 insertions, 54 deletions
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<Node, quantifiers::SygusSampler>::iterator its =
- d_sampler.find(a);
- if (its == d_sampler.end())
+ std::map<TypeNode, quantifiers::SygusSampler>::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<Node, Node>::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<Node> vars;
+ std::vector<Node> 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<Node> vars;
- std::vector<Node> 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<Node, quantifiers::CegConjecture*> 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<Node, Node> d_search_val_sample;
+ std::map<TypeNode, std::map<Node, Node>> 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<Node, quantifiers::SygusSampler> d_sampler;
+ std::map<Node, std::map<TypeNode, quantifiers::SygusSampler>> 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)
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback