diff options
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) { |