From 31914d8ecf8145510776802c018f134d02a21888 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Oct 2022 03:47:57 -0700 Subject: [PATCH] simplify purified expressions --- src/qe/mbp/mbp_term_graph.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/qe/mbp/mbp_term_graph.cpp b/src/qe/mbp/mbp_term_graph.cpp index 4709c8c72..624febffd 100644 --- a/src/qe/mbp/mbp_term_graph.cpp +++ b/src/qe/mbp/mbp_term_graph.cpp @@ -24,6 +24,7 @@ Notes: #include "ast/ast_util.h" #include "ast/for_each_expr.h" #include "ast/occurs.h" +#include "ast/rewriter/th_rewriter.h" #include "model/model_evaluator.h" #include "qe/mbp/mbp_term_graph.h" @@ -583,6 +584,7 @@ namespace mbp { ast_manager &m; u_map m_term2app; u_map m_root2rep; + th_rewriter m_rewriter; model_ref m_model; expr_ref_vector m_pinned; // tracks expr in the maps @@ -609,7 +611,7 @@ namespace mbp { } TRACE("qe_verbose", tout << *ch << " -> " << mk_pp(e, m) << "\n";); } - expr* pure = m.mk_app(a->get_decl(), kids.size(), kids.data()); + expr_ref pure = m_rewriter.mk_app(a->get_decl(), kids.size(), kids.data()); m_pinned.push_back(pure); add_term2app(t, pure); return pure; @@ -940,7 +942,7 @@ namespace mbp { } public: - projector(term_graph &tg) : m_tg(tg), m(m_tg.m), m_pinned(m) {} + projector(term_graph &tg) : m_tg(tg), m(m_tg.m), m_rewriter(m), m_pinned(m) {} void add_term2app(term const& t, expr* a) { m_term2app.insert(t.get_id(), a);