From b170f101481c51e4d753212b484bc5a48191f6ed Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 2 Oct 2024 13:26:46 -0700 Subject: [PATCH] reorder template definition Signed-off-by: Nikolaj Bjorner --- src/qe/qe_mbp.cpp | 64 ++++++++++++++++++++---------------- src/sat/smt/arith_axioms.cpp | 2 +- 2 files changed, 36 insertions(+), 30 deletions(-) diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index b5fafeeac..00926f3fb 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -45,35 +45,35 @@ using namespace qe; namespace { // rewrite select(store(a, i, k), j) into k if m \models i = j and select(a, j) if m \models i != j struct rd_over_wr_rewriter : public default_rewriter_cfg { - ast_manager &m; - array_util m_arr; - model_evaluator m_eval; - expr_ref_vector m_sc; - - rd_over_wr_rewriter(ast_manager& man, model& mdl): m(man), m_arr(m), m_eval(mdl), m_sc(m) { - m_eval.set_model_completion(false); - } - - br_status reduce_app(func_decl *f, unsigned num, expr *const *args, - expr_ref &result, proof_ref &result_pr) { - if (m_arr.is_select(f) && m_arr.is_store(args[0])) { - expr_ref ind1(m), ind2(m); - ind1 = m_eval(args[1]); - ind2 = m_eval(to_app(args[0])->get_arg(1)); - if (ind1 == ind2) { - result = to_app(args[0])->get_arg(2); - m_sc.push_back(m.mk_eq(args[1], to_app(args[0])->get_arg(1))); - return BR_DONE; - } - m_sc.push_back(m.mk_not(m.mk_eq(args[1], to_app(args[0])->get_arg(1)))); - expr_ref_vector new_args(m); - new_args.push_back(to_app(args[0])->get_arg(0)); - new_args.push_back(args[1]); - result = m_arr.mk_select(new_args); - return BR_REWRITE1; + ast_manager &m; + array_util m_arr; + model_evaluator m_eval; + expr_ref_vector m_sc; + + rd_over_wr_rewriter(ast_manager& man, model& mdl): m(man), m_arr(m), m_eval(mdl), m_sc(m) { + m_eval.set_model_completion(false); + } + + br_status reduce_app(func_decl *f, unsigned num, expr *const *args, + expr_ref &result, proof_ref &result_pr) { + if (m_arr.is_select(f) && m_arr.is_store(args[0])) { + expr_ref ind1(m), ind2(m); + ind1 = m_eval(args[1]); + ind2 = m_eval(to_app(args[0])->get_arg(1)); + if (ind1 == ind2) { + result = to_app(args[0])->get_arg(2); + m_sc.push_back(m.mk_eq(args[1], to_app(args[0])->get_arg(1))); + return BR_DONE; } - return BR_FAILED; + m_sc.push_back(m.mk_not(m.mk_eq(args[1], to_app(args[0])->get_arg(1)))); + expr_ref_vector new_args(m); + new_args.push_back(to_app(args[0])->get_arg(0)); + new_args.push_back(args[1]); + result = m_arr.mk_select(new_args); + return BR_REWRITE1; } + return BR_FAILED; + } }; // rewrite all occurrences of (as const arr c) to (as const arr v) where v = m_eval(c) struct app_const_arr_rewriter : public default_rewriter_cfg { @@ -123,6 +123,11 @@ namespace { } }; } + +template class rewriter_tpl; +template class rewriter_tpl; + + void rewrite_as_const_arr(expr* in, model& mdl, expr_ref& out) { app_const_arr_rewriter cfg(out.m(), mdl); rewriter_tpl rw(out.m(), false, cfg); @@ -675,6 +680,8 @@ public: vars.reset(); vars.append(other_vars); } + + }; mbproj::mbproj(ast_manager& m, params_ref const& p) { @@ -715,5 +722,4 @@ opt::inf_eps mbproj::maximize(expr_ref_vector const& fmls, model& mdl, app* t, e scoped_no_proof _sp(fmls.get_manager()); return m_impl->maximize(fmls, mdl, t, ge, gt); } -template class rewriter_tpl; -template class rewriter_tpl; + diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index 97a8ee563..59529658b 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/src/sat/smt/arith_axioms.cpp @@ -324,7 +324,7 @@ namespace arith { void solver::mk_bv_axiom(app* n) { - unsigned sz; + unsigned sz = 0; expr* _x = nullptr, * _y = nullptr; VERIFY(a.is_band(n, sz, _x, _y) || a.is_shl(n, sz, _x, _y) || a.is_ashr(n, sz, _x, _y) || a.is_lshr(n, sz, _x, _y)); rational N = rational::power_of_two(sz);