mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

rename to log_start for clarity

Browse source
This commit is contained in:
Jakob Rath 2023-08-03 10:25:32 +02:00
parent 6bbd68cdf1
commit e7e025a2fc
3 changed files with 6 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/polysat/polysat_params.pyg
View file

@ -4,7 +4,8 @@ def_module_params('polysat',
params=( params=(
('max_conflicts', UINT, UINT_MAX, "maximum number of conflicts before giving up"), ('max_conflicts', UINT, UINT_MAX, "maximum number of conflicts before giving up"),
('max_decisions', UINT, UINT_MAX, "maximum number of decisions before giving up"), ('max_decisions', UINT, UINT_MAX, "maximum number of decisions before giving up"),
('log', UINT, UINT_MAX, "polysat logging filter (enable logging in iteration N)"), # ('log', UINT, UINT_MAX, "polysat logging filter (TODO)"),
('log_start', UINT, UINT_MAX, "Enable logging on solver iteration N"),
('log_conflicts', BOOL, False, "log conflicts"), ('log_conflicts', BOOL, False, "log conflicts"),
('slicing.congruence', BOOL, False, "bitvector slicing: add virtual congruence terms"), ('slicing.congruence', BOOL, False, "bitvector slicing: add virtual congruence terms"),
) )

6
src/math/polysat/solver.cpp
View file

@ -80,12 +80,12 @@ namespace polysat {
m_params.append(p); m_params.append(p);
m_config.m_max_conflicts = pp.max_conflicts(); m_config.m_max_conflicts = pp.max_conflicts();
m_config.m_max_decisions = pp.max_decisions(); m_config.m_max_decisions = pp.max_decisions();
m_config.m_log_iteration = pp.log(); m_config.m_log_start = pp.log_start();
m_config.m_log_conflicts = pp.log_conflicts(); m_config.m_log_conflicts = pp.log_conflicts();
m_config.m_slicing_congruence = pp.slicing_congruence(); m_config.m_slicing_congruence = pp.slicing_congruence();
// TODO: log filter to enable/disable based on submodules // TODO: log filter to enable/disable based on submodules
if (m_config.m_log_iteration == 0) if (m_config.m_log_start == 0)
set_log_enabled(true); set_log_enabled(true);
else else
set_log_enabled(false); set_log_enabled(false);
@ -106,7 +106,7 @@ namespace polysat {
LOG("Starting"); LOG("Starting");
while (should_search()) { while (should_search()) {
m_stats.m_num_iterations++; m_stats.m_num_iterations++;
if (m_stats.m_num_iterations == config().m_log_iteration) if (m_stats.m_num_iterations == config().m_log_start)
set_log_enabled(true); set_log_enabled(true);
LOG_H1("Next solving loop iteration (#" << m_stats.m_num_iterations << ")"); LOG_H1("Next solving loop iteration (#" << m_stats.m_num_iterations << ")");
LOG("Free variables: " << m_free_pvars); LOG("Free variables: " << m_free_pvars);

2
src/math/polysat/solver.h
View file

@ -46,7 +46,7 @@ namespace polysat {
struct config_t { struct config_t {
uint64_t m_max_conflicts = std::numeric_limits<uint64_t>::max(); uint64_t m_max_conflicts = std::numeric_limits<uint64_t>::max();
uint64_t m_max_decisions = std::numeric_limits<uint64_t>::max(); uint64_t m_max_decisions = std::numeric_limits<uint64_t>::max();
unsigned m_log_iteration = UINT_MAX; unsigned m_log_start = UINT_MAX;
bool m_log_conflicts = false; bool m_log_conflicts = false;
bool m_slicing_congruence = false; bool m_slicing_congruence = false;
}; };