Reimplement support for relational triggers (#7063)

This makes relational triggers its own kind of instantiation match generator. Future PRs will delete the code interleaved in the core InstMatchGenerator class for handling relational triggers.

This PR also fixes two issues related to how trigger techniques are combined:
(1) instantiation match generators that are generated as part of multi-triggers now are properly specialized (using getInstMatchGenerator),
(2) there was a bug with auto-generated triggers: when the first auto-generated trigger was generated that was already a user trigger, then we would ignore all other auto-generated triggers.

This is work towards finding a solution for the choice.move.hard Facebook benchmark, where relational-triggers appear to be a possible solution.

10 files changed, 325 insertions, 23 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index cde739454..a2b5966e1 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -795,6 +795,8 @@ libcvc5_add_sources(
   theory/quantifiers/ematching/instantiation_engine.h
   theory/quantifiers/ematching/pattern_term_selector.cpp
   theory/quantifiers/ematching/pattern_term_selector.h
+  theory/quantifiers/ematching/relational_match_generator.cpp
+  theory/quantifiers/ematching/relational_match_generator.h
   theory/quantifiers/ematching/trigger.cpp
   theory/quantifiers/ematching/trigger.h
   theory/quantifiers/ematching/trigger_database.cpp
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index d8e3b7950..075299583 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
 #include "theory/quantifiers/ematching/inst_match_generator_simple.h"
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
+#include "theory/quantifiers/ematching/relational_match_generator.h"
 #include "theory/quantifiers/ematching/var_match_generator.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_state.h"
@@ -618,7 +619,7 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(
     InstMatchGenerator* init;
     std::map< Node, InstMatchGenerator * >::iterator iti = pat_map_init.find( pats[pCounter] );
     if( iti==pat_map_init.end() ){
-      init = new InstMatchGenerator(tparent, pats[pCounter]);
+      init = getInstMatchGenerator(tparent, q, pats[pCounter]);
     }else{
       init = iti->second;
     }
@@ -645,6 +646,7 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent,
                                                               Node q,
                                                               Node n)
 {
+  // maybe variable match generator
   if (n.getKind() != INST_CONSTANT)
   {
     Trace("var-trigger-debug")
@@ -672,6 +674,16 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent,
       return vmg;
     }
   }
+  Trace("relational-trigger")
+      << "Is " << n << " a relational trigger?" << std::endl;
+  // relational triggers
+  bool hasPol, pol;
+  Node lit;
+  if (TriggerTermInfo::isUsableRelationTrigger(n, hasPol, pol, lit))
+  {
+    Trace("relational-trigger") << "...yes, for literal " << lit << std::endl;
+    return new RelationalMatchGenerator(tparent, lit, hasPol, pol);
+  }
   return new InstMatchGenerator(tparent, n);
 }
 
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 30be83ecc..fdb0d0db3 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -339,20 +339,18 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
                           TriggerDatabase::TR_GET_OLD,
                           d_num_trigger_vars[f]);
     }
-    if (tr == nullptr)
+    // if we generated a trigger above, add it
+    if (tr != nullptr)
     {
-      // did not generate a trigger
-      continue;
-    }
-    addTrigger(tr, f);
-    if (tr->isMultiTrigger())
-    {
-      // only add a single multi-trigger
-      continue;
+      addTrigger(tr, f);
+      if (tr->isMultiTrigger())
+      {
+        // only add a single multi-trigger
+        continue;
+      }
     }
     // if we are generating additional triggers...
-    size_t index = 0;
-    if (index < patTerms.size())
+    if (patTerms.size() > 1)
     {
       // check if similar patterns exist, and if so, add them additionally
       unsigned nqfs_curr = 0;
@@ -361,7 +359,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         nqfs_curr =
             d_quant_rel->getNumQuantifiersForSymbol(patTerms[0].getOperator());
       }
-      index++;
+      size_t index = 1;
       bool success = true;
       while (success && index < patTerms.size()
              && d_is_single_trigger[patTerms[index]])
@@ -527,16 +525,22 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
     Trace("auto-gen-trigger-debug")
         << "...required polarity for " << pat << " is " << rpol
         << ", eq=" << rpoleq << std::endl;
+    // Currently, we have ad-hoc treatment for relational triggers that
+    // are not handled by RelationalMatchGen.
+    bool isAdHocRelationalTrigger =
+        TriggerTermInfo::isRelationalTrigger(pat)
+        && !TriggerTermInfo::isUsableRelationTrigger(pat);
     if (rpol != 0)
     {
       Assert(rpol == 1 || rpol == -1);
-      if (TriggerTermInfo::isRelationalTrigger(pat))
+      if (isAdHocRelationalTrigger)
       {
         pat = rpol == -1 ? pat.negate() : pat;
       }
       else
       {
-        Assert(TriggerTermInfo::isAtomicTrigger(pat));
+        Assert(TriggerTermInfo::isAtomicTrigger(pat)
+               || TriggerTermInfo::isUsableRelationTrigger(pat));
         if (pat.getType().isBoolean() && rpoleq.isNull())
         {
           if (options().quantifiers.literalMatchMode
@@ -575,13 +579,10 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
       }
       Trace("auto-gen-trigger-debug") << "...got : " << pat << std::endl;
     }
-    else
+    else if (isAdHocRelationalTrigger)
     {
-      if (TriggerTermInfo::isRelationalTrigger(pat))
-      {
-        // consider both polarities
-        addPatternToPool(f, pat.negate(), num_fv, mpat);
-      }
+      // consider both polarities
+      addPatternToPool(f, pat.negate(), num_fv, mpat);
     }
     addPatternToPool(f, pat, num_fv, mpat);
   }
diff --git a/src/theory/quantifiers/ematching/relational_match_generator.cpp b/src/theory/quantifiers/ematching/relational_match_generator.cpp
new file mode 100644
index 000000000..8981a7a2d
--- /dev/null
+++ b/src/theory/quantifiers/ematching/relational_match_generator.cpp
@@ -0,0 +1,125 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Relational match generator class.
+ */
+
+#include "theory/quantifiers/ematching/relational_match_generator.h"
+
+#include "theory/quantifiers/term_util.h"
+#include "util/rational.h"
+
+using namespace cvc5::kind;
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+namespace inst {
+
+RelationalMatchGenerator::RelationalMatchGenerator(Trigger* tparent,
+                                                   Node rtrigger,
+                                                   bool hasPol,
+                                                   bool pol)
+    : InstMatchGenerator(tparent, Node::null()),
+      d_vindex(-1),
+      d_hasPol(hasPol),
+      d_pol(pol),
+      d_counter(0)
+{
+  Assert((rtrigger.getKind() == EQUAL && rtrigger[0].getType().isReal())
+         || rtrigger.getKind() == GEQ);
+  Trace("relational-match-gen")
+      << "Relational trigger: " << rtrigger << ", hasPol/pol = " << hasPol
+      << "/" << pol << std::endl;
+  for (size_t i = 0; i < 2; i++)
+  {
+    if (rtrigger[i].getKind() == INST_CONSTANT)
+    {
+      d_var = rtrigger[i];
+      d_vindex = d_var.getAttribute(InstVarNumAttribute());
+      d_rhs = rtrigger[1 - i];
+      Assert(!quantifiers::TermUtil::hasInstConstAttr(d_rhs));
+      Kind k = rtrigger.getKind();
+      d_rel = (i == 0 ? k : (k == GEQ ? LEQ : k));
+      break;
+    }
+  }
+  Trace("relational-match-gen") << "...processed " << d_var << " (" << d_vindex
+                                << ") " << d_rel << " " << d_rhs << std::endl;
+  AlwaysAssert(!d_var.isNull())
+      << "Failed to initialize RelationalMatchGenerator";
+}
+
+bool RelationalMatchGenerator::reset(Node eqc)
+{
+  d_counter = 0;
+  return true;
+}
+
+int RelationalMatchGenerator::getNextMatch(Node q, InstMatch& m)
+{
+  Trace("relational-match-gen") << "getNextMatch, rel match gen" << std::endl;
+  // try (up to) two different terms
+  Node s;
+  Node rhs = d_rhs;
+  bool rmPrev = m.get(d_vindex).isNull();
+  while (d_counter < 2)
+  {
+    bool checkPol = false;
+    if (d_counter == 0)
+    {
+      checkPol = d_pol;
+    }
+    else
+    {
+      Assert(d_counter == 1);
+      if (d_hasPol)
+      {
+        break;
+      }
+      // try the opposite polarity
+      checkPol = !d_pol;
+    }
+    NodeManager* nm = NodeManager::currentNM();
+    // falsify ( d_var <d_rel> d_rhs ) = checkPol
+    s = rhs;
+    if (!checkPol)
+    {
+      s = nm->mkNode(PLUS, s, nm->mkConst(Rational(d_rel == GEQ ? -1 : 1)));
+    }
+    d_counter++;
+    Trace("relational-match-gen")
+        << "...try set " << s << " for " << checkPol << std::endl;
+    if (m.set(d_qstate, d_vindex, s))
+    {
+      Trace("relational-match-gen") << "...success" << std::endl;
+      int ret = continueNextMatch(q, m, InferenceId::UNKNOWN);
+      if (ret > 0)
+      {
+        Trace("relational-match-gen") << "...returned " << ret << std::endl;
+        return ret;
+      }
+      Trace("relational-match-gen") << "...failed to gen inst" << std::endl;
+      // failed
+      if (rmPrev)
+      {
+        m.d_vals[d_vindex] = Node::null();
+      }
+    }
+  }
+  return -1;
+}
+
+}  // namespace inst
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/relational_match_generator.h b/src/theory/quantifiers/ematching/relational_match_generator.h
new file mode 100644
index 000000000..eead2876a
--- /dev/null
+++ b/src/theory/quantifiers/ematching/relational_match_generator.h
@@ -0,0 +1,92 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Relational match generator class.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__QUANTIFIERS__RELATIONAL_MATCH_GENERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__RELATIONAL_MATCH_GENERATOR_H
+
+#include "expr/node.h"
+#include "theory/quantifiers/ematching/inst_match_generator.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+namespace inst {
+
+/**
+ * Match generator for relational triggers x ~ t where t is a ground term.
+ * This match generator tries a small fixed set of terms based on the kind of
+ * relation and the required polarity of the trigger in the quantified formula.
+ *
+ * For example, for quantified formula (forall ((x Int)) (=> (> x n) (P x))),
+ * we have that (> x n) is a relational trigger with required polarity "true".
+ * This generator will try the match `x -> n+1` only, where notice that n+1 is
+ * the canonical term chosen to satisfy x>n. Canonical terms for arithmetic
+ * relations (~ x n) are in set { n, n+1, n-1 }.
+ *
+ * If a relational trigger does not have a required polarity, then up to 2
+ * terms are tried, a term that satisfies the relation, and one that does not.
+ * If (>= x n) is a relational trigger with no polarity, then `x -> n` and
+ * `x -> n-1` will be generated.
+ *
+ * Currently this class handles only equality between real or integer valued
+ * terms, or inequalities (kind GEQ). It furthermore only considers ground terms
+ * t for the right hand side of relations.
+ */
+class RelationalMatchGenerator : public InstMatchGenerator
+{
+ public:
+  /**
+   * @param tparent The parent trigger that this match generator belongs to
+   * @param rtrigger The relational trigger
+   * @param hasPol Whether the trigger has an entailed polarity
+   * @param pol The entailed polarity of the relational trigger.
+   */
+  RelationalMatchGenerator(Trigger* tparent,
+                           Node rtrigger,
+                           bool hasPol,
+                           bool pol);
+
+  /** Reset */
+  bool reset(Node eqc) override;
+  /** Get the next match. */
+  int getNextMatch(Node q, InstMatch& m) override;
+
+ private:
+  /** the variable */
+  Node d_var;
+  /** The index of the variable */
+  int64_t d_vindex;
+  /** the relation kind */
+  Kind d_rel;
+  /** the right hand side */
+  Node d_rhs;
+  /** whether we have a required polarity */
+  bool d_hasPol;
+  /** the required polarity, if it exists */
+  bool d_pol;
+  /**
+   * The current number of terms we have generated since the last call to reset
+   */
+  size_t d_counter;
+};
+
+}  // namespace inst
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
+
+#endif
diff --git a/src/theory/quantifiers/ematching/trigger_term_info.cpp b/src/theory/quantifiers/ematching/trigger_term_info.cpp
index 600797f4e..f31ec088a 100644
--- a/src/theory/quantifiers/ematching/trigger_term_info.cpp
+++ b/src/theory/quantifiers/ematching/trigger_term_info.cpp
@@ -70,6 +70,46 @@ bool TriggerTermInfo::isRelationalTriggerKind(Kind k)
   return k == EQUAL || k == GEQ;
 }
 
+bool TriggerTermInfo::isUsableRelationTrigger(Node n)
+{
+  bool hasPol, pol;
+  Node lit;
+  return isUsableRelationTrigger(n, hasPol, pol, lit);
+}
+bool TriggerTermInfo::isUsableRelationTrigger(Node n,
+                                              bool& hasPol,
+                                              bool& pol,
+                                              Node& lit)
+{
+  // relational triggers (not) (= (~ x t) true|false), where ~ in { =, >= }.
+  hasPol = false;
+  pol = n.getKind() != NOT;
+  lit = pol ? n : n[0];
+  if (lit.getKind() == EQUAL && lit[1].getType().isBoolean()
+      && lit[1].isConst())
+  {
+    hasPol = true;
+    pol = lit[1].getConst<bool>() ? pol : !pol;
+    lit = lit[0];
+  }
+  // is it a relational trigger?
+  if ((lit.getKind() == EQUAL && lit[0].getType().isReal())
+      || lit.getKind() == GEQ)
+  {
+    // if one side of the relation is a variable and the other side is a ground
+    // term, we can treat this using the relational match generator
+    for (size_t i = 0; i < 2; i++)
+    {
+      if (lit[i].getKind() == INST_CONSTANT
+          && !quantifiers::TermUtil::hasInstConstAttr(lit[1 - i]))
+      {
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
 bool TriggerTermInfo::isSimpleTrigger(Node n)
 {
   Node t = n.getKind() == NOT ? n[0] : n;
@@ -105,7 +145,7 @@ int32_t TriggerTermInfo::getTriggerWeight(Node n)
   {
     return 0;
   }
-  if (isAtomicTrigger(n))
+  if (isAtomicTrigger(n) || isUsableRelationTrigger(n))
   {
     return 1;
   }
diff --git a/src/theory/quantifiers/ematching/trigger_term_info.h b/src/theory/quantifiers/ematching/trigger_term_info.h
index 753d0850c..3816d0988 100644
--- a/src/theory/quantifiers/ematching/trigger_term_info.h
+++ b/src/theory/quantifiers/ematching/trigger_term_info.h
@@ -108,6 +108,19 @@ class TriggerTermInfo
   static bool isRelationalTrigger(Node n);
   /** Is k a relational trigger kind? */
   static bool isRelationalTriggerKind(Kind k);
+  /**
+   * Is n a usable relational trigger, which is true if RelationalMatchGenerator
+   * can process n.
+   */
+  static bool isUsableRelationTrigger(Node n);
+  /**
+   * Same as above, but lit / hasPol / pol are updated to the required
+   * constructor arguments for RelationalMatchGenerator.
+   */
+  static bool isUsableRelationTrigger(Node n,
+                                      bool& hasPol,
+                                      bool& pol,
+                                      Node& lit);
   /** is n a simple trigger (see inst_match_generator.h)? */
   static bool isSimpleTrigger(Node n);
   /** get trigger weight
@@ -116,7 +129,8 @@ class TriggerTermInfo
    * 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 1 for other triggers whose kind is atomic, or are usable
+   * relational triggers.
    * Returns 2 otherwise.
    */
   static int32_t getTriggerWeight(Node n);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d24150cf6..6dafe6852 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -971,6 +971,7 @@ set(regress_0_tests
   regress0/quantifiers/simp-len.smt2
   regress0/quantifiers/simp-typ-test.smt2
   regress0/quantifiers/ufnia-fv-delta.smt2
+  regress0/quantifiers/veqt-delta.smt2
   regress0/rec-fun-const-parse-bug.smt2
   regress0/rels/addr_book_0.cvc.smt2
   regress0/rels/atom_univ2.cvc.smt2
@@ -1857,6 +1858,7 @@ set(regress_1_tests
   regress1/quantifiers/cee-npnt-dd.smt2
   regress1/quantifiers/cee-os-delta.smt2
   regress1/quantifiers/cdt-0208-to.smt2
+  regress1/quantifiers/choice-move-delta-relt.smt2
   regress1/quantifiers/const.cvc.smt2
   regress1/quantifiers/constfunc.cvc.smt2
   regress1/quantifiers/ddatv-delta2.smt2
diff --git a/test/regress/regress0/quantifiers/veqt-delta.smt2 b/test/regress/regress0/quantifiers/veqt-delta.smt2
new file mode 100644
index 000000000..dfac015c6
--- /dev/null
+++ b/test/regress/regress0/quantifiers/veqt-delta.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --relational-triggers
+; EXPECT: unsat
+(set-logic ALL)
+(declare-sort S 0)
+(declare-fun f () S)
+(assert (forall ((? S)) (= ? f)))
+(assert (exists ((? S) (v S)) (distinct ? v)))
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/choice-move-delta-relt.smt2 b/test/regress/regress1/quantifiers/choice-move-delta-relt.smt2
new file mode 100644
index 000000000..a8fd0d498
--- /dev/null
+++ b/test/regress/regress1/quantifiers/choice-move-delta-relt.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --relational-triggers --user-pat=use
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun F (Int) Bool)
+(assert (forall ((v Int)) (! (= (F 0) (< v 0)) :qid |outputbpl.194:24| :pattern ((F 0)))))
+(check-sat)