Refactor and fix uninitialized variables and improve function consist…

…ency across multiple modules

genaisrc/.#gcm.genai.mts

@@ -0,0 +1 @@
+nbjorner@LAPTOP-04AEAFKH.21956:1726928207

genaisrc/fw.genai.mts

@@ -0,0 +1,37 @@
+// This script is used to invoke ninja and automatically suggest fixes to build warnings
+import { select, input, confirm } from "@inquirer/prompts"
+
+
+// TODO: invoke ninja in z3 build directory
+// - pipe output of build to a string buffer
+// - chunk up warning/error messages one by one
+// - create AI query to have the warning/error fixed
+// - stage the changes
+// - recompile, rinse repeat until fixes
+// - backtrack from failed fixes?
+
+// let ninjaout = await host.exec("ninja", [])
+// console.log(ninjaout.stdout)
+// await runPrompt( (_) => { _.def("BUILDMSG", ninjaout, { maxTokens: 20000})
+//                           _.$`BUILDMSG is the output of a ninja build. Please generate fixes for the warning messages, stage the changes. Repeat the build process for up to three iterations to fix error or warning messages` }
+
+
+
+defData("EXAMPLEMSG","
+/home/nbjorner/z3/src/smt/theory_str.cpp: In member function ‘void smt::theory_str::instantiate_axiom_CharAt(smt::enode*)’:
+/home/nbjorner/z3/src/smt/theory_str.cpp:1092:15: warning: ‘arg0’ may be used uninitialized [-Wmaybe-uninitialized]
+ 1092 |         expr* arg0, *arg1;
+      |               ^~~~
+In file included from /home/nbjorner/z3/src/ast/ast_smt2_pp.h:26,
+                 from /home/nbjorner/z3/src/smt/theory_str.cpp:17:
+In member function ‘app* arith_util::mk_lt(expr*, expr*) const’,
+    inlined from ‘void smt::theory_str::instantiate_axiom_CharAt(smt::enode*)’ at /home/nbjorner/z3/src/smt/theory_str.cpp:1110:40:
+")
+
+// TODO: script to extract file contents
+// TODO: script what to update.
+
+$`
+You are a helpful AI assistant who knows C++ and can fix build warnings.
+You are given the following warning message ${EXAMPLEMSG}. Create a fix.
+`

src/ast/bv_decl_plugin.cpp

@@ -927,7 +927,7 @@ sort * bv_util::mk_sort(unsigned bv_size) {
 }
 
 unsigned bv_util::get_int2bv_size(parameter const& p) {
-    int sz;
+    int sz = 0;
     VERIFY(m_plugin->get_int2bv_size(1, &p, sz));
     return static_cast<unsigned>(sz);
 }
@@ -951,4 +951,4 @@ app* bv_util::mk_bv_rotate_left(expr* arg, unsigned n) {
 app* bv_util::mk_bv_rotate_right(expr* arg, unsigned n) {
     parameter p(n);
     return m_manager.mk_app(get_fid(), OP_ROTATE_RIGHT, 1, &p, 1, &arg);
-}
+}

src/ast/euf/euf_ac_plugin.cpp

@@ -907,7 +907,6 @@ namespace euf {
         m_dst_r.reset();
         m_dst_r.append(monomial(dst.r).m_nodes);
         unsigned src_r_size = m_src_r.size();
-        unsigned dst_r_size = m_dst_r.size();
         SASSERT(src_r_size == monomial(src.r).size());
         // dst_r contains C
         // src_r contains E

src/ast/euf/euf_ac_plugin.h

@@ -136,7 +136,7 @@ namespace euf {
         };
 
         theory_id                m_fid = 0;
-        unsigned                 m_op = null_decl_kind;
+        decl_kind                m_op = null_decl_kind;
         func_decl*               m_decl = nullptr;
         vector<eq>               m_eqs;
         ptr_vector<node>         m_nodes;

src/qe/mbp/mbp_arith.cpp

@@ -304,7 +304,7 @@ namespace mbp {
             return rational(b.is_pos() ? -1 : 1);
         }
 
-        bool operator()(model& model, app* v, app_ref_vector& vars, expr_ref_vector& lits) {
+        bool project1(model& model, app* v, app_ref_vector& vars, expr_ref_vector& lits) {
             app_ref_vector vs(m);
             vs.push_back(v);
             vector<def> defs;
@@ -710,8 +710,8 @@ namespace mbp {
         dealloc(m_imp);
     }
 
-    bool arith_project_plugin::operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) {
-        return (*m_imp)(model, var, vars, lits);
+    bool arith_project_plugin::project1(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) {
+        return m_imp->project1(model, var, vars, lits);
     }
 
     bool arith_project_plugin::operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
@@ -743,6 +743,6 @@ namespace mbp {
         ast_manager& m = lits.get_manager();
         arith_project_plugin ap(m);
         app_ref_vector vars(m);
-        return ap(model, var, vars, lits);
+        return ap.project1(model, var, vars, lits);
     }
 }

src/qe/mbp/mbp_arith.h

@@ -26,7 +26,7 @@ namespace mbp {
         arith_project_plugin(ast_manager& m);
         ~arith_project_plugin() override;
 
-        bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override;
+        bool project1(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override;
         bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override { return false; }
         family_id get_family_id() override;
         bool operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;

src/qe/mbp/mbp_arrays.cpp

@@ -1444,7 +1444,7 @@ namespace mbp {
         dealloc(m_imp);
     }
 
-    bool array_project_plugin::operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) {
+    bool array_project_plugin::project1(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) {
         ast_manager& m = vars.get_manager();
         app_ref_vector vvars(m, 1, &var);
         expr_ref fml = mk_and(lits);

src/qe/mbp/mbp_arrays.h

@@ -31,7 +31,7 @@ namespace mbp {
     public:
         array_project_plugin(ast_manager& m);
         ~array_project_plugin() override;
-        bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override;
+        bool project1(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override;
         bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
         void operator()(model& model, app_ref_vector& vars, expr_ref& fml, app_ref_vector& aux_vars, bool reduce_all_selects);
         family_id get_family_id() override;

src/qe/mbp/mbp_datatypes.cpp

@@ -40,7 +40,7 @@ namespace mbp {
             return lift_foreign(vars, lits);
         }
 
-        bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) {
+        bool project1(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) {
             expr_ref val = model(var);
             SASSERT(is_app(val));
             TRACE("qe", tout << mk_pp(var, m) << " := " << val << "\n";);
@@ -292,8 +292,8 @@ namespace mbp {
         dealloc(m_imp);
     }
 
-    bool datatype_project_plugin::operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) {
-        return (*m_imp)(model, var, vars, lits);
+    bool datatype_project_plugin::project1(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) {
+        return m_imp->project1(model, var, vars, lits);
     }
 
     bool datatype_project_plugin::solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) {

src/qe/mbp/mbp_datatypes.h

@@ -31,7 +31,7 @@ namespace mbp {
     public:
         datatype_project_plugin(ast_manager& m);
         ~datatype_project_plugin() override;
-        bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override;
+        bool project1(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override;
         bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
         family_id get_family_id() override;
         bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) override;

src/qe/mbp/mbp_plugin.h

@@ -60,7 +60,7 @@ namespace mbp {
     public:
         project_plugin(ast_manager& m) :m(m), m_cache(m), m_args(m), m_pure_eqs(m) {}
         virtual ~project_plugin() = default;
-        virtual bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) { return false; }
+        virtual bool project1(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) { return false; }
         /**
            \brief partial solver.
         */

src/qe/qe_mbp.cpp

@@ -452,7 +452,7 @@ class mbproj::impl {
                 var = vars.back();
                 vars.pop_back();
                 mbp::project_plugin* p = get_plugin(var);
-                if (p && (*p)(model, var, vars, fmls)) {
+                if (p && p->project1(model, var, vars, fmls)) {
                     progress = true;
                 }
                 else {

src/sat/sat_solver/inc_sat_solver.cpp

@@ -193,8 +193,6 @@ class inc_sat_solver : public solver {
         m_solver.pop_to_base_level();
         m_core.reset();
 
-
-
         if (m_solver.inconsistent()) return l_false;
         expr_ref_vector _assumptions(m);
         obj_map<expr, expr*> asm2fml;

src/sat/smt/arith_axioms.cpp

@@ -325,7 +325,7 @@ namespace arith {
 
     void solver::mk_bv_axiom(app* n) {
         unsigned sz;
-        expr* _x, * _y;
+        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);
         expr_ref x(a.mk_mod(_x, a.mk_int(N)), m);

src/sat/smt/array_internalize.cpp

@@ -128,7 +128,7 @@ namespace array {
             internalize_lambda_eh(n);
             break;
         case OP_SET_SUBSET: {
-            expr* x, *y;
+            expr* x = nullptr, *y = nullptr;
             VERIFY(a.is_subset(n->get_expr(), x, y));
             expr_ref diff(a.mk_setminus(x, y), m);
             expr_ref emp(a.mk_empty_set(x->get_sort()), m);

src/sat/smt/intblast_solver.cpp

@@ -91,7 +91,7 @@ namespace intblast {
 
     void solver::eq_internalized(euf::enode* n) {
         expr* e = n->get_expr();
-        expr* x, * y;
+        expr* x = nullptr, * y = nullptr;
         VERIFY(m.is_eq(n->get_expr(), x, y));
         SASSERT(bv.is_bv(x));
         if (!is_translated(e)) {
@@ -482,7 +482,7 @@ namespace intblast {
             return r >= 0;
         if (is_bounded(e, N))
             return true;
-        expr* x, * y;
+        expr* x = nullptr, * y = nullptr;
         if (a.is_mul(e, x, y)) 
             return is_non_negative(bv_expr, x) && is_non_negative(bv_expr, y);
         if (a.is_add(e, x, y))
@@ -544,7 +544,7 @@ namespace intblast {
     */
     expr* solver::amod(expr* bv_expr, expr* x, rational const& N) {
         rational v;
-        expr* r, *c, * t, * e;
+        expr* r = nullptr, *c = nullptr, * t = nullptr, * e = nullptr;
         if (m.is_ite(x, c, t, e))
             r = m.mk_ite(c, amod(bv_expr, t, N), amod(bv_expr, e, N));
         else if (a.is_idiv(x, t, e) && a.is_numeral(t, v) && 0 <= v && v < N && is_non_negative(bv_expr, e))
@@ -880,7 +880,7 @@ namespace intblast {
             r = umod(bv_expr, 0);
             SASSERT(bv.get_bv_size(e) >= bv.get_bv_size(bv_expr));
             unsigned arg_sz = bv.get_bv_size(bv_expr);
-            unsigned sz = bv.get_bv_size(e);
+            //unsigned sz = bv.get_bv_size(e);
             // rational N = rational::power_of_two(sz);
             rational M = rational::power_of_two(arg_sz);
             expr* signbit = a.mk_ge(r, a.mk_int(M / 2));