diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-12 16:14:29 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-02-12 16:14:29 -0600 |
| commit | 04114df7dd58bd7391704a94fe98e2935b39130d (patch) | |
| tree | 26b403b9368c9cfeea0775ec94cc2dcb01b930ca /src/theory/quantifiers/sygus_sampler.cpp | |
| parent | c9e58c9cf4b90e42d314b92054a010513da1502a (diff) | |
Minor improvements to sygus sampler (#1598)
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus_sampler.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 757b8e44f..aa0a4b778 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -430,6 +430,7 @@ Node SygusSampler::evaluate(Node n, unsigned index) // just a substitution std::vector<Node>& pt = d_samples[index]; Node ev = n.substitute(d_vars.begin(), d_vars.end(), pt.begin(), pt.end()); + Trace("sygus-sample-ev-debug") << "Rewrite : " << ev << std::endl; ev = Rewriter::rewrite(ev); Trace("sygus-sample-ev") << "( " << n << ", " << index << " ) -> " << ev << std::endl; @@ -656,6 +657,8 @@ void SygusSamplerExt::initializeSygusExt(QuantifiersEngine* qe, Node SygusSamplerExt::registerTerm(Node n, bool forceKeep) { Node eq_n = SygusSampler::registerTerm(n, forceKeep); + Trace("sygus-synth-rr") << "sygusSampleExt : " << n << "..." << eq_n + << std::endl; if (eq_n == n) { return n; @@ -678,9 +681,11 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep) isUnique = containsFreeVariables(eq_n, n); } } + Trace("sygus-synth-rr-debug") << "AlphaEq unique: " << isUnique << std::endl; bool rewRedundant = false; if (d_drewrite != nullptr) { + Trace("sygus-synth-rr-debug") << "Add rewrite..." << std::endl; if (!d_drewrite->addRewrite(n, eq_n)) { rewRedundant = isUnique; @@ -688,6 +693,7 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep) isUnique = false; } } + Trace("sygus-synth-rr-debug") << "Rewrite unique: " << isUnique << std::endl; if (isUnique) { @@ -709,7 +715,7 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep) } Trace("sygus-synth-rr") << std::endl; } - return n; + return Node::null(); } } /* CVC4::theory::quantifiers namespace */ |