mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-30 16:03:16 +00:00
Code Activity

fix compilation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-07-25 15:36:37 -07:00
parent f6fc5045d2
commit 9bba708f9b
3 changed files with 8 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context.h
View file

@ -189,7 +189,7 @@ namespace smt {
unsigned_vector m_lit_occs; //!< occurrence count of literals
svector<bool_var_data> m_bdata; //!< mapping bool_var -> data
svector<double> m_activity;
svector<double[2]> m_scores;
svector<double> m_scores[2];
clause_vector m_aux_clauses;
clause_vector m_lemmas;
vector<clause_vector> m_clauses_to_reinit;

7
src/smt/smt_internalizer.cpp
View file

@ -928,8 +928,9 @@ namespace smt {
set_bool_var(id, v);
m_bdata.reserve(v+1);
m_activity.reserve(v+1);
m_scores.reserve(v + 1);
m_scores[v][0] = m_scores[v][1] = 0.0;
m_scores[0].reserve(v + 1);
m_scores[1].reserve(v + 1);
m_scores[0][v] = m_scores[1][v] = 0.0;
m_bool_var2expr.reserve(v+1);
m_bool_var2expr[v] = n;
literal l(v, false);
@ -1531,7 +1532,7 @@ namespace smt {
for (unsigned i = 0; i < n; ++i) {
auto lit = lits[i];
unsigned v = lit.var();
m_scores[v][lit.sign()] += 1.0 / n;
m_scores[lit.sign()][v] += 1.0 / n;
}
}

3
src/smt/smt_parallel.cpp
View file

@ -92,6 +92,9 @@ namespace smt {
sl.push_child(&(new_m->limit()));
}
// Access socres as follows:
// ctx.m_scores[lit.sign()][lit.var()]
// auto cube = [](context& ctx, expr_ref_vector& lasms, expr_ref& c) {
// lookahead lh(ctx);
// c = lh.choose();