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

updates

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-18 14:54:36 -07:00
parent b1ed1ef7c2
commit f12d751007
2 changed files with 15 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/smt/smt_parallel.cpp
View file

@ -569,16 +569,6 @@ namespace smt {
void parallel::batch_manager::initialize() { void parallel::batch_manager::initialize() {
m_state = state::is_running; m_state = state::is_running;
m_search_tree.reset(); m_search_tree.reset();
#if 0
smt_parallel_params sp(p.ctx.m_params);
m_config.m_max_cube_depth = sp.max_cube_depth();
m_config.m_frugal_cube_only = sp.frugal_cube_only();
m_config.m_never_cube = sp.never_cube();
m_config.m_depth_splitting_only = sp.depth_splitting_only();
m_config.m_iterative_deepening = sp.iterative_deepening();
m_config.m_beam_search = sp.beam_search();
m_config.m_cubetree = sp.cubetree();
#endif
} }
void parallel::batch_manager::collect_statistics(::statistics& st) const { void parallel::batch_manager::collect_statistics(::statistics& st) const {
@ -595,19 +585,25 @@ namespace smt {
struct scoped_clear { struct scoped_clear {
parallel& p; parallel& p;
scoped_clear(parallel& p) : p(p) {} scoped_clear(parallel& p) : p(p) {}
~scoped_clear() { p.m_workers.reset(); p.m_assumptions_used.reset(); } ~scoped_clear() {
p.m_workers.reset();
p.m_assumptions_used.reset();
p.m_assumptions.reset();
}
}; };
scoped_clear clear(*this); scoped_clear clear(*this);
{ {
m_batch_manager.initialize(); m_batch_manager.initialize();
m_workers.reset(); m_workers.reset();
for (auto e : asms)
m_assumptions.insert(e);
scoped_limits sl(m.limit()); scoped_limits sl(m.limit());
flet<unsigned> _nt(ctx.m_fparams.m_threads, 1); flet<unsigned> _nt(ctx.m_fparams.m_threads, 1);
SASSERT(num_threads > 1); SASSERT(num_threads > 1);
for (unsigned i = 0; i < num_threads; ++i) for (unsigned i = 0; i < num_threads; ++i)
m_workers.push_back(alloc(worker, i, *this, asms)); // i.e. "new worker(i, *this, asms)" m_workers.push_back(alloc(worker, i, *this, asms));
for (auto w : m_workers) for (auto w : m_workers)
sl.push_child(&(w->limit())); sl.push_child(&(w->limit()));

31
src/smt/smt_parallel.h
View file

@ -21,9 +21,7 @@ Revision History:
#include "smt/smt_context.h" #include "smt/smt_context.h"
#include "util/search_tree.h" #include "util/search_tree.h"
#include <thread> #include <thread>
#include <condition_variable>
#include <mutex> #include <mutex>
#include <condition_variable>
namespace smt { namespace smt {
@ -51,15 +49,6 @@ namespace smt {
is_exception_msg, is_exception_msg,
is_exception_code is_exception_code
}; };
struct config {
unsigned m_max_cube_depth = 20;
bool m_frugal_cube_only = false;
bool m_never_cube = false;
bool m_depth_splitting_only = false;
bool m_iterative_deepening = false;
bool m_beam_search = false;
bool m_cubetree = false;
};
struct stats { struct stats {
unsigned m_max_cube_depth = 0; unsigned m_max_cube_depth = 0;
unsigned m_num_cubes = 0; unsigned m_num_cubes = 0;
@ -70,7 +59,6 @@ namespace smt {
parallel& p; parallel& p;
std::mutex mux; std::mutex mux;
state m_state = state::is_running; state m_state = state::is_running;
config m_config;
stats m_stats; stats m_stats;
using node = search_tree::node<cube_config>; using node = search_tree::node<cube_config>;
search_tree::tree<cube_config> m_search_tree; search_tree::tree<cube_config> m_search_tree;
@ -90,7 +78,7 @@ namespace smt {
void init_parameters_state(); void init_parameters_state();
bool is_assumption(expr* e) const { bool is_assumption(expr* e) const {
return false; // m_assumptions_used.contains(e); return p.m_assumptions.contains(e);
} }
public: public:
@ -120,22 +108,14 @@ namespace smt {
unsigned m_threads_max_conflicts = 1000; unsigned m_threads_max_conflicts = 1000;
unsigned m_max_conflicts = 10000000; unsigned m_max_conflicts = 10000000;
bool m_relevant_units_only = true; bool m_relevant_units_only = true;
bool m_never_cube = false;
bool m_share_conflicts = true; bool m_share_conflicts = true;
bool m_share_units = true; bool m_share_units = true;
double m_max_conflict_mul = 1.5; double m_max_conflict_mul = 1.5;
bool m_share_units_initial_only = false; bool m_share_units_initial_only = true;
bool m_cube_initial_only = false; bool m_cube_initial_only = true;
unsigned m_max_greedy_cubes = 1000; bool m_inprocessing = true;
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;
bool m_explicit_hardness = false;
bool m_cubetree = false;
bool m_inprocessing = false;
unsigned m_inprocessing_delay = 0; unsigned m_inprocessing_delay = 0;
unsigned m_max_cube_depth = 20;
}; };
using node = search_tree::node<cube_config>; using node = search_tree::node<cube_config>;
@ -187,6 +167,7 @@ namespace smt {
}; };
obj_hashtable<expr> m_assumptions_used; // assumptions used in unsat cores, to be used in final core obj_hashtable<expr> m_assumptions_used; // assumptions used in unsat cores, to be used in final core
obj_hashtable<expr> m_assumptions; // all assumptions
batch_manager m_batch_manager; batch_manager m_batch_manager;
scoped_ptr_vector<worker> m_workers; scoped_ptr_vector<worker> m_workers;