mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

Added facilities for dumping smt_params for debugging purposes

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-06-23 19:31:00 +01:00
parent fad1dffbf0
commit 8bde7b8a4c
24 changed files with 300 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ast/pattern/pattern_inference_params.cpp
View file

@ -30,3 +30,18 @@ void pattern_inference_params::updt_params(params_ref const & _p) {
m_pi_pull_quantifiers = p.pull_quantifiers();
m_pi_warnings = p.warnings();
}
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
void pattern_inference_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_pi_max_multi_patterns);
DISPLAY_PARAM(m_pi_block_loop_patterns);
DISPLAY_PARAM(m_pi_arith);
DISPLAY_PARAM(m_pi_use_database);
DISPLAY_PARAM(m_pi_arith_weight);
DISPLAY_PARAM(m_pi_non_nested_arith_weight);
DISPLAY_PARAM(m_pi_pull_quantifiers);
DISPLAY_PARAM(m_pi_nopat_weight);
DISPLAY_PARAM(m_pi_avoid_skolems);
DISPLAY_PARAM(m_pi_warnings);
}

2
src/ast/pattern/pattern_inference_params.h
View file

@ -46,6 +46,8 @@ struct pattern_inference_params {
}
void updt_params(params_ref const & _p);
void display(std::ostream & out) const;
};
#endif /* PATTERN_INFERENCE_PARAMS_H_ */

7
src/ast/rewriter/bit_blaster/bit_blaster_params.h
View file

@ -22,7 +22,7 @@ Revision History:
struct bit_blaster_params {
bool m_bb_ext_gates;
bool m_bb_quantifiers;
bit_blaster_params():
bit_blaster_params() :
m_bb_ext_gates(false),
m_bb_quantifiers(false) {
}
@ -32,6 +32,11 @@ struct bit_blaster_params {
p.register_bool_param("bb_quantifiers", m_bb_quantifiers, "convert bit-vectors to Booleans in quantifiers");
}
#endif
void display(std::ostream & out) const {
out << "m_bb_ext_gates=" << m_bb_ext_gates << std::endl;
out << "m_bb_quantifiers=" << m_bb_quantifiers << std::endl;
}
};
#endif /* BIT_BLASTER_PARAMS_H_ */

7
src/ast/simplifier/arith_simplifier_params.cpp
View file

@ -24,3 +24,10 @@ void arith_simplifier_params::updt_params(params_ref const & _p) {
m_arith_expand_eqs = p.arith_expand_eqs();
m_arith_process_all_eqs = p.arith_process_all_eqs();
}
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
void arith_simplifier_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_arith_expand_eqs);
DISPLAY_PARAM(m_arith_process_all_eqs);
}

2
src/ast/simplifier/arith_simplifier_params.h
View file

@ -30,6 +30,8 @@ struct arith_simplifier_params {
}
void updt_params(params_ref const & _p);
void display(std::ostream & out) const;
};
#endif /* ARITH_SIMPLIFIER_PARAMS_H_ */

7
src/ast/simplifier/bv_simplifier_params.cpp
View file

@ -27,3 +27,10 @@ void bv_simplifier_params::updt_params(params_ref const & _p) {
m_bv2int_distribute = p.bv_bv2int_distribute();
}
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
void bv_simplifier_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_hi_div0);
DISPLAY_PARAM(m_bv2int_distribute);
}

2
src/ast/simplifier/bv_simplifier_params.h
View file

@ -30,6 +30,8 @@ struct bv_simplifier_params {
}
void updt_params(params_ref const & _p);
void display(std::ostream & out) const;
};
#endif /* BV_SIMPLIFIER_PARAMS_H_ */

11
src/smt/params/dyn_ack_params.cpp
View file

@ -28,3 +28,14 @@ void dyn_ack_params::updt_params(params_ref const & _p) {
m_dack_gc = p.dack_gc();
m_dack_gc_inv_decay = p.dack_gc_inv_decay();
}
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
void dyn_ack_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_dack);
DISPLAY_PARAM(m_dack_eq);
DISPLAY_PARAM(m_dack_factor);
DISPLAY_PARAM(m_dack_threshold);
DISPLAY_PARAM(m_dack_gc);
DISPLAY_PARAM(m_dack_gc_inv_decay);
}

2
src/smt/params/dyn_ack_params.h
View file

@ -47,6 +47,8 @@ public:
}
void updt_params(params_ref const & _p);
void display(std::ostream & out) const;
};

30
src/smt/params/preprocessor_params.cpp
View file

@ -32,3 +32,33 @@ void preprocessor_params::updt_params(params_ref const & p) {
arith_simplifier_params::updt_params(p);
updt_local_params(p);
}
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
void preprocessor_params::display(std::ostream & out) const {
pattern_inference_params::display(out);
bit_blaster_params::display(out);
bv_simplifier_params::display(out);
arith_simplifier_params::display(out);
DISPLAY_PARAM(m_lift_ite);
DISPLAY_PARAM(m_ng_lift_ite);
DISPLAY_PARAM(m_pull_cheap_ite_trees);
DISPLAY_PARAM(m_pull_nested_quantifiers);
DISPLAY_PARAM(m_eliminate_term_ite);
DISPLAY_PARAM(m_eliminate_and);
DISPLAY_PARAM(m_macro_finder);
DISPLAY_PARAM(m_propagate_values);
DISPLAY_PARAM(m_propagate_booleans);
DISPLAY_PARAM(m_refine_inj_axiom);
DISPLAY_PARAM(m_eliminate_bounds);
DISPLAY_PARAM(m_simplify_bit2int);
DISPLAY_PARAM(m_nnf_cnf);
DISPLAY_PARAM(m_distribute_forall);
DISPLAY_PARAM(m_reduce_args);
DISPLAY_PARAM(m_quasi_macros);
DISPLAY_PARAM(m_restricted_quasi_macros);
DISPLAY_PARAM(m_max_bv_sharing);
DISPLAY_PARAM(m_pre_simplifier);
DISPLAY_PARAM(m_nlquant_elim);
}

2
src/smt/params/preprocessor_params.h
View file

@ -83,6 +83,8 @@ public:
void updt_local_params(params_ref const & p);
void updt_params(params_ref const & p);
void display(std::ostream & out) const;
};
#endif /* PREPROCESSOR_PARAMS_H_ */

27
src/smt/params/qi_params.cpp
View file

@ -36,3 +36,30 @@ void qi_params::updt_params(params_ref const & _p) {
m_qi_cost = p.qi_cost();
m_qi_max_eager_multipatterns = p.qi_max_multi_patterns();
}
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
void qi_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_qi_ematching);
DISPLAY_PARAM(m_qi_cost);
DISPLAY_PARAM(m_qi_new_gen);
DISPLAY_PARAM(m_qi_eager_threshold);
DISPLAY_PARAM(m_qi_lazy_threshold);
DISPLAY_PARAM(m_qi_max_eager_multipatterns);
DISPLAY_PARAM(m_qi_max_lazy_multipattern_matching);
DISPLAY_PARAM(m_qi_profile);
DISPLAY_PARAM(m_qi_profile_freq);
DISPLAY_PARAM(m_qi_quick_checker);
DISPLAY_PARAM(m_qi_lazy_quick_checker);
DISPLAY_PARAM(m_qi_promote_unsat);
DISPLAY_PARAM(m_qi_max_instances);
DISPLAY_PARAM(m_qi_lazy_instantiation);
DISPLAY_PARAM(m_qi_conservative_final_check);
DISPLAY_PARAM(m_mbqi);
DISPLAY_PARAM(m_mbqi_max_cexs);
DISPLAY_PARAM(m_mbqi_max_cexs_incr);
DISPLAY_PARAM(m_mbqi_max_iterations);
DISPLAY_PARAM(m_mbqi_trace);
DISPLAY_PARAM(m_mbqi_force_template);
DISPLAY_PARAM(m_mbqi_id);
}

4
src/smt/params/qi_params.h
View file

@ -98,13 +98,15 @@ struct qi_params {
m_mbqi_max_cexs_incr(1),
m_mbqi_max_iterations(1000),
m_mbqi_trace(false),
m_mbqi_force_template(10),
m_mbqi_force_template(10),
m_mbqi_id(0)
{
updt_params(p);
}
void updt_params(params_ref const & p);
void display(std::ostream & out) const;
};
#endif /* QI_PARAMS_H_ */

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

@ -63,3 +63,96 @@ void smt_params::updt_params(context_params const & p) {
m_auto_config = p.m_auto_config;
m_model = p.m_model;
}
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
void smt_params::display(std::ostream & out) const {
preprocessor_params::display(out);
dyn_ack_params::display(out);
qi_params::display(out);
theory_arith_params::display(out);
theory_array_params::display(out);
theory_bv_params::display(out);
theory_pb_params::display(out);
theory_datatype_params::display(out);
DISPLAY_PARAM(m_display_proof);
DISPLAY_PARAM(m_display_dot_proof);
DISPLAY_PARAM(m_display_unsat_core);
DISPLAY_PARAM(m_check_proof);
DISPLAY_PARAM(m_eq_propagation);
DISPLAY_PARAM(m_binary_clause_opt);
DISPLAY_PARAM(m_relevancy_lvl);
DISPLAY_PARAM(m_relevancy_lemma);
DISPLAY_PARAM(m_random_seed);
DISPLAY_PARAM(m_random_var_freq);
DISPLAY_PARAM(m_inv_decay);
DISPLAY_PARAM(m_clause_decay);
DISPLAY_PARAM(m_random_initial_activity);
DISPLAY_PARAM(m_phase_selection);
DISPLAY_PARAM(m_phase_caching_on);
DISPLAY_PARAM(m_phase_caching_off);
DISPLAY_PARAM(m_minimize_lemmas);
DISPLAY_PARAM(m_max_conflicts);
DISPLAY_PARAM(m_simplify_clauses);
DISPLAY_PARAM(m_tick);
DISPLAY_PARAM(m_display_features);
DISPLAY_PARAM(m_new_core2th_eq);
DISPLAY_PARAM(m_ematching);
DISPLAY_PARAM(m_case_split_strategy);
DISPLAY_PARAM(m_rel_case_split_order);
DISPLAY_PARAM(m_lookahead_diseq);
DISPLAY_PARAM(m_delay_units);
DISPLAY_PARAM(m_delay_units_threshold);
DISPLAY_PARAM(m_theory_resolve);
DISPLAY_PARAM(m_restart_strategy);
DISPLAY_PARAM(m_restart_initial);
DISPLAY_PARAM(m_restart_factor);
DISPLAY_PARAM(m_restart_adaptive);
DISPLAY_PARAM(m_agility_factor);
DISPLAY_PARAM(m_restart_agility_threshold);
DISPLAY_PARAM(m_lemma_gc_strategy);
DISPLAY_PARAM(m_lemma_gc_half);
DISPLAY_PARAM(m_recent_lemmas_size);
DISPLAY_PARAM(m_lemma_gc_initial);
DISPLAY_PARAM(m_lemma_gc_factor);
DISPLAY_PARAM(m_new_old_ratio);
DISPLAY_PARAM(m_new_clause_activity);
DISPLAY_PARAM(m_old_clause_activity);
DISPLAY_PARAM(m_new_clause_relevancy);
DISPLAY_PARAM(m_old_clause_relevancy);
DISPLAY_PARAM(m_inv_clause_decay);
DISPLAY_PARAM(m_smtlib_dump_lemmas);
DISPLAY_PARAM(m_logic);
DISPLAY_PARAM(m_profile_res_sub);
DISPLAY_PARAM(m_display_bool_var2expr);
DISPLAY_PARAM(m_display_ll_bool_var2expr);
DISPLAY_PARAM(m_abort_after_preproc);
DISPLAY_PARAM(m_model);
DISPLAY_PARAM(m_model_compact);
DISPLAY_PARAM(m_model_on_timeout);
DISPLAY_PARAM(m_model_on_final_check);
DISPLAY_PARAM(m_progress_sampling_freq);
DISPLAY_PARAM(m_display_installed_theories);
DISPLAY_PARAM(m_core_validate);
DISPLAY_PARAM(m_preprocess);
DISPLAY_PARAM(m_user_theory_preprocess_axioms);
DISPLAY_PARAM(m_user_theory_persist_axioms);
DISPLAY_PARAM(m_timeout);
DISPLAY_PARAM(m_rlimit);
DISPLAY_PARAM(m_at_labels_cex);
DISPLAY_PARAM(m_check_at_labels);
DISPLAY_PARAM(m_dump_goal_as_smt);
DISPLAY_PARAM(m_auto_config);
}

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

@ -289,6 +289,8 @@ struct smt_params : public preprocessor_params,
void updt_params(params_ref const & p);
void updt_params(context_params const & p);
void display(std::ostream & out) const;
};
#endif /* SMT_PARAMS_H_ */

48
src/smt/params/theory_arith_params.cpp
View file

@ -38,3 +38,51 @@ void theory_arith_params::updt_params(params_ref const & _p) {
}
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
void theory_arith_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_arith_mode);
DISPLAY_PARAM(m_arith_auto_config_simplex); //!< force simplex solver in auto_config
DISPLAY_PARAM(m_arith_blands_rule_threshold);
DISPLAY_PARAM(m_arith_propagate_eqs);
DISPLAY_PARAM(m_arith_bound_prop);
DISPLAY_PARAM(m_arith_stronger_lemmas);
DISPLAY_PARAM(m_arith_skip_rows_with_big_coeffs);
DISPLAY_PARAM(m_arith_max_lemma_size);
DISPLAY_PARAM(m_arith_small_lemma_size);
DISPLAY_PARAM(m_arith_reflect);
DISPLAY_PARAM(m_arith_ignore_int);
DISPLAY_PARAM(m_arith_lazy_pivoting_lvl);
DISPLAY_PARAM(m_arith_random_seed);
DISPLAY_PARAM(m_arith_random_initial_value);
DISPLAY_PARAM(m_arith_random_lower);
DISPLAY_PARAM(m_arith_random_upper);
DISPLAY_PARAM(m_arith_adaptive);
DISPLAY_PARAM(m_arith_adaptive_assertion_threshold);
DISPLAY_PARAM(m_arith_adaptive_propagation_threshold);
DISPLAY_PARAM(m_arith_dump_lemmas);
DISPLAY_PARAM(m_arith_eager_eq_axioms);
DISPLAY_PARAM(m_arith_branch_cut_ratio);
DISPLAY_PARAM(m_arith_int_eq_branching);
DISPLAY_PARAM(m_arith_enum_const_mod);
DISPLAY_PARAM(m_arith_gcd_test);
DISPLAY_PARAM(m_arith_eager_gcd);
DISPLAY_PARAM(m_arith_adaptive_gcd);
DISPLAY_PARAM(m_arith_propagation_threshold);
DISPLAY_PARAM(m_arith_pivot_strategy);
DISPLAY_PARAM(m_arith_add_binary_bounds);
DISPLAY_PARAM(m_arith_propagation_strategy);
DISPLAY_PARAM(m_arith_eq_bounds);
DISPLAY_PARAM(m_arith_lazy_adapter);
DISPLAY_PARAM(m_arith_fixnum);
DISPLAY_PARAM(m_arith_int_only);
DISPLAY_PARAM(m_nl_arith);
DISPLAY_PARAM(m_nl_arith_gb);
DISPLAY_PARAM(m_nl_arith_gb_threshold);
DISPLAY_PARAM(m_nl_arith_gb_eqs);
DISPLAY_PARAM(m_nl_arith_gb_perturbate);
DISPLAY_PARAM(m_nl_arith_max_degree);
DISPLAY_PARAM(m_nl_arith_branching);
DISPLAY_PARAM(m_nl_arith_rounds);
DISPLAY_PARAM(m_arith_euclidean_solver);
}

2
src/smt/params/theory_arith_params.h
View file

@ -156,6 +156,8 @@ struct theory_arith_params {
}
void updt_params(params_ref const & p);
void display(std::ostream & out) const;
};
#endif /* THEORY_ARITH_PARAMS_H_ */

12
src/smt/params/theory_array_params.cpp
View file

@ -25,4 +25,16 @@ void theory_array_params::updt_params(params_ref const & _p) {
m_array_extensional = p.array_extensional();
}
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
void theory_array_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_array_mode);
DISPLAY_PARAM(m_array_weak);
DISPLAY_PARAM(m_array_extensional);
DISPLAY_PARAM(m_array_laziness);
DISPLAY_PARAM(m_array_delay_exp_axiom);
DISPLAY_PARAM(m_array_cg);
DISPLAY_PARAM(m_array_always_prop_upward);
DISPLAY_PARAM(m_array_lazy_ieq);
DISPLAY_PARAM(m_array_lazy_ieq_delay);
}

1
src/smt/params/theory_array_params.h
View file

@ -71,6 +71,7 @@ struct theory_array_params : public array_simplifier_params {
}
#endif
void display(std::ostream & out) const;
};

11
src/smt/params/theory_bv_params.cpp
View file

@ -24,3 +24,14 @@ void theory_bv_params::updt_params(params_ref const & _p) {
m_bv_reflect = p.bv_reflect();
m_bv_enable_int2bv2int = p.bv_enable_int2bv();
}
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
void theory_bv_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_bv_mode);
DISPLAY_PARAM(m_bv_reflect);
DISPLAY_PARAM(m_bv_lazy_le);
DISPLAY_PARAM(m_bv_cc);
DISPLAY_PARAM(m_bv_blast_max_size);
DISPLAY_PARAM(m_bv_enable_int2bv2int);
}

2
src/smt/params/theory_bv_params.h
View file

@ -44,6 +44,8 @@ struct theory_bv_params {
}
void updt_params(params_ref const & p);
void display(std::ostream & out) const;
};
#endif /* THEORY_BV_PARAMS_H_ */

2
src/smt/params/theory_datatype_params.h
View file

@ -31,6 +31,8 @@ struct theory_datatype_params {
p.register_unsigned_param("dt_lazy_splits", m_dt_lazy_splits, "How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy");
}
#endif
void display(std::ostream & out) const { out << "m_dt_lazy_splits=" << m_dt_lazy_splits << std::endl; }
};

9
src/smt/params/theory_pb_params.cpp
View file

@ -26,3 +26,12 @@ void theory_pb_params::updt_params(params_ref const & _p) {
m_pb_enable_compilation = p.pb_enable_compilation();
m_pb_enable_simplex = p.pb_enable_simplex();
}
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
void theory_pb_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_pb_conflict_frequency);
DISPLAY_PARAM(m_pb_learn_complements);
DISPLAY_PARAM(m_pb_enable_compilation);
DISPLAY_PARAM(m_pb_enable_simplex);
}

2
src/smt/params/theory_pb_params.h
View file

@ -35,6 +35,8 @@ struct theory_pb_params {
{}
void updt_params(params_ref const & p);
void display(std::ostream & out) const;
};
#endif /* THEORY_PB_PARAMS_H_ */