Fixes for relational triggers (#2967)

9 files changed, 106 insertions, 65 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 0a69178b3..66bd265d8 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -247,7 +247,7 @@ header = "options/quantifiers_options.h"
   category   = "regular"
   long       = "relational-triggers"
   type       = "bool"
-  default    = "false"
+  default    = "true"
   read_only  = true
   help       = "choose relational triggers such as x = f(y), x >= f(y)"
 
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index cb0fcaf50..3be1d4a4b 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -173,16 +173,18 @@ void CandidateGeneratorQEAll::reset( Node eqc ) {
 }
 
 Node CandidateGeneratorQEAll::getNextCandidate() {
+  quantifiers::TermDb* tdb = d_qe->getTermDatabase();
   while( !d_eq.isFinished() ){
     TNode n = (*d_eq);
     ++d_eq;
     if( n.getType().isComparableTo( d_match_pattern_type ) ){
-      TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n );
+      TNode nh = tdb->getEligibleTermInEqc(n);
       if( !nh.isNull() ){
         if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
           nh = d_qe->getInternalRepresentative( nh, d_f, d_index );
           //don't consider this if already the instantiation is ineligible
-          if( !d_qe->getTermDatabase()->isTermEligibleForInstantiation( nh, d_f, false ) ){
+          if (!tdb->isTermEligibleForInstantiation(nh, d_f))
+          {
             nh = Node::null();
           }
         }
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 0a4386db9..9e76a6a31 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -98,28 +98,53 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
   if( !d_pattern.isNull() ){
     Trace("inst-match-gen") << "Initialize, pattern term is " << d_pattern << std::endl;
     if( d_match_pattern.getKind()==NOT ){
+      Assert(d_pattern.getKind() == NOT);
       //we want to add the children of the NOT
-      d_match_pattern = d_pattern[0];
+      d_match_pattern = d_match_pattern[0];
+    }
+
+    if (d_pattern.getKind() == NOT && d_match_pattern.getKind() == EQUAL
+        && d_match_pattern[0].getKind() == INST_CONSTANT
+        && d_match_pattern[1].getKind() == INST_CONSTANT)
+    {
+      // special case: disequalities between variables x != y will match ground
+      // disequalities.
     }
-    if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){
-      //make sure the matching portion of the equality is on the LHS of d_pattern
-      //  and record what d_match_pattern is
+    else if (d_match_pattern.getKind() == EQUAL
+             || d_match_pattern.getKind() == GEQ)
+    {
+      // We are one of the following cases:
+      //   f(x)~a, f(x)~y, x~a, x~y
+      // If we are the first or third case, we ensure that f(x)/x is on the left
+      // hand side of the relation d_pattern, d_match_pattern is f(x)/x and
+      // d_eq_class_rel (indicating the equivalence class that we are related
+      // to) is set to a.
       for( unsigned i=0; i<2; i++ ){
-        if( !quantifiers::TermUtil::hasInstConstAttr(d_match_pattern[i]) || d_match_pattern[i].getKind()==INST_CONSTANT ){
-          Node mp = d_match_pattern[1-i];
-          Node mpo = d_match_pattern[i];
-          if( mp.getKind()!=INST_CONSTANT ){
-            if( i==0 ){
-              if( d_match_pattern.getKind()==GEQ ){
-                d_pattern = NodeManager::currentNM()->mkNode( kind::GT, mp, mpo );
-                d_pattern = d_pattern.negate();
-              }else{
-                d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), mp, mpo );
-              }
+        Node mp = d_match_pattern[i];
+        Node mpo = d_match_pattern[1 - i];
+        // If this side has free variables, and the other side does not or
+        // it is a free variable, then we will match on this side of the
+        // relation.
+        if (quantifiers::TermUtil::hasInstConstAttr(mp)
+            && (!quantifiers::TermUtil::hasInstConstAttr(mpo)
+                || mpo.getKind() == INST_CONSTANT))
+        {
+          if (i == 1)
+          {
+            if (d_match_pattern.getKind() == GEQ)
+            {
+              d_pattern = NodeManager::currentNM()->mkNode(kind::GT, mp, mpo);
+              d_pattern = d_pattern.negate();
+            }
+            else
+            {
+              d_pattern = NodeManager::currentNM()->mkNode(
+                  d_match_pattern.getKind(), mp, mpo);
             }
-            d_eq_class_rel = mpo;
-            d_match_pattern = mp;
           }
+          d_eq_class_rel = mpo;
+          d_match_pattern = mp;
+          // we won't find a term in the other direction
           break;
         }
       }
@@ -178,9 +203,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
       {
         // 1-constructors have a trivial way of generating candidates in a
         // given equivalence class
-        const Datatype& dt =
-            static_cast<DatatypeType>(d_match_pattern.getType().toType())
-                .getDatatype();
+        const Datatype& dt = d_match_pattern.getType().getDatatype();
         if (dt.getNumConstructors() == 1)
         {
           d_cg = new inst::CandidateGeneratorConsExpand(qe, d_match_pattern);
@@ -188,14 +211,18 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
       }
       if (d_cg == nullptr)
       {
-        // we will be scanning lists trying to find
-        // d_match_pattern.getOperator()
-        d_cg = new inst::CandidateGeneratorQE(qe, d_match_pattern);
-      }
-      //if matching on disequality, inform the candidate generator not to match on eqc
-      if( d_pattern.getKind()==NOT && d_pattern[0].getKind()==EQUAL ){
-        ((inst::CandidateGeneratorQE*)d_cg)->excludeEqc( d_eq_class_rel );
-        d_eq_class_rel = Node::null();
+        CandidateGeneratorQE* cg =
+            new CandidateGeneratorQE(qe, d_match_pattern);
+        // we will be scanning lists trying to find ground terms whose operator
+        // is the same as d_match_operator's.
+        d_cg = cg;
+        // if matching on disequality, inform the candidate generator not to
+        // match on eqc
+        if (d_pattern.getKind() == NOT && d_pattern[0].getKind() == EQUAL)
+        {
+          cg->excludeEqc(d_eq_class_rel);
+          d_eq_class_rel = Node::null();
+        }
       }
     }else if( d_match_pattern.getKind()==INST_CONSTANT ){
       if( d_pattern.getKind()==APPLY_SELECTOR_TOTAL ){
@@ -209,12 +236,15 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
       }else{
         d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern );
       }
-    }else if( d_match_pattern.getKind()==EQUAL &&
-              d_match_pattern[0].getKind()==INST_CONSTANT && d_match_pattern[1].getKind()==INST_CONSTANT ){
+    }
+    else if (d_match_pattern.getKind() == EQUAL)
+    {
       //we will be producing candidates via literal matching heuristics
-      Assert(d_pattern.getKind() == NOT);
-      // candidates will be all disequalities
-      d_cg = new inst::CandidateGeneratorQELitDeq(qe, d_match_pattern);
+      if (d_pattern.getKind() == NOT)
+      {
+        // candidates will be all disequalities
+        d_cg = new inst::CandidateGeneratorQELitDeq(qe, d_match_pattern);
+      }
     }else{
       Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
     }
@@ -288,8 +318,10 @@ int InstMatchGenerator::getMatch(
           prev.push_back(d_children_types[0]);
         }
       }
+    }
     //for relational matching
-    }else if( !d_eq_class_rel.isNull() && d_eq_class_rel.getKind()==INST_CONSTANT ){
+    if (!d_eq_class_rel.isNull() && d_eq_class_rel.getKind() == INST_CONSTANT)
+    {
       int v = d_eq_class_rel.getAttribute(InstVarNumAttribute());
       //also must fit match to equivalence class
       bool pol = d_pattern.getKind()!=NOT;
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 8f671fb55..ce328df2e 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -325,7 +325,10 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         }
       }
       int curr_w = Trigger::getTriggerWeight( patTermsF[i] );
-      if( ntrivTriggers && !newVar && last_weight!=-1 && curr_w>last_weight ){
+      // triggers whose value is maximum (2) are considered expendable.
+      if (ntrivTriggers && !newVar && last_weight != -1 && curr_w > last_weight
+          && curr_w >= 2)
+      {
         Trace("auto-gen-trigger-debug") << "...exclude expendible non-trivial trigger : " << patTermsF[i] << std::endl;
         rmPatTermsF[patTermsF[i]] = true;
       }else{
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 31bd1aa96..201aad3a0 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -232,8 +232,8 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
                          << std::endl;
   std::map<Node, std::vector<Node> > ho_apps;
   HigherOrderTrigger::collectHoVarApplyTerms(f, trNodes, ho_apps);
-  Trace("trigger") << "...got " << ho_apps.size()
-                   << " higher-order applications." << std::endl;
+  Trace("trigger-debug") << "...got " << ho_apps.size()
+                         << " higher-order applications." << std::endl;
   Trigger* t;
   if (!ho_apps.empty())
   {
@@ -488,10 +488,15 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod
           // if child was not already removed
           if( tinfo.find( added2[i] )!=tinfo.end() ){
             if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){
-              //discard all subterms
-              Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl;
-              visited[ added2[i] ].clear();
-              tinfo.erase( added2[i] );
+              // discard all subterms
+              // do not remove if it has smaller weight
+              if (tinfo[nu].d_weight <= tinfo[added2[i]].d_weight)
+              {
+                Trace("auto-gen-trigger-debug2")
+                    << "......remove it." << std::endl;
+                visited[added2[i]].clear();
+                tinfo.erase(added2[i]);
+              }
             }else{
               if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){
                 if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight)
@@ -548,21 +553,11 @@ int Trigger::getTriggerWeight( Node n ) {
   {
     return 0;
   }
-  else if (isAtomicTrigger(n))
+  if (isAtomicTrigger(n))
   {
     return 1;
-  }else{
-    if( options::relationalTriggers() ){
-      if( isRelationalTrigger( n ) ){
-        for( unsigned i=0; i<2; i++ ){
-          if( n[i].getKind()==INST_CONSTANT && !quantifiers::TermUtil::hasInstConstAttr( n[1-i] ) ){
-            return 0;
-          }
-        }
-      }
-    }
-    return 2;
   }
+  return 2;
 }
 
 bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ) {
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index f276585d6..d47ea72ee 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -319,9 +319,12 @@ class Trigger {
   static bool isPureTheoryTrigger( Node n );
   /** get trigger weight
    *
-   * Returns 0 for triggers that are easy to process and 1 otherwise.
-   * A trigger is easy to process if it is an atomic trigger, or a relational
-   * trigger of the form x ~ g for ~ \in { =, >=, > }.
+   * Intutively, this function classifies how difficult it is to handle the
+   * trigger term n, where the smaller the value, the easier.
+   *
+   * Returns 0 for triggers that are APPLY_UF terms.
+   * Returns 1 for other triggers whose kind is atomic.
+   * Returns 2 otherwise.
    */
   static int getTriggerWeight( Node n );
   /** Returns whether n is a trigger term with a local theory extension
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 623db032a..8bd39c241 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -221,7 +221,7 @@ bool Instantiate::addInstantiation(
   {
     for (Node& t : terms)
     {
-      if (!d_term_db->isTermEligibleForInstantiation(t, q, true))
+      if (!d_term_db->isTermEligibleForInstantiation(t, q))
       {
         return false;
       }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index abb84ccd7..c4b10eb6f 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -907,7 +907,8 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) {
   }
 }
 
-bool TermDb::isTermEligibleForInstantiation( TNode n, TNode f, bool print ) {
+bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f)
+{
   if( options::lteRestrictInstClosure() ){
     //has to be both in inst closure and in ground assertions
     if( !isInstClosure( n ) ){
@@ -937,7 +938,9 @@ bool TermDb::isTermEligibleForInstantiation( TNode n, TNode f, bool print ) {
       }
     }
   }
-  return true;
+  // it cannot have instantiation constants, which originate from
+  // counterexample-guided instantiation strategies.
+  return !TermUtil::hasInstConstAttr(n);
 }
 
 Node TermDb::getEligibleTermInEqc( TNode r ) {
@@ -949,11 +952,14 @@ Node TermDb::getEligibleTermInEqc( TNode r ) {
       Node h;
       eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
       eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
-      while( h.isNull() && !eqc_i.isFinished() ){
+      while (!eqc_i.isFinished())
+      {
         TNode n = (*eqc_i);
         ++eqc_i;
-        if( hasTermCurrent( n ) ){
+        if (isTermEligibleForInstantiation(n, TNode::null()))
+        {
           h = n;
+          break;
         }
       }
       d_term_elig_eqc[r] = h;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 148a18958..cd5c27f0d 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -277,7 +277,7 @@ class TermDb : public QuantifiersUtil {
   */
   bool hasTermCurrent(Node n, bool useMode = true);
   /** is term eligble for instantiation? */
-  bool isTermEligibleForInstantiation(TNode n, TNode f, bool print = false);
+  bool isTermEligibleForInstantiation(TNode n, TNode f);
   /** get eligible term in equivalence class of r */
   Node getEligibleTermInEqc(TNode r);
   /** is r a inst closure node?