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

add experimental parameters

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-08-14 13:51:50 -07:00
parent 0cb821ba30
commit be463eab6d
3 changed files with 13 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/params/CMakeLists.txt
View file

@ -21,6 +21,7 @@ z3_add_component(params
bv_rewriter_params.pyg
fpa_rewriter_params.pyg
fpa2bv_rewriter_params.pyg
smt_parallel_params.pyg
pattern_inference_params_helper.pyg
poly_rewriter_params.pyg
rewriter_params.pyg

7
src/params/smt_parallel_params.pyg Normal file
View file

@ -0,0 +1,7 @@
def_module_params('smt_parallel',
export=True,
description='Experimental parameters for parallel solving',
params=(
('share_units', BOOL, True, 'share units'),
('share_conflicts', BOOL, True, 'share conflicts'),
))

7
src/smt/smt_parallel.cpp
View file

@ -23,6 +23,7 @@ Author:
#include "ast/ast_translation.h"
#include "smt/smt_parallel.h"
#include "smt/smt_lookahead.h"
#include "params/smt_parallel_params.hpp"
#ifdef SINGLE_THREAD
@ -99,12 +100,14 @@ namespace smt {
b.report_assumption_used(l2g, e); // report assumptions used in unsat core, so they can be used in final core
IF_VERBOSE(1, verbose_stream() << "Worker " << id << " found unsat cube\n");
b.collect_clause(l2g, id, mk_not(mk_and(unsat_core)));
if (smt_parallel_params(p.ctx.m_params).share_conflicts())
b.collect_clause(l2g, id, mk_not(mk_and(unsat_core)));
break;
}
}
}
share_units(l2g);
if (smt_parallel_params(p.ctx.m_params).share_units())
share_units(l2g);
}
}