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/dynamic_rewrite.cpp | |
| parent | c9e58c9cf4b90e42d314b92054a010513da1502a (diff) | |
Minor improvements to sygus sampler (#1598)
Diffstat (limited to 'src/theory/quantifiers/dynamic_rewrite.cpp')
| -rw-r--r-- | src/theory/quantifiers/dynamic_rewrite.cpp | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp index a19695770..3462a4d10 100644 --- a/src/theory/quantifiers/dynamic_rewrite.cpp +++ b/src/theory/quantifiers/dynamic_rewrite.cpp @@ -25,7 +25,8 @@ namespace quantifiers { DynamicRewriter::DynamicRewriter(const std::string& name, QuantifiersEngine* qe) : d_qe(qe), - d_equalityEngine(qe->getUserContext(), "DynamicRewriter::" + name, true) + d_equalityEngine(qe->getUserContext(), "DynamicRewriter::" + name, true), + d_rewrites(qe->getUserContext()) { d_equalityEngine.addFunctionKind(kind::APPLY_UF); } @@ -42,20 +43,26 @@ bool DynamicRewriter::addRewrite(Node a, Node b) // add to the equality engine Node ai = toInternal(a); Node bi = toInternal(b); + Trace("dyn-rewrite-debug") << "Internal : " << ai << " " << bi << std::endl; d_equalityEngine.addTerm(ai); d_equalityEngine.addTerm(bi); + Trace("dyn-rewrite-debug") << "get reps..." << std::endl; // may already be equal by congruence Node air = d_equalityEngine.getRepresentative(ai); Node bir = d_equalityEngine.getRepresentative(bi); + Trace("dyn-rewrite-debug") << "Reps : " << air << " " << bir << std::endl; if (air == bir) { Trace("dyn-rewrite") << "...fail, congruent." << std::endl; return false; } + Trace("dyn-rewrite-debug") << "assert eq..." << std::endl; Node eq = ai.eqNode(bi); + d_rewrites.push_back(eq); d_equalityEngine.assertEquality(eq, true, eq); + Trace("dyn-rewrite-debug") << "Finished" << std::endl; return true; } |