diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-10 16:44:02 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-10 16:44:02 -0500 |
commit | f1d4d477d7cbfb6c8ba79232986a4135c5647e4a (patch) | |
tree | 9ec138c6b901172e809fd5fb89e67e4a92ad2239 /src/theory/quantifiers/dynamic_rewrite.cpp | |
parent | 817fe6d90c25dbdfe62c658add02efd51e2e29eb (diff) |
Improve accuracy of stats for sygus sampler (#1755)
Diffstat (limited to 'src/theory/quantifiers/dynamic_rewrite.cpp')
-rw-r--r-- | src/theory/quantifiers/dynamic_rewrite.cpp | 21 |
1 files changed, 4 insertions, 17 deletions
diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp index cb7379910..00e527aba 100644 --- a/src/theory/quantifiers/dynamic_rewrite.cpp +++ b/src/theory/quantifiers/dynamic_rewrite.cpp @@ -31,39 +31,26 @@ DynamicRewriter::DynamicRewriter(const std::string& name, QuantifiersEngine* qe) d_equalityEngine.addFunctionKind(kind::APPLY_UF); } -bool DynamicRewriter::addRewrite(Node a, Node b) +void DynamicRewriter::addRewrite(Node a, Node b) { Trace("dyn-rewrite") << "Dyn-Rewriter : " << a << " == " << b << std::endl; if (a == b) { - Trace("dyn-rewrite") << "...fail, equal." << std::endl; - return false; + Trace("dyn-rewrite") << "...equal." << std::endl; + return; } // 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); + Assert(d_equalityEngine.consistent()); Trace("dyn-rewrite-debug") << "Finished" << std::endl; - return true; } bool DynamicRewriter::areEqual(Node a, Node b) |