mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 13:06:05 +00:00
Code Activity

sketch scheme not using heap

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-08-22 15:30:27 -07:00
parent 394173f98c
commit 7b40d086ba
1 changed files with 14 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/smt/smt_parallel.cpp
View file

@ -500,6 +500,20 @@ namespace smt {
} }
expr_ref_vector parallel::worker::get_split_atoms() { expr_ref_vector parallel::worker::get_split_atoms() {
#if false
for (bool_var v = 0; v < ctx->get_num_bool_vars(); ++v) {
if (ctx->get_assignment(v) != l_undef)
continue;
expr* e = ctx->bool_var2expr(v);
if (!e)
continue;
auto v_score = ctx->m_lit_scores[0][v] * ctx->m_lit_scores[1][v];
// if v_score is maximal then v is our split atom..
ctx->m_lit_scores[0][v] /= 2;
ctx->m_lit_scores[1][v] /= 2;
}
#endif
unsigned k = 2; unsigned k = 2;
auto candidates = ctx->m_pq_scores.get_heap(); auto candidates = ctx->m_pq_scores.get_heap();