From 2c4025e44771707ba548b6d8aa5a8a13ec3cd8f1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 27 Jan 2021 13:04:46 -0600 Subject: 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. --- src/preprocessing/passes/quantifier_macros.cpp | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'src/preprocessing/passes') 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(); -- cgit v1.2.3