mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 10:19:23 +00:00
Code Activity

snapshot

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-08-04 09:44:32 -07:00
parent d593bb89f3
commit d190c83984
4 changed files with 29 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/smt_context.h
View file

@ -199,7 +199,8 @@ namespace smt {
};
lit_node* m_dll_lits;
svector<std::array<double, 2>> m_lit_scores;
svector<double> m_lit_scores[2];
clause_vector m_aux_clauses;
clause_vector m_lemmas;
@ -947,11 +948,14 @@ namespace smt {
void dump_axiom(unsigned n, literal const* lits);
void add_scores(unsigned n, literal const* lits);
void reset_scores() {
for (auto& s : m_lit_scores) s[0] = s[1] = 0.0;
for (auto& e : m_lit_scores[0])
e = 0;
for (auto& e : m_lit_scores[1])
e = 0;
m_pq_scores.clear(); // Clear the priority queue heap as well
}
double get_score(literal l) const {
return m_lit_scores[l.var()][l.sign()];
return m_lit_scores[l.sign()][l.var()];
}
public:

11
src/smt/smt_internalizer.cpp
View file

@ -931,8 +931,10 @@ namespace smt {
set_bool_var(id, v);
m_bdata.reserve(v+1);
m_activity.reserve(v+1);
m_lit_scores.reserve(v + 1);
m_lit_scores[v][0] = m_lit_scores[v][1] = 0.0;
m_lit_scores[0].reserve(v + 1);
m_lit_scores[1].reserve(v + 1);
m_lit_scores[0][v] = m_lit_scores[1][v] = 0.0;
m_bool_var2expr.reserve(v+1);
m_bool_var2expr[v] = n;
literal l(v, false);
@ -1543,10 +1545,9 @@ namespace smt {
auto lit = lits[i];
unsigned v = lit.var(); // unique key per literal
auto curr_score = m_lit_scores[v][0] * m_lit_scores[v][1];
m_lit_scores[v][lit.sign()] += 1.0 / n;
m_lit_scores[lit.sign()][v] += 1.0 / n;
auto new_score = m_lit_scores[v][0] * m_lit_scores[v][1];
auto new_score = m_lit_scores[0][v] * m_lit_scores[1][v];
m_pq_scores.set(v, new_score);
}

10
src/smt/smt_parallel.cpp
View file

@ -97,16 +97,6 @@ namespace smt {
}
auto cube = [](context& ctx, expr_ref_vector& lasms, expr_ref& c) {
lookahead lh(ctx);
c = lh.choose();
if (c) {
if ((ctx.get_random_value() % 2) == 0)
c = c.get_manager().mk_not(c);
lasms.push_back(c);
}
};
auto cube_pq = [&](context& ctx, expr_ref_vector& lasms, expr_ref& c) {
unsigned k = 3; // Number of top literals you want

16
src/smt/smt_parallel.h
View file

@ -24,6 +24,22 @@ namespace smt {
class parallel {
context& ctx;
class worker {
ast_manager m;
context ctx;
expr_ref_vector asms;
public:
worker(context& ctx, expr_ref_vector const& asms);
void run();
void cancel();
};
std::mutex mux;
void set_unsat();
void set_sat(ast_translation& tr, model& m);
void get_cubes(ast_translation& tr, expr_ref_vector& cubes);
public:
parallel(context& ctx): ctx(ctx) {}