diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-27 13:58:45 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-02-27 13:58:45 -0600 |
| commit | 0ab8cf84132ea19e6c7a37ab0d11398b2e16e654 (patch) | |
| tree | 5702972ef9a6e5d5b9ccb30a50a8339fe9e3057a /src/theory/quantifiers/sygus_sampler.cpp | |
| parent | cb8e3b305ecf83cde0380f9198fa6d3f795362cd (diff) | |
Improvements to sygus sampling (#1621)
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus_sampler.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
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) { |