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.

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) {