From 4fb65ae4d0018dc01fe79df8bbf7f3ec0ff583b9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 14 Apr 2020 21:28:57 -0500 Subject: [PATCH] Fix combinations of cegqi and non-standard triggers (#4271) Counterexample-guided instantiation may produce quantified formulas with INST_CONSTANT nodes, which are also used as patterns for non-standard triggers for E-matching. This fixes a few combinations that were problematic. Fixes #4250, fixes #4254, fixes #4269 and fixes #4281. --- .../ematching/inst_match_generator.cpp | 13 ++++++++++-- .../ematching/inst_match_generator.h | 2 +- src/theory/quantifiers/ematching/trigger.cpp | 21 +++++++++++++++++-- src/theory/quantifiers/inst_match.cpp | 14 +++++++++---- src/theory/quantifiers/inst_match.h | 6 +++--- 5 files changed, 44 insertions(+), 12 deletions(-) diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 6fdd6d67a..964d2e492 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -596,7 +596,15 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n) Node x; if (options::purifyTriggers()) { - x = Trigger::getInversionVariable(n); + Node xi = Trigger::getInversionVariable(n); + if (!xi.isNull()) + { + Node qa = quantifiers::TermUtil::getInstConstAttr(xi); + if (qa == q) + { + x = xi; + } + } } if (!x.isNull()) { @@ -624,7 +632,8 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q, int ret_val = -1; if( !d_eq_class.isNull() ){ Trace("var-trigger-matching") << "Matching " << d_eq_class << " against " << d_var << " in " << d_subs << std::endl; - Node s = d_subs.substitute( d_var, d_eq_class ); + TNode tvar = d_var; + Node s = d_subs.substitute(tvar, d_eq_class); s = Rewriter::rewrite( s ); Trace("var-trigger-matching") << "...got " << s << ", " << s.getKind() << std::endl; d_eq_class = Node::null(); diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 3995c67b4..b71ff3c21 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -438,7 +438,7 @@ public: private: /** variable we are matching (x in the example x+1). */ - TNode d_var; + Node d_var; /** cache of d_var.getType() */ TypeNode d_var_type; /** The substitution for what we match (x-1 in the example x+1). */ diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index e177e24a6..b2284d78e 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -298,20 +298,37 @@ Node Trigger::getIsUsableEq( Node q, Node n ) { bool Trigger::isUsableEqTerms( Node q, Node n1, Node n2 ) { if( n1.getKind()==INST_CONSTANT ){ if( options::relationalTriggers() ){ - if( !quantifiers::TermUtil::hasInstConstAttr(n2) ){ + Node q1 = quantifiers::TermUtil::getInstConstAttr(n1); + if (q1 != q) + { + // x is a variable from another quantified formula, fail + return false; + } + Node q2 = quantifiers::TermUtil::getInstConstAttr(n2); + if (q2.isNull()) + { + // x = c return true; - }else if( n2.getKind()==INST_CONSTANT ){ + } + if (n2.getKind() == INST_CONSTANT && q2 == q) + { + // x = y return true; } + // we dont check x = f(y), which is handled symmetrically below + // when n1 and n2 are swapped } }else if( isUsableAtomicTrigger( n1, q ) ){ if (options::relationalTriggers() && n2.getKind() == INST_CONSTANT + && quantifiers::TermUtil::getInstConstAttr(n2) == q && !expr::hasSubterm(n1, n2)) { + // f(x) = y return true; } else if (!quantifiers::TermUtil::hasInstConstAttr(n2)) { + // f(x) = c return true; } } diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index bd947d70b..af425c570 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -100,14 +100,20 @@ void InstMatch::clear() { } } -Node InstMatch::get(int i) const { return d_vals[i]; } +Node InstMatch::get(size_t i) const +{ + Assert(i < d_vals.size()); + return d_vals[i]; +} -void InstMatch::setValue( int i, TNode n ) { +void InstMatch::setValue(size_t i, TNode n) +{ + Assert(i < d_vals.size()); d_vals[i] = n; } -bool InstMatch::set(EqualityQuery* q, int i, TNode n) +bool InstMatch::set(EqualityQuery* q, size_t i, TNode n) { - Assert(i >= 0); + Assert(i < d_vals.size()); if( !d_vals[i].isNull() ){ if (q->areEqual(d_vals[i], n)) { diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index d298c43a8..324b2c736 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -79,15 +79,15 @@ public: out << " )"; } /** get the i^th term in the instantiation */ - Node get(int i) const; + Node get(size_t i) const; /** set/overwrites the i^th field in the instantiation with n */ - void setValue( int i, TNode n ); + void setValue(size_t i, TNode n); /** set the i^th term in the instantiation to n * * This method returns true if the i^th field was previously uninitialized, * or is equivalent to n modulo the equalities given by q. */ - bool set(EqualityQuery* q, int i, TNode n); + bool set(EqualityQuery* q, size_t i, TNode n); }; inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) { -- 2.30.2