mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 17:01:55 +00:00
Code Activity

pop to search level

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-10 12:53:20 -07:00
parent 4d2338133f
commit a0214b944d
3 changed files with 13 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_parallel.cpp
View file

@ -991,6 +991,8 @@ namespace smt {
// auto candidates = ctx->m_pq_scores.get_heap();
std::vector<std::pair<double, expr*>> top_k; // will hold at most k elements
ctx->pop_to_search_lvl();
for (bool_var v = 0; v < ctx->get_num_bool_vars(); ++v) {
if (ctx->get_assignment(v) != l_undef)
continue;

14
src/smt/smt_parallel2.cpp
View file

@ -62,6 +62,7 @@ namespace smt {
#include <mutex>
#include <condition_variable>
#define SHARE_SEARCH_TREE 1
#define LOG_WORKER(lvl, s) IF_VERBOSE(lvl, verbose_stream() << "Worker " << id << s)
@ -73,9 +74,9 @@ namespace smt {
search_tree::node<cube_config>* node = nullptr;
expr_ref_vector cube(m);
while (true) {
collect_shared_clauses(m_g2l);
#if 0
#if SHARE_SEARCH_TREE
if (!b.get_cube(m_g2l, id, cube, node)) {
LOG_WORKER(1, " no more cubes\n");
return;
@ -84,6 +85,7 @@ namespace smt {
if (!get_cube(cube, node))
return;
#endif
collect_shared_clauses(m_g2l);
check_cube_start:
LOG_WORKER(1, " CUBE SIZE IN MAIN LOOP: " << cube.size() << "\n");
@ -101,10 +103,13 @@ namespace smt {
// return unprocessed cubes to the batch manager
// add a split literal to the batch manager.
// optionally process other cubes and delay sending back unprocessed cubes to batch manager.
if (m_config.m_max_cube_depth <= cube.size())
goto check_cube_start;
auto atom = get_split_atom();
if (!atom)
goto check_cube_start;
#if 0
#if SHARE_SEARCH_TREE
b.split(m_l2g, id, node, atom);
#else
split(node, atom);
@ -133,7 +138,7 @@ namespace smt {
b.report_assumption_used(m_l2g, e); // report assumptions used in unsat core, so they can be used in final core
LOG_WORKER(1, " found unsat cube\n");
#if 0
#if SHARE_SEARCH_TREE
b.backtrack(m_l2g, unsat_core, node);
#else
backtrack(unsat_core, node);
@ -208,6 +213,7 @@ namespace smt {
m_config.m_beam_search = pp.beam_search();
m_config.m_explicit_hardness = pp.explicit_hardness();
m_config.m_cubetree = pp.cubetree();
m_config.m_max_cube_depth = pp.max_cube_depth();
// don't share initial units
ctx->pop_to_base_lvl();

1
src/smt/smt_parallel2.h
View file

@ -130,6 +130,7 @@ namespace smt {
bool m_cube_initial_only = false;
unsigned m_max_greedy_cubes = 1000;
unsigned m_num_split_lits = 2;
unsigned m_max_cube_depth = 20;
bool m_backbone_detection = false;
bool m_iterative_deepening = false;
bool m_beam_search = false;