From 5f9eb8917bb37c851ebac084700a53e01a06640d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 29 Aug 2024 15:10:35 -0700 Subject: [PATCH] gcm Signed-off-by: Nikolaj Bjorner --- genaisrc/gcm.genai.mts | 81 +++++++++++++++++++++++++++++++++++ src/ast/sls/bv_sls_eval.cpp | 7 ++- src/ast/sls/bv_sls_fixed.cpp | 37 ++++++++-------- src/ast/sls/sls_bv_plugin.cpp | 2 +- src/ast/sls/sls_context.cpp | 5 +++ src/ast/sls/sls_context.h | 7 +++ 6 files changed, 117 insertions(+), 22 deletions(-) create mode 100644 genaisrc/gcm.genai.mts diff --git a/genaisrc/gcm.genai.mts b/genaisrc/gcm.genai.mts new file mode 100644 index 000000000..b39e9a8e0 --- /dev/null +++ b/genaisrc/gcm.genai.mts @@ -0,0 +1,81 @@ +import { select, input, confirm } from "@inquirer/prompts" + +// Check for staged changes and stage all changes if none are staged +let diff = await host.exec("git", ["diff", "--cached"]) +if (!diff.stdout) { + const stage = await confirm({ + message: "No staged changes. Stage all changes?", + default: true, + }) + if (stage) { + await host.exec("git", ["add", "."]) + diff = await host.exec("git", [ + "diff", + "--cached", + "--", + ".", + ":!**/genaiscript.d.ts", + ]) + } + if (!diff.stdout) cancel("no staged changes") +} + +console.log(diff.stdout) + +let choice +let message +do { + // Generate commit message + message = ( + await runPrompt( + (_) => { + _.def("GIT_DIFF", diff, { maxTokens: 20000 }) + _.$`GIT_DIFF is a diff of all staged changes, coming from the command: +\`\`\` +git diff --cached +\`\`\` +Please generate a concise, one-line commit message for these changes. +- do NOT add quotes` + }, + { cache: false, temperature: 0.8 } + ) + ).text + + // Prompt user for commit message + choice = await select({ + message, + choices: [ + { + name: "commit", + value: "commit", + description: "accept message and commit", + }, + { + name: "edit", + value: "edit", + description: "edit message and commit", + }, + { + name: "regenerate", + value: "regenerate", + description: "regenerate message", + }, + ], + }) + + // Handle user choice + if (choice === "edit") { + message = await input({ + message: "Edit commit message", + required: true, + }) + choice = "commit" + } + // Regenerate message + if (choice === "commit" && message) { + console.log((await host.exec("git", ["commit", "-m", message])).stdout) + if (await confirm({ message: "Push changes?", default: true })) + console.log((await host.exec("git", ["push"])).stdout) + break + } +} while (choice !== "commit") diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index 2649d6f09..e98c3cbba 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -1001,8 +1001,7 @@ namespace bv { if (a.try_set(m_tmp)) return true; } - return a.set_random(m_rand); - + return a.set_random(m_rand); } bool sls_eval::try_repair_sub(bvect const& e, bvval& a, bvval & b, unsigned i) { @@ -1269,7 +1268,7 @@ namespace bv { } bool sls_eval::try_repair_ule(bool e, bvval& a, bvval const& b) { - verbose_stream() << "try-repair-ule " << e << " " << a << " " << b << "\n"; + //verbose_stream() << "try-repair-ule " << e << " " << a << " " << b << "\n"; if (e) { // a <= t return a.set_random_at_most(b.bits(), m_rand); @@ -1285,7 +1284,7 @@ namespace bv { } bool sls_eval::try_repair_uge(bool e, bvval& a, bvval const& b) { - verbose_stream() << "try-repair-uge " << e << " " << a << " " << b << "\n"; + //verbose_stream() << "try-repair-uge " << e << " " << a << " " << b << "\n"; if (e) { // a >= t return a.set_random_at_least(b.bits(), m_rand); diff --git a/src/ast/sls/bv_sls_fixed.cpp b/src/ast/sls/bv_sls_fixed.cpp index eac8f69c6..16492f2b3 100644 --- a/src/ast/sls/bv_sls_fixed.cpp +++ b/src/ast/sls/bv_sls_fixed.cpp @@ -312,29 +312,32 @@ namespace bv { return; switch (e->get_decl_kind()) { case OP_BAND: { - SASSERT(e->get_num_args() == 2); - auto& a = ev.wval(e->get_arg(0)); - auto& b = ev.wval(e->get_arg(1)); - // (a.fixed & b.fixed) | (a.fixed & ~a.bits) | (b.fixed & ~b.bits) - for (unsigned i = 0; i < a.nw; ++i) - v.fixed[i] = (a.fixed[i] & b.fixed[i]) | (a.fixed[i] & ~a.bits(i)) | (b.fixed[i] & ~b.bits(i)); + if (e->get_num_args() == 2) { + auto& a = ev.wval(e->get_arg(0)); + auto& b = ev.wval(e->get_arg(1)); + // (a.fixed & b.fixed) | (a.fixed & ~a.bits) | (b.fixed & ~b.bits) + for (unsigned i = 0; i < a.nw; ++i) + v.fixed[i] = (a.fixed[i] & b.fixed[i]) | (a.fixed[i] & ~a.bits(i)) | (b.fixed[i] & ~b.bits(i)); + } break; } case OP_BOR: { - SASSERT(e->get_num_args() == 2); - auto& a = ev.wval(e->get_arg(0)); - auto& b = ev.wval(e->get_arg(1)); - // (a.fixed & b.fixed) | (a.fixed & a.bits) | (b.fixed & b.bits) - for (unsigned i = 0; i < a.nw; ++i) - v.fixed[i] = (a.fixed[i] & b.fixed[i]) | (a.fixed[i] & a.bits(i)) | (b.fixed[i] & b.bits(i)); + if (e->get_num_args() == 2) { + auto& a = ev.wval(e->get_arg(0)); + auto& b = ev.wval(e->get_arg(1)); + // (a.fixed & b.fixed) | (a.fixed & a.bits) | (b.fixed & b.bits) + for (unsigned i = 0; i < a.nw; ++i) + v.fixed[i] = (a.fixed[i] & b.fixed[i]) | (a.fixed[i] & a.bits(i)) | (b.fixed[i] & b.bits(i)); + } break; } case OP_BXOR: { - SASSERT(e->get_num_args() == 2); - auto& a = ev.wval(e->get_arg(0)); - auto& b = ev.wval(e->get_arg(1)); - for (unsigned i = 0; i < a.nw; ++i) - v.fixed[i] = a.fixed[i] & b.fixed[i]; + if (e->get_num_args() == 2) { + auto& a = ev.wval(e->get_arg(0)); + auto& b = ev.wval(e->get_arg(1)); + for (unsigned i = 0; i < a.nw; ++i) + v.fixed[i] = a.fixed[i] & b.fixed[i]; + } break; } case OP_BNOT: { diff --git a/src/ast/sls/sls_bv_plugin.cpp b/src/ast/sls/sls_bv_plugin.cpp index efb56670a..7e308db10 100644 --- a/src/ast/sls/sls_bv_plugin.cpp +++ b/src/ast/sls/sls_bv_plugin.cpp @@ -91,7 +91,7 @@ namespace sls { ctx.new_value_eh(t); is_sat = false; } - return true; + return is_sat; } std::ostream& bv_plugin::display(std::ostream& out) const { diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp index 076bef5ad..35c3f2bf6 100644 --- a/src/ast/sls/sls_context.cpp +++ b/src/ast/sls/sls_context.cpp @@ -119,6 +119,7 @@ namespace sls { TRACE("sls", tout << "repair down " << mk_bounded_pp(e, m) << "\n"); if (is_app(e)) { auto p = m_plugins.get(get_fid(e), nullptr); + ++m_stats.m_num_repair_down; if (p && !p->repair_down(to_app(e)) && !m_repair_up.contains(e->get_id())) { IF_VERBOSE(3, verbose_stream() << "revert repair: " << mk_bounded_pp(e, m) << "\n"); m_repair_up.insert(e->get_id()); @@ -128,6 +129,7 @@ namespace sls { while (!m_repair_up.empty() && !m_new_constraint && m.inc()) { auto id = m_repair_up.erase_min(); expr* e = term(id); + ++m_stats.m_num_repair_up; TRACE("sls", tout << "repair up " << mk_bounded_pp(e, m) << "\n"); if (is_app(e)) { auto p = m_plugins.get(get_fid(e), nullptr); @@ -531,11 +533,14 @@ namespace sls { for (auto p : m_plugins) if (p) p->collect_statistics(st); + st.update("sls-repair-down", m_stats.m_num_repair_down); + st.update("sls-repair-up", m_stats.m_num_repair_up); } void context::reset_statistics() { for (auto p : m_plugins) if (p) p->reset_statistics(); + m_stats.reset(); } } diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h index b0afcdde5..0b8ded614 100644 --- a/src/ast/sls/sls_context.h +++ b/src/ast/sls/sls_context.h @@ -94,6 +94,12 @@ namespace sls { } }; + struct stats { + unsigned m_num_repair_down = 0; + unsigned m_num_repair_up = 0; + void reset() { memset(this, 0, sizeof(*this)); } + }; + ast_manager& m; sat_solver_context& s; scoped_ptr_vector m_plugins; @@ -113,6 +119,7 @@ namespace sls { less_depth m_ld; heap m_repair_down; heap m_repair_up; + stats m_stats; void register_plugin(plugin* p);