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

timeout backoff

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-09 16:02:01 -07:00
parent 9b2cb8a359
commit 9bab5ce7b7
3 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_parallel.cpp
View file

@ -501,7 +501,7 @@ namespace smt {
auto& cube = m_cubes.back(); auto& cube = m_cubes.back();
// print out the cubes in m_cubes // print out the cubes in m_cubes
for (auto& e : m_cubes) { for (auto& e : m_cubes) {
IF_VERBOSE(1, verbose_stream() << "Cube: " << e << "\n"); IF_VERBOSE(4, verbose_stream() << "Cube: " << e << "\n");
} }
expr_ref_vector l_cube(g2l.to()); expr_ref_vector l_cube(g2l.to());

3
src/smt/smt_parallel2.cpp
View file

@ -89,6 +89,7 @@ namespace smt {
switch (r) { switch (r) {
case l_undef: { case l_undef: {
update_max_thread_conflicts();
LOG_WORKER(1, " found undef cube\n"); LOG_WORKER(1, " found undef cube\n");
// return unprocessed cubes to the batch manager // return unprocessed cubes to the batch manager
// add a split literal to the batch manager. // add a split literal to the batch manager.
@ -283,7 +284,7 @@ namespace smt {
asms.push_back(atom); asms.push_back(atom);
lbool r = l_undef; lbool r = l_undef;
ctx->get_fparams().m_max_conflicts = std::min(cube.size() * 0 + m_config.m_threads_max_conflicts, m_config.m_max_conflicts); ctx->get_fparams().m_max_conflicts = std::min(m_config.m_threads_max_conflicts, m_config.m_max_conflicts);
IF_VERBOSE(1, verbose_stream() << " Checking cube\n" << bounded_pp_exprs(cube) << "with max_conflicts: " << ctx->get_fparams().m_max_conflicts << "\n";); IF_VERBOSE(1, verbose_stream() << " Checking cube\n" << bounded_pp_exprs(cube) << "with max_conflicts: " << ctx->get_fparams().m_max_conflicts << "\n";);
try { try {
r = ctx->check(asms.size(), asms.data()); r = ctx->check(asms.size(), asms.data());

5
src/smt/smt_parallel2.h
View file

@ -155,6 +155,11 @@ namespace smt {
lbool check_cube(expr_ref_vector const& cube); lbool check_cube(expr_ref_vector const& cube);
void share_units(ast_translation& l2g); void share_units(ast_translation& l2g);
void update_max_thread_conflicts() {
m_config.m_threads_max_conflicts = (unsigned)(m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts);
} // allow for backoff scheme of conflicts within the thread for cube timeouts.
public: public:
worker(unsigned id, parallel2& p, expr_ref_vector const& _asms); worker(unsigned id, parallel2& p, expr_ref_vector const& _asms);
void run(); void run();