mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

refactor: add asserts, use case split strategy param

Browse source
This commit is contained in:
Murphy Berzish 2017-05-02 13:06:08 -04:00
parent 5b4792955d
commit a8d069ba46
4 changed files with 21 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smt/params/smt_params.cpp
View file

@ -32,7 +32,6 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_restart_factor = p.restart_factor();
m_case_split_strategy = static_cast<case_split_strategy>(p.case_split());
m_theory_case_split = p.theory_case_split();
m_theory_aware_branching = p.theory_aware_branching();
m_delay_units = p.delay_units();
m_delay_units_threshold = p.delay_units_threshold();
m_preprocess = _p.get_bool("preprocess", true); // hidden parameter

5
src/smt/params/smt_params.h
View file

@ -66,7 +66,8 @@ enum case_split_strategy {
CS_ACTIVITY_WITH_CACHE, // case split based on activity and cache the activity
CS_RELEVANCY, // case split based on relevancy
CS_RELEVANCY_ACTIVITY, // case split based on relevancy and activity
CS_RELEVANCY_GOAL // based on relevancy and the current goal
CS_RELEVANCY_GOAL, // based on relevancy and the current goal
CS_ACTIVITY_THEORY_AWARE_BRANCHING // activity-based case split, but theory solvers can manipulate activity
};
struct smt_params : public preprocessor_params,
@ -110,7 +111,6 @@ struct smt_params : public preprocessor_params,
unsigned m_rel_case_split_order;
bool m_lookahead_diseq;
bool m_theory_case_split;
bool m_theory_aware_branching;
// -----------------------------------
//
@ -242,7 +242,6 @@ struct smt_params : public preprocessor_params,
m_rel_case_split_order(0),
m_lookahead_diseq(false),
m_theory_case_split(false),
m_theory_aware_branching(false),
m_delay_units(false),
m_delay_units_threshold(32),
m_theory_resolve(false),

3
src/smt/params/smt_params_helper.pyg
View file

@ -11,7 +11,7 @@ def_module_params(module_name='smt',
('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences'),
('restart_strategy', UINT, 1, '0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic'),
('restart_factor', DOUBLE, 1.1, 'when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the currect restart threshold'),
('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal'),
('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal, 6 - activity-based case split with theory-aware branching activity'),
('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'),
('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ignored if delay_units is false'),
('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
@ -62,7 +62,6 @@ def_module_params(module_name='smt',
('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'),
('theory_case_split', BOOL, False, 'Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead.'),
('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'),
('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'),
('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),

39
src/smt/smt_case_split_queue.cpp
View file

@ -1164,9 +1164,10 @@ namespace smt {
virtual void pop_scope(unsigned num_scopes) {}
virtual void next_case_split(bool_var & next, lbool & phase) {
phase = l_undef;
if (m_context.get_random_value() < static_cast<int>(m_params.m_random_var_freq * random_gen::max_value())) {
int threshold = static_cast<int>(m_params.m_random_var_freq * random_gen::max_value());
SASSERT(threshold >= 0);
if (m_context.get_random_value() < threshold) {
SASSERT(m_context.get_num_b_internalized() > 0);
next = m_context.get_random_value() % m_context.get_num_b_internalized();
TRACE("random_split", tout << "next: " << next << " get_assignment(next): " << m_context.get_assignment(next) << "\n";);
if (m_context.get_assignment(next) == l_undef)
@ -1237,25 +1238,21 @@ namespace smt {
warning_msg("auto configuration (option AUTO_CONFIG) must be disabled to use option CASE_SPLIT=3, 4 or 5");
p.m_case_split_strategy = CS_ACTIVITY;
}
if (p.m_theory_aware_branching) {
// override
switch (p.m_case_split_strategy) {
case CS_ACTIVITY_DELAY_NEW:
return alloc(dact_case_split_queue, ctx, p);
case CS_ACTIVITY_WITH_CACHE:
return alloc(cact_case_split_queue, ctx, p);
case CS_RELEVANCY:
return alloc(rel_case_split_queue, ctx, p);
case CS_RELEVANCY_ACTIVITY:
return alloc(rel_act_case_split_queue, ctx, p);
case CS_RELEVANCY_GOAL:
return alloc(rel_goal_case_split_queue, ctx, p);
case CS_ACTIVITY_THEORY_AWARE_BRANCHING:
return alloc(theory_aware_branching_queue, ctx, p);
} else {
switch (p.m_case_split_strategy) {
case CS_ACTIVITY_DELAY_NEW:
return alloc(dact_case_split_queue, ctx, p);
case CS_ACTIVITY_WITH_CACHE:
return alloc(cact_case_split_queue, ctx, p);
case CS_RELEVANCY:
return alloc(rel_case_split_queue, ctx, p);
case CS_RELEVANCY_ACTIVITY:
return alloc(rel_act_case_split_queue, ctx, p);
case CS_RELEVANCY_GOAL:
return alloc(rel_goal_case_split_queue, ctx, p);
default:
return alloc(act_case_split_queue, ctx, p);
}
default:
return alloc(act_case_split_queue, ctx, p);
}
}