diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-25 09:28:22 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-25 09:28:22 -0500 |
commit | d7bc8b2759d7b657c52d379db62cf049861be579 (patch) | |
tree | c941abf5f1833f95c0ba45834bd2750359db7cd9 /src/theory/quantifiers | |
parent | d59314199fc72fa299ed536937a2184c54f0fc98 (diff) |
Fix issue with multi-triggers that include variable triggers (#1810)
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/ematching/inst_match_generator.cpp | 56 |
1 files changed, 28 insertions, 28 deletions
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 9c3095e59..3ceefcd90 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -142,21 +142,22 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< for (unsigned i = 0, size = d_match_pattern.getNumChildren(); i < size; i++) { - Node qa = quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i]); + Node pat = d_match_pattern[i]; + Node qa = quantifiers::TermUtil::getInstConstAttr(pat); if (!qa.isNull()) { - InstMatchGenerator* cimg = - getInstMatchGenerator(q, d_match_pattern[i]); - if (cimg) + if (pat.getKind() == INST_CONSTANT && qa == q) { - d_children.push_back(cimg); - d_children_index.push_back(i); - d_children_types.push_back(-2); - }else{ - if (d_match_pattern[i].getKind() == INST_CONSTANT && qa == q) + d_children_types.push_back(pat.getAttribute(InstVarNumAttribute())); + } + else + { + InstMatchGenerator* cimg = getInstMatchGenerator(q, pat); + if (cimg) { - d_children_types.push_back( - d_match_pattern[i].getAttribute(InstVarNumAttribute())); + d_children.push_back(cimg); + d_children_index.push_back(i); + d_children_types.push_back(-2); } else { @@ -535,24 +536,23 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, std::vecto InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n) { - if (n.getKind() == INST_CONSTANT) + if (n.getKind() != INST_CONSTANT) { - return NULL; - } - Trace("var-trigger-debug") << "Is " << n << " a variable trigger?" - << std::endl; - Node x; - if (options::purifyTriggers()) - { - x = Trigger::getInversionVariable(n); - } - if (!x.isNull()) - { - Node s = Trigger::getInversion(n, x); - VarMatchGeneratorTermSubs* vmg = new VarMatchGeneratorTermSubs(x, s); - Trace("var-trigger") << "Term substitution trigger : " << n - << ", var = " << x << ", subs = " << s << std::endl; - return vmg; + Trace("var-trigger-debug") + << "Is " << n << " a variable trigger?" << std::endl; + Node x; + if (options::purifyTriggers()) + { + x = Trigger::getInversionVariable(n); + } + if (!x.isNull()) + { + Node s = Trigger::getInversion(n, x); + VarMatchGeneratorTermSubs* vmg = new VarMatchGeneratorTermSubs(x, s); + Trace("var-trigger") << "Term substitution trigger : " << n + << ", var = " << x << ", subs = " << s << std::endl; + return vmg; + } } return new InstMatchGenerator(n); } |