From 8bde7b8a4cdabe15f4d72c07d172460d598ebd99 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 23 Jun 2016 19:31:00 +0100 Subject: [PATCH] Added facilities for dumping smt_params for debugging purposes --- src/ast/pattern/pattern_inference_params.cpp | 15 +++ src/ast/pattern/pattern_inference_params.h | 2 + .../rewriter/bit_blaster/bit_blaster_params.h | 7 +- .../simplifier/arith_simplifier_params.cpp | 7 ++ src/ast/simplifier/arith_simplifier_params.h | 2 + src/ast/simplifier/bv_simplifier_params.cpp | 7 ++ src/ast/simplifier/bv_simplifier_params.h | 2 + src/smt/params/dyn_ack_params.cpp | 11 +++ src/smt/params/dyn_ack_params.h | 2 + src/smt/params/preprocessor_params.cpp | 30 ++++++ src/smt/params/preprocessor_params.h | 2 + src/smt/params/qi_params.cpp | 27 ++++++ src/smt/params/qi_params.h | 4 +- src/smt/params/smt_params.cpp | 93 +++++++++++++++++++ src/smt/params/smt_params.h | 2 + src/smt/params/theory_arith_params.cpp | 48 ++++++++++ src/smt/params/theory_arith_params.h | 2 + src/smt/params/theory_array_params.cpp | 12 +++ src/smt/params/theory_array_params.h | 1 + src/smt/params/theory_bv_params.cpp | 11 +++ src/smt/params/theory_bv_params.h | 2 + src/smt/params/theory_datatype_params.h | 2 + src/smt/params/theory_pb_params.cpp | 9 ++ src/smt/params/theory_pb_params.h | 2 + 24 files changed, 300 insertions(+), 2 deletions(-) diff --git a/src/ast/pattern/pattern_inference_params.cpp b/src/ast/pattern/pattern_inference_params.cpp index 8adbdb9f1..b36d372f5 100644 --- a/src/ast/pattern/pattern_inference_params.cpp +++ b/src/ast/pattern/pattern_inference_params.cpp @@ -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); +} \ No newline at end of file diff --git a/src/ast/pattern/pattern_inference_params.h b/src/ast/pattern/pattern_inference_params.h index a941b7dd6..0dc413399 100644 --- a/src/ast/pattern/pattern_inference_params.h +++ b/src/ast/pattern/pattern_inference_params.h @@ -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_ */ diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_params.h b/src/ast/rewriter/bit_blaster/bit_blaster_params.h index ee32d005a..15ece0043 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_params.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_params.h @@ -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_ */ diff --git a/src/ast/simplifier/arith_simplifier_params.cpp b/src/ast/simplifier/arith_simplifier_params.cpp index a3fabe02f..8584cdae0 100644 --- a/src/ast/simplifier/arith_simplifier_params.cpp +++ b/src/ast/simplifier/arith_simplifier_params.cpp @@ -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); +} \ No newline at end of file diff --git a/src/ast/simplifier/arith_simplifier_params.h b/src/ast/simplifier/arith_simplifier_params.h index 2ff8fe2c0..6186ee4a2 100644 --- a/src/ast/simplifier/arith_simplifier_params.h +++ b/src/ast/simplifier/arith_simplifier_params.h @@ -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_ */ diff --git a/src/ast/simplifier/bv_simplifier_params.cpp b/src/ast/simplifier/bv_simplifier_params.cpp index 5d6cd363f..1ed263aa6 100644 --- a/src/ast/simplifier/bv_simplifier_params.cpp +++ b/src/ast/simplifier/bv_simplifier_params.cpp @@ -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); +} \ No newline at end of file diff --git a/src/ast/simplifier/bv_simplifier_params.h b/src/ast/simplifier/bv_simplifier_params.h index 50015b7ca..dafa99065 100644 --- a/src/ast/simplifier/bv_simplifier_params.h +++ b/src/ast/simplifier/bv_simplifier_params.h @@ -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_ */ diff --git a/src/smt/params/dyn_ack_params.cpp b/src/smt/params/dyn_ack_params.cpp index 15f48bad1..b62530fbf 100644 --- a/src/smt/params/dyn_ack_params.cpp +++ b/src/smt/params/dyn_ack_params.cpp @@ -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); +} \ No newline at end of file diff --git a/src/smt/params/dyn_ack_params.h b/src/smt/params/dyn_ack_params.h index f87e3b6df..017b7fe94 100644 --- a/src/smt/params/dyn_ack_params.h +++ b/src/smt/params/dyn_ack_params.h @@ -47,6 +47,8 @@ public: } void updt_params(params_ref const & _p); + + void display(std::ostream & out) const; }; diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp index 9ad787c2a..7a0e96248 100644 --- a/src/smt/params/preprocessor_params.cpp +++ b/src/smt/params/preprocessor_params.cpp @@ -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); +} diff --git a/src/smt/params/preprocessor_params.h b/src/smt/params/preprocessor_params.h index 3806b26cf..4ffad48a2 100644 --- a/src/smt/params/preprocessor_params.h +++ b/src/smt/params/preprocessor_params.h @@ -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_ */ diff --git a/src/smt/params/qi_params.cpp b/src/smt/params/qi_params.cpp index 60fcd6fc4..a341040ce 100644 --- a/src/smt/params/qi_params.cpp +++ b/src/smt/params/qi_params.cpp @@ -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); +} \ No newline at end of file diff --git a/src/smt/params/qi_params.h b/src/smt/params/qi_params.h index 00baea170..c9736909a 100644 --- a/src/smt/params/qi_params.h +++ b/src/smt/params/qi_params.h @@ -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_ */ diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 8222c3d60..8a9188e2b 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -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); +} \ No newline at end of file diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 9c1eec649..366570365 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -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_ */ diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index fef7ca2a0..1e3f29142 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -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); +} \ No newline at end of file diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index 18418d1ef..943bd711e 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -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_ */ diff --git a/src/smt/params/theory_array_params.cpp b/src/smt/params/theory_array_params.cpp index e3c8b2448..c0015bf2c 100644 --- a/src/smt/params/theory_array_params.cpp +++ b/src/smt/params/theory_array_params.cpp @@ -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); +} \ No newline at end of file diff --git a/src/smt/params/theory_array_params.h b/src/smt/params/theory_array_params.h index 85996078f..af51427c4 100644 --- a/src/smt/params/theory_array_params.h +++ b/src/smt/params/theory_array_params.h @@ -71,6 +71,7 @@ struct theory_array_params : public array_simplifier_params { } #endif + void display(std::ostream & out) const; }; diff --git a/src/smt/params/theory_bv_params.cpp b/src/smt/params/theory_bv_params.cpp index d3f386ab4..631c5765b 100644 --- a/src/smt/params/theory_bv_params.cpp +++ b/src/smt/params/theory_bv_params.cpp @@ -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); +} \ No newline at end of file diff --git a/src/smt/params/theory_bv_params.h b/src/smt/params/theory_bv_params.h index 00565969e..5830e5176 100644 --- a/src/smt/params/theory_bv_params.h +++ b/src/smt/params/theory_bv_params.h @@ -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_ */ diff --git a/src/smt/params/theory_datatype_params.h b/src/smt/params/theory_datatype_params.h index 4dd09a596..9f801e46c 100644 --- a/src/smt/params/theory_datatype_params.h +++ b/src/smt/params/theory_datatype_params.h @@ -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; } }; diff --git a/src/smt/params/theory_pb_params.cpp b/src/smt/params/theory_pb_params.cpp index 6d980fe5d..a1e13a6e7 100644 --- a/src/smt/params/theory_pb_params.cpp +++ b/src/smt/params/theory_pb_params.cpp @@ -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); +} \ No newline at end of file diff --git a/src/smt/params/theory_pb_params.h b/src/smt/params/theory_pb_params.h index 2af4f04b7..6a129e601 100644 --- a/src/smt/params/theory_pb_params.h +++ b/src/smt/params/theory_pb_params.h @@ -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_ */