From d38879e478546151ee7cb46cd7a0583e678a043c Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 13 Jun 2018 13:35:27 -0700 Subject: [PATCH] Renamed spacer options --- src/muz/base/fixedpoint_params.pyg | 92 +++++++++----------------- src/muz/spacer/spacer_context.cpp | 51 +++++++------- src/muz/spacer/spacer_context.h | 14 ++-- src/muz/spacer/spacer_dl_interface.cpp | 2 +- src/muz/spacer/spacer_pdr.cpp | 2 +- 5 files changed, 67 insertions(+), 94 deletions(-) diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index f11e2faf9..7e92b0d2c 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -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'), + )) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 64d047d73..40c42015b 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -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 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(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) diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index fcd396a62..f3d00a857 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -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 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;} diff --git a/src/muz/spacer/spacer_dl_interface.cpp b/src/muz/spacer/spacer_dl_interface.cpp index cadbcfb0e..807e9b751 100644 --- a/src/muz/spacer/spacer_dl_interface.cpp +++ b/src/muz/spacer/spacer_dl_interface.cpp @@ -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()); } diff --git a/src/muz/spacer/spacer_pdr.cpp b/src/muz/spacer/spacer_pdr.cpp index 6b13e82f8..ad2b6200d 100644 --- a/src/muz/spacer/spacer_pdr.cpp +++ b/src/muz/spacer/spacer_pdr.cpp @@ -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) {