diff --git a/genaisrc/gai.genai.mts b/genaisrc/gai.genai.mts index 9de3cf11a..45828b6d0 100644 --- a/genaisrc/gai.genai.mts +++ b/genaisrc/gai.genai.mts @@ -1,10 +1,12 @@ script({ tools: ["agent_fs", "agent_git", "agent_github"], + model: "azure:gpt-4o", + maxTokens: 20000 }) const { - workflow = "latest failed", - failure_run_id = "latest", + workflow = "RISC V and PowerPC 64", + failure_run_id = "11296730058", branch = await git.defaultBranch(), } = env.vars diff --git a/package.json b/package.json index 437d8ce95..1a6c721c0 100644 --- a/package.json +++ b/package.json @@ -4,6 +4,7 @@ "genaiscript": "^1.63.0" }, "scripts": { - "gcm": "genaiscript run gcm" + "gcm": "genaiscript run gcm", + "gai": "genaiscript run gai" } } diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp index 6eb396fa5..71c86efe0 100644 --- a/src/ast/sls/sls_context.cpp +++ b/src/ast/sls/sls_context.cpp @@ -44,6 +44,7 @@ namespace sls { void context::updt_params(params_ref const& p) { smt_params_helper smtp(p); m_rand.set_seed(smtp.random_seed()); + m_params.append(p); } void context::register_plugin(plugin* p) { diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h index 5cdbdd3f7..4eccba0bc 100644 --- a/src/ast/sls/sls_context.h +++ b/src/ast/sls/sls_context.h @@ -108,6 +108,7 @@ namespace sls { indexed_uint_set m_relevant, m_visited; expr_ref_vector m_atoms; unsigned_vector m_atom2bool_var; + params_ref m_params; vector> m_parents; sat::literal_vector m_root_literals, m_unit_literals; indexed_uint_set m_unit_indices; @@ -149,6 +150,7 @@ namespace sls { void on_restart(); void updt_params(params_ref const& p); + params_ref const& get_params() const { return m_params; } // expose sat_solver to plugins vector const& clauses() const { return s.clauses(); } diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp index 5114e3829..aee13acc8 100644 --- a/src/ast/sls/sls_euf_plugin.cpp +++ b/src/ast/sls/sls_euf_plugin.cpp @@ -38,7 +38,7 @@ namespace sls { void euf_plugin::initialize() { m_incremental = ctx.get_params().get_bool("euf_incremental", m_incremental); - IF_VERBOSE(2, verbose_stream() << "sls.euf: incremental " << m_incremental << < "\n"); + IF_VERBOSE(2, verbose_stream() << "sls.euf: incremental " << m_incremental << "\n"); } void euf_plugin::start_propagation() { @@ -80,6 +80,7 @@ namespace sls { replay(); } void euf_plugin::resolve() { + auto& g = *m_g; if (!g.inconsistent()) return; @@ -118,7 +119,7 @@ namespace sls { auto l = m_replay_stack.back(); m_replay_stack.pop_back(); propagate_literal_incremental_step(l); - if (g.inconsistent()) + if (m_g->inconsistent()) resolve(); } } @@ -149,8 +150,8 @@ namespace sls { expr_ref eq(m.mk_eq(a, b), m); auto c = g.find(eq); if (!g.find(eq)) { - enode* args[2] = { g.find(a), g.find(b) }; - c = g.mk(eq, 2, args, nullptr); + euf::enode* args[2] = { g.find(a), g.find(b) }; + c = g.mk(eq, 0, 2, args); } g.merge(c, g.find(m.mk_false()), to_ptr(lit)); }