From 29ec68284b554cb6bc507322d7e8b3a3ef0976e6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 1 Dec 2012 18:34:53 -0800 Subject: [PATCH] Added better error message when old parameter name is used Signed-off-by: Leonardo de Moura --- src/api/api_context.cpp | 1 - src/api/api_context.h | 1 - src/front_end_params/front_end_params.h | 4 --- src/util/gparams.cpp | 38 +++++++++++++++++++------ 4 files changed, 30 insertions(+), 14 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index ba8d2ae64..11fb28a02 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -90,7 +90,6 @@ namespace api { context::context(config_params * p, bool user_ref_count): m_params(p ? p->m_params : front_end_params()), - m_param_ini(m_params), m_user_ref_count(user_ref_count), m_manager(m_params.m_proof_mode, m_params.m_trace_stream), m_plugins(m_manager), diff --git a/src/api/api_context.h b/src/api/api_context.h index 3da506b54..76c601d60 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -53,7 +53,6 @@ namespace api { struct add_plugins { add_plugins(ast_manager & m); }; front_end_params m_params; - param_ini m_param_ini; bool m_user_ref_count; //!< if true, the user is responsible for managing referenc counters. ast_manager m_manager; add_plugins m_plugins; diff --git a/src/front_end_params/front_end_params.h b/src/front_end_params/front_end_params.h index 626f51a19..c3fa9fa95 100644 --- a/src/front_end_params/front_end_params.h +++ b/src/front_end_params/front_end_params.h @@ -41,11 +41,7 @@ struct front_end_params : public smt_params { m_memory_high_watermark(0), m_memory_max_size(0), m_proof_mode(PGM_DISABLED), -#if defined(SMTCOMP) || defined(_EXTERNAL_RELEASE) m_auto_config(true), -#else - m_auto_config(false), -#endif m_debug_ref_count(false), m_trace(false), m_trace_file_name("z3.log"), diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 426789bb4..e7b2a52eb 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -21,6 +21,19 @@ Notes: extern void gparams_register_modules(); +char const * g_old_params_names[] = { + "arith_adaptive","arith_adaptive_assertion_threshold","arith_adaptive_gcd","arith_adaptive_propagation_threshold","arith_add_binary_bounds","arith_blands_rule_threshold","arith_branch_cut_ratio","arith_dump_lemmas","arith_eager_eq_axioms","arith_eager_gcd","arith_eq_bounds","arith_euclidean_solver","arith_expand_eqs","arith_force_simplex","arith_gcd_test","arith_ignore_int","arith_lazy_adapter","arith_lazy_pivoting","arith_max_lemma_size","arith_process_all_eqs","arith_propagate_eqs","arith_propagation_mode","arith_propagation_threshold","arith_prop_strategy","arith_random_initial_value","arith_random_lower","arith_random_seed","arith_random_upper","arith_reflect","arith_skip_big_coeffs","arith_small_lemma_size","arith_solver","arith_stronger_lemmas","array_always_prop_upward","array_canonize","array_cg","array_delay_exp_axiom","array_extensional","array_laziness","array_lazy_ieq","array_lazy_ieq_delay","array_solver","array_weak","async_commands","at_labels_cex","auto_config","bb_eager","bb_ext_gates","bb_quantifiers","bin_clauses","bit2int","bv2int_distribute","bv_blast_max_size","bv_cc","bv_enable_int2bv_propagation","bv_lazy_le","bv_max_sharing","bv_reflect","bv_solver","case_split","check_at_labels","check_proof","cnf_factor","cnf_mode","context_simplifier","dack","dack_eq","dack_factor","dack_gc","dack_gc_inv_decay","dack_threshold","default_qid","default_table","default_table_checked","delay_units","delay_units_threshold","der","display_config","display_dot_proof","display_error_for_visual_studio","display_features","display_proof","display_unsat_core","distribute_forall","dt_lazy_splits","dump_goal_as_smt","elim_and","elim_bounds","elim_nlarith_quantifiers","elim_quantifiers","elim_term_ite","ematching","engine","eq_propagation","hi_div0","ignore_bad_patterns","ignore_setparameter","instruction_max","inst_gen","interactive","internalizer_nnf","lemma_gc_factor","lemma_gc_half","lemma_gc_initial","lemma_gc_new_clause_activity","lemma_gc_new_clause_relevancy","lemma_gc_new_old_ratio","lemma_gc_old_clause_activity","lemma_gc_old_clause_relevancy","lemma_gc_strategy","lift_ite","lookahead_diseq","macro_finder","max_conflicts","max_counterexamples","mbqi","mbqi_force_template","mbqi_max_cexs","mbqi_max_cexs_incr","mbqi_max_iterations","mbqi_trace","minimize_lemmas","model","model_compact","model_completion","model_display_arg_sort","model_hide_unused_partitions","model_on_final_check","model_on_timeout","model_partial","model_v1","model_v2","model_validate","new_core2th_eq","ng_lift_ite","nl_arith","nl_arith_branching","nl_arith_gb","nl_arith_gb_eqs","nl_arith_gb_perturbate","nl_arith_gb_threshold","nl_arith_max_degree","nl_arith_rounds","nnf_factor","nnf_ignore_labels","nnf_mode","nnf_sk_hack","order","order_var_weight","order_weights","phase_selection","pi_arith","pi_arith_weight","pi_avoid_skolems","pi_block_looop_patterns","pi_max_multi_patterns","pi_non_nested_arith_weight","pi_nopat_weight","pi_pull_quantifiers","pi_use_database","pi_warnings","pp_bounded","pp_bv_literals","pp_bv_neg","pp_decimal","pp_decimal_precision","pp_fixed_indent","pp_flat_assoc","pp_max_depth","pp_max_indent","pp_max_num_lines","pp_max_ribbon","pp_max_width","pp_min_alias_size","pp_simplify_implies","pp_single_line","precedence","precedence_gen","pre_demodulator","pre_simplifier","pre_simplify_expr","profile_res_sub","progress_sampling_freq","proof_mode","propagate_booleans","propagate_values","pull_cheap_ite_trees","pull_nested_quantifiers","qi_conservative_final_check","qi_cost","qi_eager_threshold","qi_lazy_instantiation","qi_lazy_quick_checker","qi_lazy_threshold","qi_max_eager_multi_patterns","qi_max_instances","qi_max_lazy_multi_pattern_matching","qi_new_gen","qi_profile","qi_profile_freq","qi_promote_unsat","qi_quick_checker","quasi_macros","random_case_split_freq","random_initial_activity","random_seed","recent_lemma_threshold","reduce_args","refine_inj_axiom","relevancy","relevancy_lemma","rel_case_split_order","restart_adaptive","restart_agility_threshold","restart_factor","restart_initial","restart_strategy","restricted_quasi_macros","simplify_clauses","smtlib2_compliant","smtlib_category","smtlib_dump_lemmas","smtlib_logic","smtlib_source_info","smtlib_trace_path","soft_timeout","solver","spc_bs","spc_es","spc_factor_subsumption_index_opt","spc_initial_subsumption_index_opt","spc_max_subsumption_index_features","spc_min_func_freq_subsumption_index","spc_num_iterations","spc_trace","statistics","strong_context_simplifier","tick","trace","trace_file_name","type_check","user_theory_persist_axioms","user_theory_preprocess_axioms","verbose","warning","well_sorted_check","z3_solver_ll_pp","z3_solver_smt_pp", 0 }; + +bool is_old_param_name(symbol const & name) { + char const * const * it = g_old_params_names; + while (*it) { + if (name == *it) + return true; + it++; + } + return false; +} + struct gparams::imp { dictionary m_module_param_descrs; param_descrs m_param_descrs; @@ -120,14 +133,26 @@ public: } } + void throw_unknown_parameter(symbol const & param_name, symbol const & mod_name) { + if (mod_name == symbol::null) { + if (is_old_param_name(param_name)) { + throw exception("unknown parameter '%s', this is an old parameter name, invoke 'z3 -ps' to obtain the new parameter list", + param_name.bare_str()); + } + else { + throw exception("unknown parameter '%s'", param_name.bare_str()); + } + } + else { + throw exception("unknown parameter '%s' at module '%s'", param_name.bare_str(), mod_name.bare_str()); + } + } + void set(param_descrs const & d, symbol const & param_name, char const * value, symbol const & mod_name) { param_kind k = d.get_kind(param_name); params_ref & ps = get_params(mod_name); if (k == CPK_INVALID) { - if (mod_name == symbol::null) - throw exception("unknown parameter '%s'", param_name.bare_str()); - else - throw exception("unknown parameter '%s' at module '%s'", param_name.bare_str(), mod_name.bare_str()); + throw_unknown_parameter(param_name, mod_name); } else if (k == CPK_UINT) { long val = strtol(value, 0, 10); @@ -200,10 +225,7 @@ public: std::string get_default(param_descrs const & d, symbol const & p, symbol const & m) { if (!d.contains(p)) { - if (m == symbol::null) - throw exception("unknown parameter '%s'", p.bare_str()); - else - throw exception("unknown parameter '%s' at module '%s'", p.bare_str(), m.bare_str()); + throw_unknown_parameter(p, m); } char const * r = d.get_default(p); if (r == 0)