diff --git a/genaisrc/.#gcm.genai.mts b/genaisrc/.#gcm.genai.mts new file mode 100644 index 000000000..9102e16be --- /dev/null +++ b/genaisrc/.#gcm.genai.mts @@ -0,0 +1 @@ +nbjorner@LAPTOP-04AEAFKH.21956:1726928207 \ No newline at end of file diff --git a/genaisrc/fw.genai.mts b/genaisrc/fw.genai.mts new file mode 100644 index 000000000..11f4ed579 --- /dev/null +++ b/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. +` diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 5dd9f6080..8c9a5652f 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/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(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); -} \ No newline at end of file +} diff --git a/src/ast/euf/euf_ac_plugin.cpp b/src/ast/euf/euf_ac_plugin.cpp index 174ef363b..69d0e6572 100644 --- a/src/ast/euf/euf_ac_plugin.cpp +++ b/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 diff --git a/src/ast/euf/euf_ac_plugin.h b/src/ast/euf/euf_ac_plugin.h index d55d7dbb4..809ac55cf 100644 --- a/src/ast/euf/euf_ac_plugin.h +++ b/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 m_eqs; ptr_vector m_nodes; diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp index ef4428fa7..8bbf3a002 100644 --- a/src/qe/mbp/mbp_arith.cpp +++ b/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 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); } } diff --git a/src/qe/mbp/mbp_arith.h b/src/qe/mbp/mbp_arith.h index ca4cccb74..666ffffc4 100644 --- a/src/qe/mbp/mbp_arith.h +++ b/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; diff --git a/src/qe/mbp/mbp_arrays.cpp b/src/qe/mbp/mbp_arrays.cpp index fa7ec8cb5..6e036a714 100644 --- a/src/qe/mbp/mbp_arrays.cpp +++ b/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); diff --git a/src/qe/mbp/mbp_arrays.h b/src/qe/mbp/mbp_arrays.h index 7dd904108..ed06ba78b 100644 --- a/src/qe/mbp/mbp_arrays.h +++ b/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; diff --git a/src/qe/mbp/mbp_datatypes.cpp b/src/qe/mbp/mbp_datatypes.cpp index 32e2b9f27..5a88016db 100644 --- a/src/qe/mbp/mbp_datatypes.cpp +++ b/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) { diff --git a/src/qe/mbp/mbp_datatypes.h b/src/qe/mbp/mbp_datatypes.h index f30aaaa9f..28f93089d 100644 --- a/src/qe/mbp/mbp_datatypes.h +++ b/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& defs) override; diff --git a/src/qe/mbp/mbp_plugin.h b/src/qe/mbp/mbp_plugin.h index 4f73b92e6..c270489e8 100644 --- a/src/qe/mbp/mbp_plugin.h +++ b/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. */ diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index 97f12238d..b5fafeeac 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -452,7 +452,7 @@ public: 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 { diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 5e0d10918..522638c1d 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -193,8 +193,6 @@ public: m_solver.pop_to_base_level(); m_core.reset(); - - if (m_solver.inconsistent()) return l_false; expr_ref_vector _assumptions(m); obj_map asm2fml; diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index 7270e7080..f35f3851a 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/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); diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp index d5a1dd2c5..9e41be3bb 100644 --- a/src/sat/smt/array_internalize.cpp +++ b/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); diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index f91113d59..d6dfe57d7 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/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));