1 files changed, 15 insertions, 1 deletions
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);