From 0f03dbb1378354adcfef635a93f8b13987c2d983 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 17 Feb 2021 13:34:54 -0600 Subject: Move methods from term util to quantifiers registry (#5916) Towards eliminating dependencies on quantifiers engine, and eliminating the TermUtil class. Note that QuantifiersModule had to be moved to its own file to avoid circular include dependencies. --- src/preprocessing/passes/quantifier_macros.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/preprocessing') diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp index 69b665854..eef0326b6 100644 --- a/src/preprocessing/passes/quantifier_macros.cpp +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -24,8 +24,8 @@ #include "smt/smt_engine_scope.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/ematching/pattern_term_selector.h" +#include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/rewriter.h" @@ -196,8 +196,8 @@ bool QuantifierMacros::isGroundUfTerm(Node q, Node n) { Node icn = d_preprocContext->getTheoryEngine() ->getQuantifiersEngine() - ->getTermUtil() - ->substituteBoundVariablesToInstConstants(n, q); + ->getQuantifiersRegistry() + .substituteBoundVariablesToInstConstants(n, q); Trace("macros-debug2") << "Get free variables in " << icn << std::endl; std::vector< Node > var; quantifiers::TermUtil::computeInstConstContainsForQuant(q, icn, var); -- cgit v1.2.3