mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 18:29:23 +00:00
Code Activity

configuration parameter renaming

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-20 20:32:44 +03:00
parent f86702a49b
commit 0eb0406444
2 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_parallel.cpp
View file

@ -155,7 +155,7 @@ namespace smt {
unsigned sz = ctx->assigned_literals().size();
for (unsigned j = m_num_shared_units; j < sz; ++j) { // iterate only over new literals since last sync
literal lit = ctx->assigned_literals()[j];
if (!ctx->is_relevant(lit.var()) && m_config.m_relevant_units_only)
if (!ctx->is_relevant(lit.var()) && m_config.m_share_units_relevant_only)
continue;
if (m_config.m_share_units_initial_only && lit.var() >= m_num_initial_atoms) {

8
src/smt/smt_parallel.h
View file

@ -108,16 +108,16 @@ namespace smt {
class worker {
struct config {
unsigned m_threads_max_conflicts = 1000;
unsigned m_max_conflicts = 10000000;
bool m_relevant_units_only = true;
bool m_share_conflicts = true;
bool m_share_conflicts = false;
bool m_share_units = true;
double m_max_conflict_mul = 1.5;
bool m_share_units_relevant_only = true;
bool m_share_units_initial_only = true;
double m_max_conflict_mul = 1.5;
bool m_cube_initial_only = true;
bool m_inprocessing = true;
unsigned m_inprocessing_delay = 1;
unsigned m_max_cube_depth = 20;
unsigned m_max_conflicts = UINT_MAX;
};
using node = search_tree::node<cube_config>;