diff options
Diffstat (limited to 'src/preprocessing/passes/sygus_inference.cpp')
| -rw-r--r-- | src/preprocessing/passes/sygus_inference.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index d105c436a..8abd77a27 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -21,7 +21,7 @@ #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/quantifiers_preprocess.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/sygus_utils.h" #include "theory/rewriter.h" @@ -65,7 +65,7 @@ PreprocessingPassResult SygusInference::applyInternal( prev.substitute(funs.begin(), funs.end(), sols.begin(), sols.end()); if (curr != prev) { - curr = theory::Rewriter::rewrite(curr); + curr = rewrite(curr); Trace("sygus-infer-debug") << "...rewrote " << prev << " to " << curr << std::endl; assertionsToPreprocess->replace(i, curr); @@ -118,6 +118,7 @@ bool SygusInference::solveSygus(const std::vector<Node>& assertions, // process eassertions std::vector<Node> processed_assertions; + quantifiers::QuantifiersPreprocess qp(d_env); for (const Node& as : eassertions) { // substitution for this assertion @@ -126,12 +127,12 @@ bool SygusInference::solveSygus(const std::vector<Node>& assertions, std::map<TypeNode, unsigned> type_count; Node pas = as; // rewrite - pas = theory::Rewriter::rewrite(pas); + pas = rewrite(pas); Trace("sygus-infer") << "assertion : " << pas << std::endl; if (pas.getKind() == FORALL) { // preprocess the quantified formula - TrustNode trn = quantifiers::QuantifiersRewriter::preprocess(pas); + TrustNode trn = qp.preprocess(pas); if (!trn.isNull()) { pas = trn.getNode(); |