From 5d3b515a5070859fa4566e6007a7b2f437089c6d Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 15 May 2018 12:36:54 -0700 Subject: [PATCH] Cleanup option names and default values --- src/muz/base/fixedpoint_params.pyg | 31 +++++++++++++++------------ src/muz/spacer/spacer_context.cpp | 14 ++++++------ src/muz/spacer/spacer_prop_solver.cpp | 8 +++---- 3 files changed, 28 insertions(+), 25 deletions(-) diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index 65d89e420..799e06fe6 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -166,7 +166,7 @@ def_module_params('fixedpoint', ('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.split_farkas_literals', BOOL, False, "Split Farkas literals"), + ('spacer.iuc.split_farkas_literals', BOOL, False, "Split Farkas literals"), ('spacer.native_mbp', BOOL, False, "Use native mbp of Z3"), ('spacer.eq_prop', BOOL, True, "Enable equality and bound propagation in arithmetic"), ('spacer.weak_abs', BOOL, True, "Weak abstraction"), @@ -179,23 +179,26 @@ def_module_params('fixedpoint', ('spacer.vs.recheck', BOOL, False, 're-check locally during benchmark dumping'), ('spacer.mbqi', BOOL, True, 'use model-based quantifier instantiation'), ('spacer.keep_proxy', BOOL, True, 'keep proxy variables (internal parameter)'), - ('spacer.instantiate', BOOL, True, 'instantiate quantified lemmas'), - ('spacer.qlemmas', BOOL, True, 'allow quantified lemmas in frames'), - ('spacer.iuc', UINT, 1, '0 = use old implementation of unsat-core-generation, 1 = use new implementation of IUC generation, 2 = use new implementation of IUC + min-cut optimization'), - ('spacer.iuc.arith', UINT, 2, '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, 3 = use additive IUC plugin'), - ('spacer.old_hyp_reducer', BOOL, False, 'use old hyp reducer instead of new implementation, for debugging only'), + ('spacer.q3.instantiate', BOOL, True, 'instantiate quantified lemmas'), + ('spacer.q3', BOOL, True, 'allow quantified lemmas in frames'), + ('spacer.iuc', UINT, 0, + '0 = use old implementation of unsat-core-generation, ' + + '1 = use new implementation of IUC generation, ' + + '2 = use new implementation of IUC + min-cut optimization'), + ('spacer.iuc.arith', UINT, 0, + '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.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.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.use_quant_generalizer', BOOL, False, 'use quantified lemma generalizer'), - ('spacer.quic_gen_normalize', BOOL, True, 'normalize cube before quantified generalization'), - ('spacer.share_lemmas', BOOL, False, "Share frame lemmas"), - ('spacer.share_invariants', BOOL, False, "Share invariants lemmas"), + ('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') )) - - - diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index f700ce83e..60f6b9a85 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -2026,8 +2026,8 @@ context::context(fixedpoint_params const& params, m_expanded_lvl(0), m_use_native_mbp(params.spacer_native_mbp ()), m_ground_cti (params.spacer_ground_cti ()), - m_instantiate (params.spacer_instantiate ()), - m_use_qlemmas (params.spacer_qlemmas ()), + m_instantiate (params.spacer_q3_instantiate ()), + m_use_qlemmas (params.spacer_q3()), m_weak_abs(params.spacer_weak_abs()), m_use_restarts(params.spacer_restarts()), m_restart_initial_threshold(params.spacer_restart_initial_threshold()), @@ -2303,11 +2303,11 @@ void context::init_lemma_generalizers(datalog::rule_set& rules) fparams.m_ng_lift_ite = LI_FULL; } - if (m_params.spacer_use_quant_generalizer()) { + if (m_params.spacer_q3_use_qgen()) { m_lemma_generalizers.push_back(alloc(lemma_bool_inductive_generalizer, *this, 0, true)); m_lemma_generalizers.push_back(alloc(lemma_quantifier_generalizer, *this, - m_params.spacer_quic_gen_normalize())); + m_params.spacer_q3_qgen_normalize())); } if (get_params().spacer_use_eqclass()) { @@ -3138,7 +3138,7 @@ lbool context::expand_node(pob& n) sanity_checker(lemma); ); - + TRACE("spacer", tout << "invariant state: " << (is_infty_level(lemma->level())?"(inductive)":"") << mk_pp(lemma->get_expr(), m) << "\n";); @@ -3649,8 +3649,8 @@ void context::new_lemma_eh(pred_transformer &pt, lemma *lem) { } if (!handle) return; - if ((is_infty_level(lem->level()) && m_params.spacer_share_invariants()) || - (!is_infty_level(lem->level()) && m_params.spacer_share_lemmas())) { + if ((is_infty_level(lem->level()) && m_params.spacer_p3_share_invariants()) || + (!is_infty_level(lem->level()) && m_params.spacer_p3_share_lemmas())) { expr_ref_vector args(m); for (unsigned i = 0; i < pt.sig_size(); ++i) { args.push_back(m.mk_const(pt.get_manager().o2n(pt.sig(i), 0))); diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp index d14cd6e91..9850f9e6e 100644 --- a/src/muz/spacer/spacer_prop_solver.cpp +++ b/src/muz/spacer/spacer_prop_solver.cpp @@ -62,12 +62,12 @@ prop_solver::prop_solver(manager& pm, fixedpoint_params const& p, symbol const& m_contexts[0] = alloc(spacer::itp_solver, *(m_solvers[0]), p.spacer_iuc(), p.spacer_iuc_arith(), - p.spacer_old_hyp_reducer(), - p.spacer_split_farkas_literals()); + p.spacer_iuc_old_hyp_reducer(), + p.spacer_iuc_split_farkas_literals()); m_contexts[1] = alloc(spacer::itp_solver, *(m_solvers[1]), p.spacer_iuc(), p.spacer_iuc_arith(), - p.spacer_old_hyp_reducer(), - p.spacer_split_farkas_literals()); + p.spacer_iuc_old_hyp_reducer(), + p.spacer_iuc_split_farkas_literals()); for (unsigned i = 0; i < 2; ++i) { m_contexts[i]->assert_expr(m_pm.get_background()); }