mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

Renamed spacer options

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-13 13:35:27 -07:00
parent 81575fae7c
commit d38879e478
5 changed files with 67 additions and 94 deletions
Download patch file Download diff file Expand all files Collapse all files

92
src/muz/base/fixedpoint_params.pyg
View file

@ -56,43 +56,19 @@ def_module_params('fixedpoint',
"table columns, if it would have been empty otherwise"),
('datalog.subsumption', BOOL, True,
"if true, removes/filters predicates with total transitions"),
('pdr.bfs_model_search', BOOL, True,
"use BFS strategy for expanding model search"),
('pdr.farkas', BOOL, True,
"use lemma generator based on Farkas (for linear real arithmetic)"),
('generate_proof_trace', BOOL, False, "trace for 'sat' answer as proof object"),
('pdr.flexible_trace', BOOL, False,
"allow PDR generate long counter-examples " +
"by extending candidate trace within search area"),
('pdr.flexible_trace_depth', UINT, UINT_MAX,
'Controls the depth (below the current level) at which flexible trace can be applied'),
('pdr.use_model_generalizer', BOOL, False,
"use model for backwards propagation (instead of symbolic simulation)"),
('pdr.validate_result', BOOL, False,
('spacer.push_pob', BOOL, False, "push blocked pobs to higher level"),
('spacer.push_pob_max_depth', UINT, UINT_MAX,
'Maximum depth at which push_pob is enabled'),
('validate', BOOL, False,
"validate result (by proof checking or model checking)"),
('pdr.simplify_formulas_pre', BOOL, False,
"simplify derived formulas before inductive propagation"),
('pdr.simplify_formulas_post', BOOL, False,
"simplify derived formulas after inductive propagation"),
('pdr.use_multicore_generalizer', BOOL, False,
"extract multiple cores for blocking states"),
('pdr.use_inductive_generalizer', BOOL, True,
('spacer.simplify_lemmas_pre', BOOL, False,
"simplify derived lemmas before inductive propagation"),
('spacer.simplify_lemmas_post', BOOL, False,
"simplify derived lemmas after inductive propagation"),
('spacer.use_inductive_generalizer', BOOL, True,
"generalize lemmas using induction strengthening"),
('pdr.use_arith_inductive_generalizer', BOOL, False,
"generalize lemmas using arithmetic heuristics for induction strengthening"),
('pdr.use_convex_closure_generalizer', BOOL, False,
"generalize using convex closures of lemmas"),
('pdr.use_convex_interior_generalizer', BOOL, False,
"generalize using convex interiors of lemmas"),
('pdr.cache_mode', UINT, 0, "use no (0), symbolic (1) or explicit " +
"cache (2) for model search"),
('pdr.inductive_reachability_check', BOOL, False,
"assume negation of the cube on the previous level when " +
"checking for reachability (not only during cube weakening)"),
('pdr.max_num_contexts', UINT, 500, "maximal number of contexts to create"),
('pdr.try_minimize_core', BOOL, False,
"try to reduce core size (before inductive minimization)"),
('pdr.utvpi', BOOL, True, 'Enable UTVPI strategy'),
('spacer.max_num_contexts', UINT, 500, "maximal number of contexts to create"),
('print_fixedpoint_extensions', BOOL, True,
"use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, " +
"when printing rules"),
@ -126,11 +102,11 @@ def_module_params('fixedpoint',
('xform.compress_unbound', BOOL, True, "compress tails with unbound variables"),
('xform.fix_unbound_vars', BOOL, False, "fix unbound variables in tail"),
('xform.unfold_rules', UINT, 0,
"unfold rules statically using iterative squarring"),
"unfold rules statically using iterative squaring"),
('xform.slice', BOOL, True, "simplify clause set using slicing"),
('xform.karr', BOOL, False,
"Add linear invariants to clauses using Karr's method"),
('spacer.use_eqclass', BOOL, False, "Generalizes equalities to equivalence classes"),
('spacer.use_euf_gen', BOOL, False, 'Generalize lemmas and pobs using implied equalities'),
('xform.transform_arrays', BOOL, False,
"Rewrites arrays equalities and applies select over store"),
('xform.instantiate_arrays', BOOL, False,
@ -149,36 +125,31 @@ def_module_params('fixedpoint',
('xform.tail_simplifier_pve', BOOL, True, "propagate_variable_equivalences"),
('xform.subsumption_checker', BOOL, True, "Enable subsumption checker (no support for model conversion)"),
('xform.coi', BOOL, True, "use cone of influence simplification"),
('spacer.order_children', UINT, 0, 'SPACER: order of enqueuing children in non-linear rules : 0 (original), 1 (reverse)'),
('spacer.eager_reach_check', BOOL, True, 'SPACER: eagerly check if a query is reachable using reachability facts of predecessors'),
('spacer.order_children', UINT, 0, 'SPACER: order of enqueuing children in non-linear rules : 0 (original), 1 (reverse), 2 (random)'),
('spacer.use_lemma_as_cti', BOOL, False, 'SPACER: use a lemma instead of a CTI in flexible_trace'),
('spacer.reset_obligation_queue', BOOL, True, 'SPACER: reset obligation queue when entering a new level'),
('spacer.reset_pob_queue', BOOL, True, 'SPACER: reset pob obligation queue when entering a new level'),
('spacer.use_array_eq_generalizer', BOOL, True, 'SPACER: attempt to generalize lemmas with array equalities'),
('spacer.use_derivations', BOOL, True, 'SPACER: using derivation mechanism to cache intermediate results for non-linear rules'),
('xform.array_blast', BOOL, False, "try to eliminate local array terms using Ackermannization -- some array terms may remain"),
('xform.array_blast_full', BOOL, False, "eliminate all local array variables by QE"),
('spacer.skip_propagate', BOOL, False, "Skip propagate/pushing phase. Turns PDR into a BMC that returns either reachable or unknown"),
('spacer.propagate', BOOL, True, 'Enable propagate/pushing phase'),
('spacer.max_level', UINT, UINT_MAX, "Maximum level to explore"),
('spacer.elim_aux', BOOL, True, "Eliminate auxiliary variables in reachability facts"),
('spacer.blast_term_ite', BOOL, True, "Expand non-Boolean ite-terms"),
('spacer.nondet_tie_break', BOOL, False, "Break ties in obligation queue non-deterministically"),
('spacer.reach_dnf', BOOL, True, "Restrict reachability facts to DNF"),
('bmc.linear_unrolling_depth', UINT, UINT_MAX, "Maximal level to explore"),
('spacer.iuc.split_farkas_literals', BOOL, False, "Split Farkas literals"),
('spacer.native_mbp', BOOL, False, "Use native mbp of Z3"),
('spacer.native_mbp', BOOL, True, "Use native mbp of Z3"),
('spacer.eq_prop', BOOL, True, "Enable equality and bound propagation in arithmetic"),
('spacer.weak_abs', BOOL, True, "Weak abstraction"),
('spacer.restarts', BOOL, False, "Enable reseting obligation queue"),
('spacer.restart_initial_threshold', UINT, 10, "Intial threshold for restarts"),
('spacer.random_seed', UINT, 0, "Random seed to be used by SMT solver"),
('spacer.ground_cti', BOOL, True, "Require CTI to be ground"),
('spacer.vs.dump_benchmarks', BOOL, False, 'dump benchmarks in virtual solver'),
('spacer.vs.dump_min_time', DOUBLE, 5.0, 'min time to dump benchmark'),
('spacer.vs.recheck', BOOL, False, 're-check locally during benchmark dumping'),
('spacer.mbqi', BOOL, True, 'use model-based quantifier instantiation'),
('spacer.mbqi', BOOL, True, 'Enable mbqi'),
('spacer.keep_proxy', BOOL, True, 'keep proxy variables (internal parameter)'),
('spacer.q3.instantiate', BOOL, True, 'instantiate quantified lemmas'),
('spacer.q3', BOOL, True, 'allow quantified lemmas in frames'),
('spacer.q3', BOOL, True, 'Allow quantified lemmas in frames'),
('spacer.q3.instantiate', BOOL, True, 'Instantiate quantified lemmas'),
('spacer.iuc', UINT, 1,
'0 = use old implementation of unsat-core-generation, ' +
'1 = use new implementation of IUC generation, ' +
@ -187,21 +158,24 @@ def_module_params('fixedpoint',
'0 = use simple Farkas plugin, ' +
'1 = use simple Farkas plugin with constant from other partition (like old unsat-core-generation),' +
'2 = use Gaussian elimination optimization (broken), 3 = use additive IUC plugin'),
('spacer.iuc.old_hyp_reducer', BOOL, True, 'use old hyp reducer instead of new implementation, for debugging only'),
('spacer.lemma_sanity_check', BOOL, False, 'check during generalization whether lemma is actually correct'),
('spacer.reuse_pobs', BOOL, True, 'reuse POBs'),
('spacer.iuc.print_farkas_stats', BOOL, False, 'prints for each proof how many Farkas lemmas it contains and how many of these participate in the cut'),
('spacer.iuc.debug_proof', BOOL, False, 'prints proof used by unsat-core-learner for debugging purposes'),
('spacer.simplify_pob', BOOL, False, 'simplify POBs by removing redundant constraints'),
('spacer.iuc.old_hyp_reducer', BOOL, False, 'use old hyp reducer instead of new implementation, for debugging only'),
('spacer.validate_lemmas', BOOL, False, 'Validate each lemma after generalization'),
('spacer.reuse_pobs', BOOL, True, 'Reuse pobs'),
('spacer.ground_pobs', BOOL, True, 'Ground pobs by using values from a model'),
('spacer.iuc.print_farkas_stats', BOOL, False, 'prints for each proof how many Farkas lemmas it contains and how many of these participate in the cut (for debugging)'),
('spacer.iuc.debug_proof', BOOL, False, 'prints proof used by unsat-core-learner for debugging purposes (debugging)'),
('spacer.simplify_pob', BOOL, False, 'simplify pobs by removing redundant constraints'),
('spacer.q3.use_qgen', BOOL, False, 'use quantified lemma generalizer'),
('spacer.q3.qgen.normalize', BOOL, True, 'normalize cube before quantified generalization'),
('spacer.p3.share_lemmas', BOOL, False, 'Share frame lemmas'),
('spacer.p3.share_invariants', BOOL, False, "Share invariants lemmas"),
('spacer.from_level', UINT, 0, 'starting level to explore'),
('spacer.print_json', SYMBOL, '', 'print pobs tree in JSON format to a given file'),
('spacer.ctp', BOOL, False, 'enable counterexample-to-pushing technique'),
('spacer.use_inc_clause', BOOL, False, 'Use incremental clause to represent trans'),
('spacer.min_level', UINT, 0, 'Minimal level to explore'),
('spacer.print_json', SYMBOL, '', 'Print pobs tree in JSON format to a given file'),
('spacer.ctp', BOOL, True, 'Enable counterexample-to-pushing'),
('spacer.use_inc_clause', BOOL, True, 'Use incremental clause to represent trans'),
('spacer.dump_benchmarks', BOOL, False, 'Dump SMT queries as benchmarks'),
('spacer.dump_threshold', DOUBLE, 5.0, 'Threshold in seconds on dumping benchmarks'),
('spacer.gpdr', BOOL, False, 'Use GPDR solving strategy for non-linear CHC'),
('spacer.gpdr.bfs', BOOL, True, 'Use BFS exploration strategy for expanding model search'),
))

51
src/muz/spacer/spacer_context.cpp
View file

@ -82,7 +82,7 @@ void pob::set_post(expr* post) {
void pob::set_post(expr* post, app_ref_vector const &binding) {
normalize(post, m_post,
m_pt.get_context().simplify_pob(),
m_pt.get_context().use_eqclass());
m_pt.get_context().use_euf_gen());
m_binding.reset();
if (!binding.empty()) {m_binding.append(binding);}
@ -1590,13 +1590,12 @@ void pred_transformer::init_rules(decl2rel const& pts) {
if (not_inits.empty ()) {m_all_init = true;}
}
static bool is_all_non_null(app_ref_vector const& v)
{
for (unsigned i = 0; i < v.size(); ++i) {
if (!v[i]) { return false; }
}
#ifdef Z3DEBUG
static bool is_all_non_null(app_ref_vector const& apps) {
for (auto *a : apps) if (!a) return false;
return true;
}
#endif
void pred_transformer::init_rule(decl2rel const& pts, datalog::rule const& rule) {
scoped_watch _t_(m_initialize_watch);
@ -2196,7 +2195,7 @@ context::context(fixedpoint_params const& params,
ref<solver> pool2_base =
mk_smt_solver(m, params_ref::get_empty(), symbol::null);
unsigned max_num_contexts = params.pdr_max_num_contexts();
unsigned max_num_contexts = params.spacer_max_num_contexts();
m_pool0 = alloc(solver_pool, pool0_base.get(), max_num_contexts);
m_pool1 = alloc(solver_pool, pool1_base.get(), max_num_contexts);
m_pool2 = alloc(solver_pool, pool2_base.get(), max_num_contexts);
@ -2214,42 +2213,42 @@ void context::updt_params() {
m_random.set_seed(m_params.spacer_random_seed());
m_children_order = static_cast<spacer_children_order>(m_params.spacer_order_children());
m_simplify_pob = m_params.spacer_simplify_pob();
m_use_eqclass = m_params.spacer_use_eqclass();
m_use_euf_gen = m_params.spacer_use_euf_gen();
m_use_ctp = m_params.spacer_ctp();
m_use_inc_clause = m_params.spacer_use_inc_clause();
m_blast_term_ite = m_params.spacer_blast_term_ite();
m_reuse_pobs = m_params.spacer_reuse_pobs();
m_use_ind_gen = m_params.pdr_use_inductive_generalizer();
m_use_ind_gen = m_params.spacer_use_inductive_generalizer();
m_use_array_eq_gen = m_params.spacer_use_array_eq_generalizer();
m_check_lemmas = m_params.spacer_lemma_sanity_check();
m_validate_lemmas = m_params.spacer_validate_lemmas();
m_max_level = m_params.spacer_max_level ();
m_skip_propagate = m_params.spacer_skip_propagate ();
m_reset_obligation_queue = m_params.spacer_reset_obligation_queue();
m_flexible_trace = m_params.pdr_flexible_trace();
m_flexible_trace_depth = m_params.pdr_flexible_trace_depth();
m_use_propagate = m_params.spacer_propagate ();
m_reset_obligation_queue = m_params.spacer_reset_pob_queue();
m_push_pob = m_params.spacer_push_pob();
m_push_pob_max_depth = m_params.spacer_push_pob_max_depth();
m_use_lemma_as_pob = m_params.spacer_use_lemma_as_cti();
m_elim_aux = m_params.spacer_elim_aux();
m_reach_dnf = m_params.spacer_reach_dnf();
m_use_derivations = m_params.spacer_use_derivations();
m_validate_result = m_params.pdr_validate_result();
m_validate_result = m_params.validate();
m_use_eq_prop = m_params.spacer_eq_prop();
m_ground_pob = m_params.spacer_ground_cti();
m_ground_pob = m_params.spacer_ground_pobs();
m_q3_qgen = m_params.spacer_q3_use_qgen();
m_use_gpdr = m_params.spacer_gpdr();
m_simplify_formulas_pre = m_params.pdr_simplify_formulas_pre();
m_simplify_formulas_post = m_params.pdr_simplify_formulas_post();
m_simplify_formulas_pre = m_params.spacer_simplify_lemmas_pre();
m_simplify_formulas_post = m_params.spacer_simplify_lemmas_post();
m_use_native_mbp = m_params.spacer_native_mbp ();
m_instantiate = m_params.spacer_q3_instantiate ();
m_use_qlemmas = m_params.spacer_q3();
m_weak_abs = m_params.spacer_weak_abs();
m_use_restarts = m_params.spacer_restarts();
m_restart_initial_threshold = m_params.spacer_restart_initial_threshold();
m_pdr_bfs = m_params.spacer_gpdr_bfs();
if (m_use_gpdr) {
// set options to be compatible with GPDR
m_weak_abs = false;
m_flexible_trace = false;
m_push_pob = false;
m_use_qlemmas = false;
m_ground_pob = true;
m_reset_obligation_queue = false;
@ -2552,7 +2551,7 @@ void context::init_lemma_generalizers()
m_params.spacer_q3_qgen_normalize()));
}
if (use_eqclass()) {
if (m_use_euf_gen) {
m_lemma_generalizers.push_back (alloc(lemma_eq_generalizer, *this));
}
@ -2567,7 +2566,7 @@ void context::init_lemma_generalizers()
m_lemma_generalizers.push_back(alloc(lemma_array_eq_generalizer, *this));
}
if (m_check_lemmas) {
if (m_validate_lemmas) {
m_lemma_generalizers.push_back(alloc(lemma_sanity_checker, *this));
}
@ -2995,7 +2994,7 @@ lbool context::solve_core (unsigned from_lvl)
if (check_reachability()) { return l_true; }
if (lvl > 0 && !m_skip_propagate)
if (lvl > 0 && m_use_propagate)
if (propagate(m_expanded_lvl, lvl, UINT_MAX)) { dump_json(); return l_false; }
dump_json();
@ -3142,8 +3141,8 @@ bool context::check_reachability ()
/// returns true if the given pob can be re-scheduled
bool context::is_requeue(pob &n) {
if (!m_flexible_trace) {return false;}
unsigned max_depth = m_flexible_trace_depth;
if (!m_push_pob) {return false;}
unsigned max_depth = m_push_pob_max_depth;
return (n.level() >= m_pob_queue.max_level() ||
m_pob_queue.max_level() - n.level() <= max_depth);
}
@ -3309,7 +3308,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
unsigned num_reuse_reach = 0;
if (m_flexible_trace && n.pt().is_blocked(n, uses_level)) {
if (m_push_pob && n.pt().is_blocked(n, uses_level)) {
// if (!m_pob_queue.is_root (n)) n.close ();
IF_VERBOSE (1, verbose_stream () << " K "
<< std::fixed << std::setprecision(2)

14
src/muz/spacer/spacer_context.h
View file

@ -907,17 +907,17 @@ class context {
bool m_weak_abs;
bool m_use_restarts;
bool m_simplify_pob;
bool m_use_eqclass;
bool m_use_euf_gen;
bool m_use_ctp;
bool m_use_inc_clause;
bool m_blast_term_ite;
bool m_reuse_pobs;
bool m_use_ind_gen;
bool m_use_array_eq_gen;
bool m_check_lemmas;
bool m_skip_propagate;
bool m_validate_lemmas;
bool m_use_propagate;
bool m_reset_obligation_queue;
bool m_flexible_trace;
bool m_push_pob;
bool m_use_lemma_as_pob;
bool m_elim_aux;
bool m_reach_dnf;
@ -929,8 +929,8 @@ class context {
bool m_use_gpdr;
bool m_simplify_formulas_pre;
bool m_simplify_formulas_post;
unsigned m_flexible_trace_depth;
bool m_pdr_bfs;
unsigned m_push_pob_max_depth;
unsigned m_max_level;
unsigned m_restart_initial_threshold;
scoped_ptr_vector<spacer_callback> m_callbacks;
@ -1003,7 +1003,7 @@ public:
bool use_instantiate () {return m_instantiate;}
bool weak_abs() {return m_weak_abs;}
bool use_qlemmas () {return m_use_qlemmas;}
bool use_eqclass() { return m_use_eqclass;}
bool use_euf_gen() {return m_use_euf_gen;}
bool simplify_pob() {return m_simplify_pob;}
bool use_ctp() {return m_use_ctp;}
bool use_inc_clause() {return m_use_inc_clause;}

2
src/muz/spacer/spacer_dl_interface.cpp
View file

@ -164,7 +164,7 @@ lbool dl_interface::query(expr * query)
return l_false;
}
return m_context->solve(m_ctx.get_params().spacer_from_level());
return m_context->solve(m_ctx.get_params().spacer_min_level());
}

2
src/muz/spacer/spacer_pdr.cpp
View file

@ -230,7 +230,7 @@ lbool context::gpdr_solve_core() {
//if there is no query predicate, abort
if (!m_rels.find(m_query_pred, m_query)) { return l_false; }
model_search ms(true);
model_search ms(m_pdr_bfs);
unsigned lvl = 0;
unsigned max_level = m_max_level;
for (lvl = 0; lvl < max_level; ++lvl) {