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

configuration update to SAT solver on creation time. Adding random_seed to sat parameters to enable command-line and module mode to work at the level of sat solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-26 16:42:11 -07:00
parent 9412890c63
commit e57e5328ce
4 changed files with 8 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/sat/sat_config.cpp
View file

@ -68,7 +68,10 @@ namespace sat {
m_restart_factor = p.restart_factor(); m_restart_factor = p.restart_factor();
m_random_freq = p.random_freq(); m_random_freq = p.random_freq();
m_random_seed = p.random_seed();
if (m_random_seed == 0)
m_random_seed = _p.get_uint("random_seed", 0);
m_burst_search = p.burst_search(); m_burst_search = p.burst_search();
m_max_conflicts = p.max_conflicts(); m_max_conflicts = p.max_conflicts();

1
src/sat/sat_config.h
View file

@ -53,6 +53,7 @@ namespace sat {
unsigned m_restart_initial; unsigned m_restart_initial;
double m_restart_factor; // for geometric case double m_restart_factor; // for geometric case
double m_random_freq; double m_random_freq;
unsigned m_random_seed;
unsigned m_burst_search; unsigned m_burst_search;
unsigned m_max_conflicts; unsigned m_max_conflicts;

1
src/sat/sat_params.pyg
View file

@ -9,6 +9,7 @@ def_module_params('sat',
('restart.initial', UINT, 100, 'initial restart (number of conflicts)'), ('restart.initial', UINT, 100, 'initial restart (number of conflicts)'),
('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'), ('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'),
('random_freq', DOUBLE, 0.01, 'frequency of random case splits'), ('random_freq', DOUBLE, 0.01, 'frequency of random case splits'),
('random_seed', UINT, 0, 'random seed'),
('burst_search', UINT, 100, 'number of conflicts before first global simplification'), ('burst_search', UINT, 100, 'number of conflicts before first global simplification'),
('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts'), ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts'),
('gc', SYMBOL, 'glue_psm', 'garbage collection strategy: psm, glue, glue_psm, dyn_psm'), ('gc', SYMBOL, 'glue_psm', 'garbage collection strategy: psm, glue, glue_psm, dyn_psm'),

4
src/sat/sat_solver.cpp
View file

@ -46,7 +46,7 @@ namespace sat {
m_qhead(0), m_qhead(0),
m_scope_lvl(0), m_scope_lvl(0),
m_params(p) { m_params(p) {
m_config.updt_params(p); updt_params(p);
} }
solver::~solver() { solver::~solver() {
@ -1972,7 +1972,7 @@ namespace sat {
m_asymm_branch.updt_params(p); m_asymm_branch.updt_params(p);
m_probing.updt_params(p); m_probing.updt_params(p);
m_scc.updt_params(p); m_scc.updt_params(p);
m_rand.set_seed(p.get_uint("random_seed", 0)); m_rand.set_seed(m_config.m_random_seed);
} }
void solver::collect_param_descrs(param_descrs & d) { void solver::collect_param_descrs(param_descrs & d) {