mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

parallel helper

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-28 13:51:20 -07:00
parent 8ba9d8c16a
commit 85c9d9ed27
4 changed files with 29 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/params/smt_parallel.pyg Normal file
View file

@ -0,0 +1,25 @@
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'),
('never_cube', BOOL, False, 'never cube'),
('frugal_cube_only', BOOL, False, 'only apply frugal cube strategy'),
('relevant_units_only', BOOL, True, 'only share relvant units'),
('max_conflict_mul', DOUBLE, 1.5, 'increment multiplier for max-conflicts'),
('share_units_initial_only', BOOL, True, 'share only initial Boolean atoms as units'),
('cube_initial_only', BOOL, False, 'cube only on initial Boolean atoms'),
('max_cube_depth', UINT, 20, 'maximum depth (size) of a cube to share'),
('max_greedy_cubes', UINT, 1000, 'maximum number of cube to greedily share before switching to frugal'),
('num_split_lits', UINT, 2, 'how many literals, k, we split on to create 2^k cubes'),
('depth_splitting_only', BOOL, False, 'only apply frugal cube strategy, and only on deepest (biggest) cubes from the batch manager'),
('backbone_detection', BOOL, False, 'apply backbone literal heuristic'),
('iterative_deepening', BOOL, False, 'deepen cubes based on iterative hardness cutoff heuristic'),
('beam_search', BOOL, False, 'use beam search with PQ to rank cubes given to threads'),
('explicit_hardness', BOOL, False, 'use explicit hardness metric for cube'),
('cubetree', BOOL, False, 'use cube tree data structure for storing cubes'),
('searchtree', BOOL, False, 'use search tree implementation (parallel2)'),
('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification'),
('inprocessing_delay', UINT, 0, 'number of undef before invoking simplification')
))

1
src/smt/smt_clause_proof.cpp
View file

@ -195,6 +195,7 @@ namespace smt {
if (m_on_clause_eh) {
// Encode status as an integer flag for simplicity.
unsigned st_code = 0;
IF_VERBOSE(0, if (status::assumption != st) verbose_stream() << "status " << st << "\n");
switch (st) {
case status::assumption: st_code = 1; break;
case status::lemma: st_code = 2; break;

2
src/smt/smt_context.cpp
View file

@ -4386,6 +4386,8 @@ namespace smt {
}
}
#endif
IF_VERBOSE(0, verbose_stream() << "(smt.learned-clause"; verbose_stream() << " :size " << num_lits;
verbose_stream() << " :conflicts " << m_num_conflicts << ")\n";);
mk_clause(num_lits, lits, js, CLS_LEARNED);
if (delay_forced_restart) {
SASSERT(num_lits == 1);

1
src/smt/theory_lra.cpp
View file

@ -3469,6 +3469,7 @@ public:
}
void set_conflict_or_lemma(literal_vector const& core, bool is_conflict) {
IF_VERBOSE(0, verbose_stream() << "set conflict or lemma " << core << "\n");
reset_evidence();
for (literal lit : core) {
m_core.push_back(lit);