reorder template definition

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Oct 2, 2024 · b170f10 · b170f10
1 parent 6dec943
commit b170f10
Show file tree

Hide file tree

Showing 2 changed files with 36 additions and 30 deletions.
diff --git 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<app_const_arr_rewriter>;
+template class rewriter_tpl<rd_over_wr_rewriter>;
+
+
 void rewrite_as_const_arr(expr* in, model& mdl, expr_ref& out) {
     app_const_arr_rewriter cfg(out.m(), mdl);
     rewriter_tpl<app_const_arr_rewriter> rw(out.m(), false, cfg);
@@ -675,6 +680,8 @@ class mbproj::impl {
         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<app_const_arr_rewriter>;
-template class rewriter_tpl<rd_over_wr_rewriter>;
+
diff --git 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);