From: Andrew Reynolds Date: Mon, 20 Aug 2018 21:29:30 +0000 (-0500) Subject: Minor improvements to the interface for sygus sampler (#2326) X-Git-Tag: cvc5-1.0.0~4757 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=34a4f78458773e9816d90c84fd2047b74a699527;p=cvc5.git Minor improvements to the interface for sygus sampler (#2326) --- diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index aea449fd1..7b01d6cb9 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -887,33 +887,30 @@ Node SygusSymBreakNew::registerSearchValue( std::ostream* out = nodeManagerOptions.getOut(); (*out) << "(unsound-rewrite " << bv << " " << bvr << ")" << 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, bvr); - if (pt_index >= 0) + (*out) << "; unsound: are not equivalent for : " << std::endl; + std::vector vars; + its->second.getVariables(vars); + std::vector pt; + its->second.getSamplePoint(pt_index, pt); + Assert(vars.size() == pt.size()); + for (unsigned i = 0, size = pt.size(); i < size; i++) { - 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: " << 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 " - << bv_e << " and " << pbv_e << std::endl; - } - else - { - // no witness point found? - Assert(false); + (*out) << "; 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); + (*out) << "; unsound: where they evaluate to " << bv_e << " and " + << pbv_e << std::endl; + } + else + { + // no witness point found? + Assert(false); } if (options::sygusRewVerifyAbort()) { diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 37ee01370..7319ba73e 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -526,9 +526,8 @@ bool Cegis::sampleAddRefinementLemma(const std::vector& candidates, 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, vars, pt); + d_cegis_sampler.getSamplePoint(i, 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/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 6808f2a6e..e30fda8f9 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -32,7 +32,7 @@ SygusSampler::SygusSampler() } void SygusSampler::initialize(TypeNode tn, - std::vector& vars, + const std::vector& vars, unsigned nsamples, bool unique_type_ids) { @@ -433,11 +433,9 @@ void SygusSampler::getVariables(std::vector& vars) const } 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()); } diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index f90c6ebd0..64706264a 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -77,7 +77,7 @@ class SygusSampler : public LazyTrieEvaluator * type that is used to determine when a rewrite rule is redundant. */ virtual void initialize(TypeNode tn, - std::vector& vars, + const std::vector& vars, unsigned nsamples, bool unique_type_ids = false); /** initialize sygus @@ -110,12 +110,16 @@ class SygusSampler : public LazyTrieEvaluator * Appends sample point #index to the vector pt, d_vars to vars. */ void getSamplePoint(unsigned index, - std::vector& vars, std::vector& pt); /** Add pt to the set of sample points considered by this sampler */ void addSamplePoint(std::vector& pt); /** evaluate n on sample point index */ Node evaluate(Node n, unsigned index) override; + /** + * Compute the variables from the domain of d_var_index that occur in n, + * store these in the vector fvs. + */ + void computeFreeVariables(Node n, std::vector& fvs); /** * Returns the index of a sample point such that the evaluation of a and b * diverge, or -1 if no such sample point exists. @@ -220,11 +224,6 @@ class SygusSampler : public LazyTrieEvaluator * of an argument to function f. */ bool d_is_valid; - /** - * Compute the variables from the domain of d_var_index that occur in n, - * store these in the vector fvs. - */ - void computeFreeVariables(Node n, std::vector& fvs); /** initialize samples * * Adds nsamples sample points to d_samples.