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.

1 files changed, 19 insertions, 2 deletions

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;
     }
   }