mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 21:16:02 +00:00
Code Activity

Merge branch 'ilana' into parallel-solving

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-08-04 09:47:53 -07:00 • committed by GitHub
commit a0a06704dc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context.h
View file

@ -192,11 +192,13 @@ namespace smt {
svector<bool_var_data> m_bdata; //!< mapping bool_var -> data
svector<double> m_activity;
updatable_priority_queue::priority_queue<bool_var, double> m_pq_scores;
struct lit_node : dll_base<lit_node> {
literal lit;
lit_node(literal l) : lit(l) { init(this); }
};
lit_node* m_dll_lits;
svector<std::array<double, 2>> m_lit_scores;
clause_vector m_aux_clauses;

3
src/smt/smt_parallel.cpp
View file

@ -109,6 +109,7 @@ namespace smt {
auto cube_pq = [&](context& ctx, expr_ref_vector& lasms, expr_ref& c) {
unsigned k = 3; // Number of top literals you want
ast_manager& m = ctx.get_manager();
// Get the entire fixed-size priority queue (it's not that big)
@ -302,7 +303,7 @@ namespace smt {
finished_id = i;
result = r;
}
else if (!first) return;
else if (!first) return; // nothing new to contribute
}
// Cancel limits on other threads now that a result is known