mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

fix sls build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-11 14:02:06 -07:00
parent 73f09fe94a
commit 2ecb1c8b94
5 changed files with 14 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
genaisrc/gai.genai.mts
View file

@ -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

3
package.json
View file

@ -4,6 +4,7 @@
"genaiscript": "^1.63.0"
},
"scripts": {
"gcm": "genaiscript run gcm"
"gcm": "genaiscript run gcm",
"gai": "genaiscript run gai"
}
}

1
src/ast/sls/sls_context.cpp
View file

@ -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) {

2
src/ast/sls/sls_context.h
View file

@ -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<ptr_vector<expr>> 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<sat::clause_info> const& clauses() const { return s.clauses(); }

9
src/ast/sls/sls_euf_plugin.cpp
View file

@ -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));
}