From 7b40d086ba4b7381e8b8e117133231d12f3fd989 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 22 Aug 2025 15:30:27 -0700 Subject: [PATCH] sketch scheme not using heap Signed-off-by: Nikolaj Bjorner --- src/smt/smt_parallel.cpp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index c78c8ad3b..47c1a5fd2 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -500,6 +500,20 @@ namespace smt { } 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; auto candidates = ctx->m_pq_scores.get_heap();