mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

removing dead params

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-22 16:36:46 -08:00
parent 33c44d014b
commit c4197722bb
5 changed files with 3 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/front_end_params/front_end_params.cpp
View file

@ -25,8 +25,6 @@ void front_end_params::register_params(ini_params & p) {
parser_params::register_params(p); parser_params::register_params(p);
arith_simplifier_params::register_params(p); arith_simplifier_params::register_params(p);
model_params::register_params(p); model_params::register_params(p);
p.register_unsigned_param("MAX_COUNTEREXAMPLES", m_max_num_cex,
"set the maximum number of counterexamples when using Simplify front end");
p.register_bool_param("AT_LABELS_CEX", m_at_labels_cex, p.register_bool_param("AT_LABELS_CEX", m_at_labels_cex,
"only use labels that contain '@' when building multiple counterexamples"); "only use labels that contain '@' when building multiple counterexamples");
p.register_bool_param("CHECK_AT_LABELS", m_check_at_labels, p.register_bool_param("CHECK_AT_LABELS", m_check_at_labels,

4
src/front_end_params/model_params.cpp
View file

@ -21,7 +21,6 @@ Revision History:
void model_params::register_params(ini_params & p) { void model_params::register_params(ini_params & p) {
p.register_bool_param("MODEL_PARTIAL", m_model_partial, "enable/disable partial function interpretations", true); p.register_bool_param("MODEL_PARTIAL", m_model_partial, "enable/disable partial function interpretations", true);
p.register_bool_param("MODEL_HIDE_UNUSED_PARTITIONS", m_model_hide_unused_partitions, "hide unused partitions, some partitions are associated with internal terms/formulas created by Z3", true);
p.register_bool_param("MODEL_V1", m_model_v1_pp, p.register_bool_param("MODEL_V1", m_model_v1_pp,
"use Z3 version 1.x pretty printer", true); "use Z3 version 1.x pretty printer", true);
p.register_bool_param("MODEL_V2", m_model_v2_pp, p.register_bool_param("MODEL_V2", m_model_v2_pp,
@ -30,8 +29,7 @@ void model_params::register_params(ini_params & p) {
"try to compact function graph (i.e., function interpretations that are lookup tables", true); "try to compact function graph (i.e., function interpretations that are lookup tables", true);
p.register_bool_param("MODEL_COMPLETION", m_model_completion, p.register_bool_param("MODEL_COMPLETION", m_model_completion,
"assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model", true); "assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model", true);
p.register_bool_param("MODEL_DISPLAY_ARG_SORT", m_model_display_arg_sort,
"display the sort of each argument when printing function interpretations", true);
} }

6
src/front_end_params/model_params.h
View file

@ -23,21 +23,17 @@ Revision History:
struct model_params { struct model_params {
bool m_model_partial; bool m_model_partial;
bool m_model_hide_unused_partitions;
bool m_model_compact; bool m_model_compact;
bool m_model_v1_pp; bool m_model_v1_pp;
bool m_model_v2_pp; bool m_model_v2_pp;
bool m_model_completion; bool m_model_completion;
bool m_model_display_arg_sort;
model_params(): model_params():
m_model_partial(false), m_model_partial(false),
m_model_hide_unused_partitions(true),
m_model_compact(false), m_model_compact(false),
m_model_v1_pp(false), m_model_v1_pp(false),
m_model_v2_pp(false), m_model_v2_pp(false),
m_model_completion(false), m_model_completion(false) {
m_model_display_arg_sort(true) {
} }
void register_params(ini_params & p); void register_params(ini_params & p);

2
src/front_end_params/pattern_inference_params.cpp
View file

@ -21,7 +21,7 @@ Revision History:
void pattern_inference_params::register_params(ini_params & p) { void pattern_inference_params::register_params(ini_params & p) {
p.register_unsigned_param("PI_MAX_MULTI_PATTERNS", m_pi_max_multi_patterns, p.register_unsigned_param("PI_MAX_MULTI_PATTERNS", m_pi_max_multi_patterns,
"when patterns are not provided, the prover uses a heuristic to infer them. This option sets the threshold on the number of extra multi-patterns that can be created. By default, the prover creates at most one multi-pattern when there is no unary pattern"); "when patterns are not provided, the prover uses a heuristic to infer them. This option sets the threshold on the number of extra multi-patterns that can be created. By default, the prover creates at most one multi-pattern when there is no unary pattern");
p.register_bool_param("PI_BLOCK_LOOOP_PATTERNS", m_pi_block_loop_patterns, p.register_bool_param("PI_BLOCK_LOOP_PATTERNS", m_pi_block_loop_patterns,
"block looping patterns during pattern inference"); "block looping patterns during pattern inference");
p.register_int_param("PI_ARITH", 0, 2, reinterpret_cast<int&>(m_pi_arith), p.register_int_param("PI_ARITH", 0, 2, reinterpret_cast<int&>(m_pi_arith),
"0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms."); "0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms.");

1
src/front_end_params/preprocessor_params.h
View file

@ -39,7 +39,6 @@ struct preprocessor_params : public nnf_params, public cnf_params, public patter
bool m_pull_nested_quantifiers; bool m_pull_nested_quantifiers;
bool m_eliminate_term_ite; bool m_eliminate_term_ite;
bool m_eliminate_and; // represent (and a b) as (not (or (not a) (not b))) bool m_eliminate_and; // represent (and a b) as (not (or (not a) (not b)))
bool m_reverse_implies; // translate (implies a b) into (or b (not a))
bool m_macro_finder; bool m_macro_finder;
bool m_propagate_values; bool m_propagate_values;
bool m_propagate_booleans; bool m_propagate_booleans;