Split pattern term selector from trigger (#5811)

This separates the utilities for selecting pattern terms from the Trigger class itself. This includes a PatternTermSelector, which implements the techniques for selecting the pool of pattern terms, and TriggerTermInfo which contains basic information about pattern terms.

It makes minor refactoring to make the PatternTermSelector class more than just static methods, e.g. it is now a configurable object that selects pattern terms. This makes some of the methods take fewer arguments.

More refactoring is possible, to be addressed on future PRs.

1 files changed, 6 insertions, 5 deletions

diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index 028bfede5..35eeac125 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -22,7 +22,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/arith/arith_msum.h"
-#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/quantifiers/ematching/pattern_term_selector.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
@@ -191,17 +191,18 @@ bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){
   return pol && n.getKind()==EQUAL;
 }
 
-bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) {
+bool QuantifierMacros::isGroundUfTerm(Node q, Node n)
+{
   Node icn = d_preprocContext->getTheoryEngine()
                  ->getQuantifiersEngine()
                  ->getTermUtil()
-                 ->substituteBoundVariablesToInstConstants(n, f);
+                 ->substituteBoundVariablesToInstConstants(n, q);
   Trace("macros-debug2") << "Get free variables in " << icn << std::endl;
   std::vector< Node > var;
-  quantifiers::TermUtil::computeInstConstContainsForQuant(f, icn, var);
+  quantifiers::TermUtil::computeInstConstContainsForQuant(q, icn, var);
   Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl;
   std::vector< Node > trigger_var;
-  inst::Trigger::getTriggerVariables( icn, f, trigger_var );
+  inst::PatternTermSelector::getTriggerVariables(icn, q, trigger_var);
   Trace("macros-debug2") << "Done." << std::endl;
   //only if all variables are also trigger variables
   return trigger_var.size()>=var.size();