From 9374a4e20ae1bcabcaacbd1408a2ab728886f462 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 1 Dec 2012 16:30:39 -0800 Subject: [PATCH] removed ini_file Signed-off-by: Leonardo de Moura --- src/cmd_context/cmd_context.cpp | 5 - .../arith_simplifier_params.cpp | 3 +- .../arith_simplifier_params.h | 4 - src/front_end_params/bit_blaster_params.h | 4 +- src/front_end_params/bv_simplifier_params.h | 4 +- src/front_end_params/dyn_ack_params.cpp | 3 +- src/front_end_params/dyn_ack_params.h | 3 - src/front_end_params/front_end_params.cpp | 10 +- src/front_end_params/front_end_params.h | 25 - .../pattern_inference_params.cpp | 3 +- .../pattern_inference_params.h | 4 - src/front_end_params/preprocessor_params.h | 3 + src/front_end_params/qi_params.h | 7 +- src/front_end_params/smt_params.cpp | 2 + src/front_end_params/smt_params.h | 7 +- src/front_end_params/theory_arith_params.cpp | 2 + src/front_end_params/theory_arith_params.h | 4 +- src/front_end_params/theory_array_params.h | 5 +- src/front_end_params/theory_bv_params.h | 4 +- src/front_end_params/theory_datatype_params.h | 4 +- src/muz_qe/dl_cmds.cpp | 6 +- src/muz_qe/dl_context.cpp | 16 +- src/muz_qe/pdr_dl_interface.cpp | 22 +- src/shell/datalog_frontend.cpp | 8 +- src/shell/datalog_frontend.h | 2 +- src/shell/main.cpp | 55 +- src/shell/smtlib_frontend.cpp | 1 - src/smt/smt_context.cpp | 6 - src/smt/smt_context.h | 2 - src/smt/smt_setup.cpp | 1 - src/test/ini_file.cpp | 50 - src/test/main.cpp | 1 - src/util/ini_file.cpp | 1564 ----------------- src/util/ini_file.h | 117 -- src/util/instruction_count.cpp | 41 - src/util/instruction_count.h | 43 - src/util/util.cpp | 6 +- src/util/warning.cpp | 6 +- 38 files changed, 82 insertions(+), 1971 deletions(-) delete mode 100644 src/test/ini_file.cpp delete mode 100644 src/util/ini_file.cpp delete mode 100644 src/util/ini_file.h delete mode 100644 src/util/instruction_count.cpp delete mode 100644 src/util/instruction_count.h diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index cd8c81387..984e5db0c 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1295,11 +1295,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions return; IF_VERBOSE(100, verbose_stream() << "check-sat..." << std::endl;); TRACE("before_check_sat", dump_assertions(tout);); - if (params().m_ignore_checksat) { - m_check_sat_result = 0; - regular_stream() << "unknown" << std::endl; - return; - } if (!has_manager()) init_manager(); if (m_solver) { diff --git a/src/front_end_params/arith_simplifier_params.cpp b/src/front_end_params/arith_simplifier_params.cpp index 21808bc1e..8cf07b915 100644 --- a/src/front_end_params/arith_simplifier_params.cpp +++ b/src/front_end_params/arith_simplifier_params.cpp @@ -19,8 +19,9 @@ Revision History: #include"arith_simplifier_params.h" +#if 0 void arith_simplifier_params::register_params(ini_params & p) { p.register_bool_param("arith_expand_eqs", m_arith_expand_eqs); p.register_bool_param("arith_process_all_eqs", m_arith_process_all_eqs); } - +#endif diff --git a/src/front_end_params/arith_simplifier_params.h b/src/front_end_params/arith_simplifier_params.h index 3e44b5a6e..f1b22b09a 100644 --- a/src/front_end_params/arith_simplifier_params.h +++ b/src/front_end_params/arith_simplifier_params.h @@ -19,8 +19,6 @@ Revision History: #ifndef _ARITH_SIMPLIFIER_PARAMS_H_ #define _ARITH_SIMPLIFIER_PARAMS_H_ -#include"ini_file.h" - struct arith_simplifier_params { bool m_arith_expand_eqs; bool m_arith_process_all_eqs; @@ -29,8 +27,6 @@ struct arith_simplifier_params { m_arith_expand_eqs(false), m_arith_process_all_eqs(false) { } - - void register_params(ini_params & p); }; #endif /* _ARITH_SIMPLIFIER_PARAMS_H_ */ diff --git a/src/front_end_params/bit_blaster_params.h b/src/front_end_params/bit_blaster_params.h index ab183d7fc..653c8fc74 100644 --- a/src/front_end_params/bit_blaster_params.h +++ b/src/front_end_params/bit_blaster_params.h @@ -19,8 +19,6 @@ Revision History: #ifndef _BIT_BLASTER_PARAMS_H_ #define _BIT_BLASTER_PARAMS_H_ -#include"ini_file.h" - struct bit_blaster_params { bool m_bb_ext_gates; bool m_bb_quantifiers; @@ -28,10 +26,12 @@ struct bit_blaster_params { m_bb_ext_gates(false), m_bb_quantifiers(false) { } +#if 0 void register_params(ini_params & p) { p.register_bool_param("bb_ext_gates", m_bb_ext_gates, "use extended gates during bit-blasting"); p.register_bool_param("bb_quantifiers", m_bb_quantifiers, "convert bit-vectors to Booleans in quantifiers"); } +#endif }; #endif /* _BIT_BLASTER_PARAMS_H_ */ diff --git a/src/front_end_params/bv_simplifier_params.h b/src/front_end_params/bv_simplifier_params.h index 50dedfd22..887940e36 100644 --- a/src/front_end_params/bv_simplifier_params.h +++ b/src/front_end_params/bv_simplifier_params.h @@ -19,8 +19,6 @@ Revision History: #ifndef _BV_SIMPLIFIER_PARAMS_H_ #define _BV_SIMPLIFIER_PARAMS_H_ -#include"ini_file.h" - struct bv_simplifier_params { bool m_hi_div0; //!< if true, uses the hardware interpretation for div0, mod0, ... if false, div0, mod0, ... are considered uninterpreted. bool m_bv2int_distribute; //!< if true allows downward propagation of bv2int. @@ -29,10 +27,12 @@ struct bv_simplifier_params { m_hi_div0(true), m_bv2int_distribute(true) { } +#if 0 void register_params(ini_params & p) { p.register_bool_param("hi_div0", m_hi_div0, "if true, then Z3 uses the usual hardware interpretation for division (rem, mod) by zero. Otherwise, these operations are considered uninterpreted."); p.register_bool_param("bv2int_distribute", m_bv2int_distribute, "if true, then int2bv is distributed over arithmetical operators."); } +#endif }; #endif /* _BV_SIMPLIFIER_PARAMS_H_ */ diff --git a/src/front_end_params/dyn_ack_params.cpp b/src/front_end_params/dyn_ack_params.cpp index 90a0bb17b..2e94c376d 100644 --- a/src/front_end_params/dyn_ack_params.cpp +++ b/src/front_end_params/dyn_ack_params.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include"dyn_ack_params.h" +#if 0 void dyn_ack_params::register_params(ini_params & p) { p.register_int_param("dack", 0, 2, reinterpret_cast(m_dack), "0 - disable dynamic ackermannization, 1 - expand Leibniz's axiom if a congruence is the root of a conflict, 2 - expand Leibniz's axiom if a congruence is used during conflict resolution."); @@ -27,5 +28,5 @@ void dyn_ack_params::register_params(ini_params & p) { p.register_unsigned_param("dack_gc", m_dack_gc, "Dynamic ackermannization garbage collection frequency (per conflict)."); p.register_double_param("dack_gc_inv_decay", m_dack_gc_inv_decay); } - +#endif diff --git a/src/front_end_params/dyn_ack_params.h b/src/front_end_params/dyn_ack_params.h index c5325195e..9f7ce578c 100644 --- a/src/front_end_params/dyn_ack_params.h +++ b/src/front_end_params/dyn_ack_params.h @@ -19,8 +19,6 @@ Revision History: #ifndef _DYN_ACK_PARAMS_H_ #define _DYN_ACK_PARAMS_H_ -#include"ini_file.h" - enum dyn_ack_strategy { DACK_DISABLED, DACK_ROOT, // congruence is the root of the conflict @@ -45,7 +43,6 @@ public: m_dack_gc_inv_decay(0.8) { } - void register_params(ini_params & p); }; diff --git a/src/front_end_params/front_end_params.cpp b/src/front_end_params/front_end_params.cpp index d30ec825d..49c3f042e 100644 --- a/src/front_end_params/front_end_params.cpp +++ b/src/front_end_params/front_end_params.cpp @@ -18,8 +18,9 @@ Revision History: --*/ #include"front_end_params.h" +#if 0 + void front_end_params::register_params(ini_params & p) { - p.register_param_vector(m_param_vector.get()); preprocessor_params::register_params(p); smt_params::register_params(p); arith_simplifier_params::register_params(p); @@ -27,8 +28,6 @@ void front_end_params::register_params(ini_params & p) { "only use labels that contain '@' when building multiple counterexamples"); p.register_bool_param("check_at_labels", m_check_at_labels, "check that labels containing '@' are used correctly to only produce unique counter examples"); - p.register_bool_param("default_qid", m_default_qid, "create a default quantifier id based on its position, the id is used to report profiling information (see QI_PROFILE)"); - p.register_bool_param("type_check", m_well_sorted_check, "enable/disable type checker"); p.register_bool_param("well_sorted_check", m_well_sorted_check, "enable/disable type checker"); p.register_unsigned_param("soft_timeout", m_soft_timeout, "set approximate timeout for each solver query (milliseconds), the value 0 represents no timeout", true); @@ -49,10 +48,7 @@ void front_end_params::register_params(ini_params & p) { PRIVATE_PARAMS({ - p.register_bool_param("ignore_checksat", m_ignore_checksat); p.register_bool_param("debug_ref_count", m_debug_ref_count); - p.register_bool_param("incremental_core_assert", m_incremental_core_assert); - DEBUG_CODE(p.register_int_param("copy_params", m_copy_params);); }); // temporary hack until strategic_solver is ported to new tactic framework @@ -61,6 +57,8 @@ void front_end_params::register_params(ini_params & p) { }); } +#endif + void front_end_params::open_trace_file() { if (m_trace) { m_trace_stream = alloc(std::fstream, m_trace_file_name.c_str(), std::ios_base::out); diff --git a/src/front_end_params/front_end_params.h b/src/front_end_params/front_end_params.h index 505052450..d033ba911 100644 --- a/src/front_end_params/front_end_params.h +++ b/src/front_end_params/front_end_params.h @@ -19,7 +19,6 @@ Revision History: #ifndef _FRONT_END_PARAMS_H_ #define _FRONT_END_PARAMS_H_ -#include"ini_file.h" #include"ast.h" #include"preprocessor_params.h" #include"smt_params.h" @@ -27,23 +26,14 @@ Revision History: struct front_end_params : public preprocessor_params, public smt_params, public arith_simplifier_params { - ref m_param_vector; bool m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples. bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples. - bool m_default_qid; bool m_well_sorted_check; - bool m_incremental_core_assert; // assert conditions to the core incrementally - unsigned m_soft_timeout; - double m_instr_out; unsigned m_memory_high_watermark; unsigned m_memory_max_size; proof_gen_mode m_proof_mode; bool m_auto_config; -#ifdef Z3DEBUG - int m_copy_params; // used for testing copy params... Invoke method copy_params(m_copy_params) in main.cpp when diff -1. -#endif - bool m_ignore_checksat; // abort before checksat... for internal debugging bool m_debug_ref_count; bool m_trace; std::string m_trace_file_name; @@ -54,14 +44,9 @@ struct front_end_params : public preprocessor_params, public smt_params, bool m_dump_goal_as_smt; front_end_params(): - m_param_vector(alloc(param_vector, this)), m_at_labels_cex(false), m_check_at_labels(false), - m_default_qid(false), m_well_sorted_check(true), - m_incremental_core_assert(true), - m_soft_timeout(0), - m_instr_out(0.0), m_memory_high_watermark(0), m_memory_max_size(0), m_proof_mode(PGM_DISABLED), @@ -70,10 +55,6 @@ struct front_end_params : public preprocessor_params, public smt_params, #else m_auto_config(false), #endif -#ifdef Z3DEBUG - m_copy_params(-1), -#endif - m_ignore_checksat(false), m_debug_ref_count(false), m_trace(false), m_trace_file_name("z3.log"), @@ -83,16 +64,10 @@ struct front_end_params : public preprocessor_params, public smt_params, m_dump_goal_as_smt(false) { } - void register_params(ini_params & p); - void open_trace_file(); void close_trace_file(); - void copy_params(unsigned idx) { - m_param_vector->copy_params(this, idx); - } - bool has_auto_config(unsigned idx) { return m_auto_config; } private: diff --git a/src/front_end_params/pattern_inference_params.cpp b/src/front_end_params/pattern_inference_params.cpp index 4b0d4c964..cfc0df4f1 100644 --- a/src/front_end_params/pattern_inference_params.cpp +++ b/src/front_end_params/pattern_inference_params.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include"pattern_inference_params.h" +#if 0 void pattern_inference_params::register_params(ini_params & p) { 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"); @@ -33,5 +34,5 @@ void pattern_inference_params::register_params(ini_params & p) { p.register_bool_param("pi_avoid_skolems", m_pi_avoid_skolems); p.register_bool_param("pi_warnings", m_pi_warnings, "enable/disable warning messages in the pattern inference module."); } - +#endif diff --git a/src/front_end_params/pattern_inference_params.h b/src/front_end_params/pattern_inference_params.h index 79d7b4d87..7108e5589 100644 --- a/src/front_end_params/pattern_inference_params.h +++ b/src/front_end_params/pattern_inference_params.h @@ -19,8 +19,6 @@ Revision History: #ifndef _PATTERN_INFERENCE_PARAMS_H_ #define _PATTERN_INFERENCE_PARAMS_H_ -#include"ini_file.h" - enum arith_pattern_inference_kind { AP_NO, // do not infer patterns with arithmetic terms AP_CONSERVATIVE, // only infer patterns with arithmetic terms if there is no other option @@ -51,8 +49,6 @@ struct pattern_inference_params { m_pi_avoid_skolems(true), m_pi_warnings(false) { } - - void register_params(ini_params & p); }; #endif /* _PATTERN_INFERENCE_PARAMS_H_ */ diff --git a/src/front_end_params/preprocessor_params.h b/src/front_end_params/preprocessor_params.h index 00466bc02..b84aebe1a 100644 --- a/src/front_end_params/preprocessor_params.h +++ b/src/front_end_params/preprocessor_params.h @@ -76,6 +76,7 @@ public: m_nlquant_elim(false) { } +#if 0 void register_params(ini_params & p) { pattern_inference_params::register_params(p); bit_blaster_params::register_params(p); @@ -100,6 +101,8 @@ public: p.register_bool_param("bv_max_sharing", m_max_bv_sharing); p.register_bool_param("pre_simplifier", m_pre_simplifier); } +#endif + }; #endif /* _PREPROCESSOR_PARAMS_H_ */ diff --git a/src/front_end_params/qi_params.h b/src/front_end_params/qi_params.h index aee2c4d3d..1a8edb3a8 100644 --- a/src/front_end_params/qi_params.h +++ b/src/front_end_params/qi_params.h @@ -19,7 +19,7 @@ Revision History: #ifndef _QI_PARAMS_H_ #define _QI_PARAMS_H_ -#include"ini_file.h" +#include"util.h" enum quick_checker_mode { MC_NO, // do not use (cheap) model checking based instantiation @@ -105,7 +105,8 @@ struct qi_params { m_mbqi_force_template(10), m_instgen(false) { } - + +#if 0 void register_params(ini_params & p) { p.register_unsigned_param("qi_max_eager_multi_patterns", m_qi_max_eager_multipatterns, "Specify the number of extra multi patterns that are processed eagerly. By default, the prover use at most one multi-pattern eagerly when there is no unary pattern. This value should be smaller than or equal to PI_MAX_MULTI_PATTERNS"); @@ -133,6 +134,8 @@ struct qi_params { p.register_bool_param("inst_gen", m_instgen, "Enable Instantiation Generation solver (disables other quantifier reasoning)", false); } +#endif + }; #endif /* _QI_PARAMS_H_ */ diff --git a/src/front_end_params/smt_params.cpp b/src/front_end_params/smt_params.cpp index 737b369b4..77d3660e6 100644 --- a/src/front_end_params/smt_params.cpp +++ b/src/front_end_params/smt_params.cpp @@ -19,6 +19,7 @@ Revision History: #include"smt_params.h" #include"trace.h" +#if 0 void smt_params::register_params(ini_params & p) { dyn_ack_params::register_params(p); qi_params::register_params(p); @@ -117,3 +118,4 @@ void smt_params::register_params(ini_params & p) { } +#endif diff --git a/src/front_end_params/smt_params.h b/src/front_end_params/smt_params.h index c6b34a2d3..804049315 100644 --- a/src/front_end_params/smt_params.h +++ b/src/front_end_params/smt_params.h @@ -19,7 +19,6 @@ Revision History: #ifndef _SMT_PARAMS_H_ #define _SMT_PARAMS_H_ -#include"ini_file.h" #include"dyn_ack_params.h" #include"qi_params.h" #include"theory_arith_params.h" @@ -196,6 +195,7 @@ struct smt_params : public dyn_ack_params, public qi_params, public theory_arith bool m_preprocess; // temporary hack for disabling all preprocessing.. bool m_user_theory_preprocess_axioms; bool m_user_theory_persist_axioms; + unsigned m_soft_timeout; smt_params(): m_display_proof(false), @@ -259,12 +259,11 @@ struct smt_params : public dyn_ack_params, public qi_params, public theory_arith m_display_installed_theories(false), m_preprocess(true), // temporary hack for disabling all preprocessing.. m_user_theory_preprocess_axioms(false), - m_user_theory_persist_axioms(false) + m_user_theory_persist_axioms(false), + m_soft_timeout(0) { } - - void register_params(ini_params & p); }; #endif /* _SMT_PARAMS_H_ */ diff --git a/src/front_end_params/theory_arith_params.cpp b/src/front_end_params/theory_arith_params.cpp index 49a654dbf..8dde26e94 100644 --- a/src/front_end_params/theory_arith_params.cpp +++ b/src/front_end_params/theory_arith_params.cpp @@ -19,6 +19,7 @@ Revision History: #include"theory_arith_params.h" +#if 0 void theory_arith_params::register_params(ini_params & p) { #ifdef _EXTERNAL_RELEASE p.register_int_param("arith_solver", 0, 3, reinterpret_cast(m_arith_mode), "select arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination"); @@ -74,3 +75,4 @@ void theory_arith_params::register_params(ini_params & p) { p.register_bool_param("arith_euclidean_solver", m_arith_euclidean_solver, ""); } +#endif diff --git a/src/front_end_params/theory_arith_params.h b/src/front_end_params/theory_arith_params.h index 290049037..01163dd0a 100644 --- a/src/front_end_params/theory_arith_params.h +++ b/src/front_end_params/theory_arith_params.h @@ -19,7 +19,7 @@ Revision History: #ifndef _THEORY_ARITH_PARAMS_H_ #define _THEORY_ARITH_PARAMS_H_ -#include"ini_file.h" +#include enum arith_solver_id { AS_NO_ARITH, @@ -150,8 +150,6 @@ struct theory_arith_params { m_nl_arith_rounds(1024), m_arith_euclidean_solver(false) { } - - void register_params(ini_params & p); }; #endif /* _THEORY_ARITH_PARAMS_H_ */ diff --git a/src/front_end_params/theory_array_params.h b/src/front_end_params/theory_array_params.h index 3d45ebcf5..e33bc2566 100644 --- a/src/front_end_params/theory_array_params.h +++ b/src/front_end_params/theory_array_params.h @@ -19,8 +19,6 @@ Revision History: #ifndef _THEORY_ARRAY_PARAMS_H_ #define _THEORY_ARRAY_PARAMS_H_ -#include"ini_file.h" - enum array_solver_id { AR_NO_ARRAY, AR_SIMPLE, @@ -55,6 +53,7 @@ struct theory_array_params { m_array_simplify(true) { } +#if 0 void register_params(ini_params & p) { p.register_int_param("array_solver", 0, 3, reinterpret_cast(m_array_mode), "0 - no array, 1 - simple, 2 - model based, 3 - full"); p.register_bool_param("array_weak", m_array_weak); @@ -69,6 +68,8 @@ struct theory_array_params { p.register_bool_param("array_canonize", m_array_canonize_simplify, "Normalize arrays into normal form during simplification"); } +#endif + }; diff --git a/src/front_end_params/theory_bv_params.h b/src/front_end_params/theory_bv_params.h index 6bf5ac868..18a3bac77 100644 --- a/src/front_end_params/theory_bv_params.h +++ b/src/front_end_params/theory_bv_params.h @@ -19,8 +19,6 @@ Revision History: #ifndef _THEORY_BV_PARAMS_H_ #define _THEORY_BV_PARAMS_H_ -#include"ini_file.h" - enum bv_solver_id { BS_NO_BV, BS_BLASTER @@ -40,6 +38,7 @@ struct theory_bv_params { m_bv_cc(false), m_bv_blast_max_size(INT_MAX), m_bv_enable_int2bv2int(false) {} +#if 0 void register_params(ini_params & p) { p.register_int_param("bv_solver", 0, 2, reinterpret_cast(m_bv_mode), "0 - no bv, 1 - simple"); p.register_unsigned_param("bv_blast_max_size", m_bv_blast_max_size, "Maximal size for bit-vectors to blast"); @@ -49,6 +48,7 @@ struct theory_bv_params { p.register_bool_param("bv_enable_int2bv_propagation", m_bv_enable_int2bv2int, "enable full (potentially expensive) propagation for int2bv and bv2int"); } +#endif }; #endif /* _THEORY_BV_PARAMS_H_ */ diff --git a/src/front_end_params/theory_datatype_params.h b/src/front_end_params/theory_datatype_params.h index 33b2c1814..8f914ac7b 100644 --- a/src/front_end_params/theory_datatype_params.h +++ b/src/front_end_params/theory_datatype_params.h @@ -19,8 +19,6 @@ Revision History: #ifndef _THEORY_DATATYPE_PARAMS_H_ #define _THEORY_DATATYPE_PARAMS_H_ -#include"ini_file.h" - struct theory_datatype_params { unsigned m_dt_lazy_splits; @@ -28,9 +26,11 @@ struct theory_datatype_params { m_dt_lazy_splits(1) { } +#if 0 void register_params(ini_params & p) { 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 }; diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz_qe/dl_cmds.cpp index 28e699c7c..d89b8d80d 100644 --- a/src/muz_qe/dl_cmds.cpp +++ b/src/muz_qe/dl_cmds.cpp @@ -472,8 +472,10 @@ static void install_dl_cmds_aux(cmd_context& ctx, dl_collected_cmds* collected_c ctx.insert(alloc(dl_query_cmd, dl_ctx)); ctx.insert(alloc(dl_declare_rel_cmd, dl_ctx)); ctx.insert(alloc(dl_declare_var_cmd, dl_ctx)); - PRIVATE_PARAMS(ctx.insert(alloc(dl_push_cmd, dl_ctx));); // not exposed to keep command-extensions simple. - PRIVATE_PARAMS(ctx.insert(alloc(dl_pop_cmd, dl_ctx));); +#ifndef _EXTERNAL_RELEASE + ctx.insert(alloc(dl_push_cmd, dl_ctx)); // not exposed to keep command-extensions simple. + ctx.insert(alloc(dl_pop_cmd, dl_ctx)); +#endif } void install_dl_cmds(cmd_context & ctx) { diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 3a2844964..631e1266c 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -997,19 +997,19 @@ namespace datalog { p.insert("print_low_level_smt2", CPK_BOOL, "(default false) use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)"); p.insert("print_with_variable_declarations", CPK_BOOL, "(default true) use variable declarations when displaying rules (instead of attempting to use original names)"); - PRIVATE_PARAMS( - p.insert("dbg_fpr_nonempty_relation_signature", CPK_BOOL, - "if true, finite_product_relation will attempt to avoid creating inner relation with empty signature " - "by putting in half of the table columns, if it would have been empty otherwise"); - - p.insert("smt_relation_ground_recursive", CPK_BOOL, "Ensure recursive relation is ground in union"); - ); +#ifndef _EXTERNAL_RELEASE + p.insert("dbg_fpr_nonempty_relation_signature", CPK_BOOL, + "if true, finite_product_relation will attempt to avoid creating inner relation with empty signature " + "by putting in half of the table columns, if it would have been empty otherwise"); + p.insert("smt_relation_ground_recursive", CPK_BOOL, "Ensure recursive relation is ground in union"); + p.insert("inline_linear_branch", CPK_BOOL, "try linear inlining method with potential expansion"); +#endif p.insert("fix_unbound_vars", CPK_BOOL, "fix unbound variables in tail"); p.insert("default_table_checker", CPK_SYMBOL, "see default_table_checked"); p.insert("inline_linear", CPK_BOOL, "(default true) try linear inlining method"); p.insert("inline_eager", CPK_BOOL, "(default true) try eager inlining of rules"); - PRIVATE_PARAMS(p.insert("inline_linear_branch", CPK_BOOL, "try linear inlining method with potential expansion");); + pdr::dl_interface::collect_params(p); bmc::collect_params(p); diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp index 6cbc3b78d..cee6cf747 100644 --- a/src/muz_qe/pdr_dl_interface.cpp +++ b/src/muz_qe/pdr_dl_interface.cpp @@ -258,16 +258,18 @@ void dl_interface::collect_params(param_descrs& p) { p.insert("unfold_rules", CPK_UINT, "PDR: (default 0) unfold rules statically using iterative squarring"); p.insert("use_model_generalizer", CPK_BOOL, "PDR: (default false) use model for backwards propagation (instead of symbolic simulation)"); p.insert("validate_result", CPK_BOOL, "PDR (default false) validate result (by proof checking or model checking)"); - PRIVATE_PARAMS(p.insert("use_multicore_generalizer", CPK_BOOL, "PDR: (default false) extract multiple cores for blocking states");); - PRIVATE_PARAMS(p.insert("use_inductive_generalizer", CPK_BOOL, "PDR: (default true) generalize lemmas using induction strengthening");); - PRIVATE_PARAMS(p.insert("use_interpolants", CPK_BOOL, "PDR: (default false) use iZ3 interpolation for lemma generation");); - PRIVATE_PARAMS(p.insert("dump_interpolants", CPK_BOOL, "PDR: (default false) display interpolants");); - PRIVATE_PARAMS(p.insert("cache_mode", CPK_UINT, "PDR: use no (0 - default) symbolic (1) or explicit cache (2) for model search");); - PRIVATE_PARAMS(p.insert("inductive_reachability_check", CPK_BOOL, - "PDR: (default false) assume negation of the cube on the previous level when " - "checking for reachability (not only during cube weakening)");); - PRIVATE_PARAMS(p.insert("max_num_contexts", CPK_UINT, "PDR: (default 500) maximal number of contexts to create");); - PRIVATE_PARAMS(p.insert("try_minimize_core", CPK_BOOL, "PDR: (default false) try to reduce core size (before inductive minimization)");); +#ifndef _EXTERNAL_RELEASE + p.insert("use_multicore_generalizer", CPK_BOOL, "PDR: (default false) extract multiple cores for blocking states"); + p.insert("use_inductive_generalizer", CPK_BOOL, "PDR: (default true) generalize lemmas using induction strengthening"); + p.insert("use_interpolants", CPK_BOOL, "PDR: (default false) use iZ3 interpolation for lemma generation"); + p.insert("dump_interpolants", CPK_BOOL, "PDR: (default false) display interpolants"); + p.insert("cache_mode", CPK_UINT, "PDR: use no (0 - default) symbolic (1) or explicit cache (2) for model search"); + p.insert("inductive_reachability_check", CPK_BOOL, + "PDR: (default false) assume negation of the cube on the previous level when " + "checking for reachability (not only during cube weakening)"); + p.insert("max_num_contexts", CPK_UINT, "PDR: (default 500) maximal number of contexts to create"); + p.insert("try_minimize_core", CPK_BOOL, "PDR: (default false) try to reduce core size (before inductive minimization)"); +#endif p.insert("simplify_formulas_pre", CPK_BOOL, "PDR: (default false) simplify derived formulas before inductive propagation"); p.insert("simplify_formulas_post", CPK_BOOL, "PDR: (default false) simplify derived formulas after inductive propagation"); p.insert("slice", CPK_BOOL, "PDR: (default true) simplify clause set using slicing"); diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp index d422db708..4bfe2a545 100644 --- a/src/shell/datalog_frontend.cpp +++ b/src/shell/datalog_frontend.cpp @@ -50,10 +50,10 @@ datalog_params::datalog_params(): m_default_table_checked(false) {} -void datalog_params::register_params(ini_params& p) { - p.register_symbol_param("DEFAULT_TABLE", m_default_table, "Datalog engine: default table (sparse)"); - p.register_bool_param("DEFAULT_TABLE_CHECKED", m_default_table_checked, "Wrap default table with a sanity checker"); -} +// void datalog_params::register_params(ini_params& p) { +// p.register_symbol_param("DEFAULT_TABLE", m_default_table, "Datalog engine: default table (sparse)"); +// p.register_bool_param("DEFAULT_TABLE_CHECKED", m_default_table_checked, "Wrap default table with a sanity checker"); +// } static void display_statistics( std::ostream& out, diff --git a/src/shell/datalog_frontend.h b/src/shell/datalog_frontend.h index 898a7fd97..7e08fce0e 100644 --- a/src/shell/datalog_frontend.h +++ b/src/shell/datalog_frontend.h @@ -23,7 +23,7 @@ struct datalog_params { symbol m_default_table; bool m_default_table_checked; datalog_params(); - virtual void register_params(ini_params& p); + // virtual void register_params(ini_params& p); }; unsigned read_datalog(char const * file, datalog_params const& dl_params, front_end_params & front_end_params); diff --git a/src/shell/main.cpp b/src/shell/main.cpp index bc3953c1e..5434206cc 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -109,13 +109,13 @@ public: virtual ~extra_params() {} - virtual void register_params(ini_params & p) { - datalog_params::register_params(p); - p.register_bool_param("STATISTICS", m_statistics, "display statistics"); - } + // PARAM-TODO + // virtual void register_params(ini_params & p) { + // datalog_params::register_params(p); + // p.register_bool_param("STATISTICS", m_statistics, "display statistics"); + // } }; -ini_params* g_params = 0; extra_params* g_extra_params = 0; bool g_params_initialized = false; @@ -123,12 +123,12 @@ void init_params() { if (!g_params_initialized) { z3_bound_num_procs(); g_front_end_params = new front_end_params(); - g_params = new ini_params(); + // g_params = new ini_params(); g_extra_params = new extra_params(); - register_verbosity_level(*g_params); - register_warning(*g_params); - g_front_end_params->register_params(*g_params); - g_extra_params->register_params(*g_params); + // register_verbosity_level(*g_params); + // register_warning(*g_params); + // g_front_end_params->register_params(*g_params); + // g_extra_params->register_params(*g_params); g_params_initialized = true; } } @@ -137,37 +137,11 @@ void del_params() { if (g_front_end_params != NULL) g_front_end_params->close_trace_file(); delete g_extra_params; - delete g_params; delete g_front_end_params; g_extra_params = 0; - g_params = 0; g_front_end_params = 0; } - -void read_ini_file(const char * file_name) { - std::ifstream in(file_name); - if (in.bad() || in.fail()) { - std::cerr << "Error: failed to open init file \"" << file_name << "\".\n"; - exit(ERR_INI_FILE); - } - g_params->read_ini_file(in); -} - -void display_ini_help() { - g_params->display_params(std::cout); -} - -void display_config() { - if (g_front_end_params->m_display_config) { - display_ini_help(); - } -} - -void display_ini_doc() { - g_params->display_params_documentation(std::cout); -} - void parse_cmd_line_args(int argc, char ** argv) { int i = 1; char * eq_pos = 0; @@ -285,10 +259,6 @@ void parse_cmd_line_args(int argc, char ** argv) { gparams::display(std::cout); exit(0); } - else if (strcmp(opt_name, "geninidoc") == 0) { - display_ini_doc(); - exit(0); - } #ifdef _TRACE else if (strcmp(opt_name, "tr") == 0) { if (!opt_arg) @@ -375,11 +345,6 @@ int main(int argc, char ** argv) { memory::set_high_watermark(static_cast(g_front_end_params->m_memory_high_watermark) * 1024 * 1024); memory::set_max_size(static_cast(g_front_end_params->m_memory_max_size) * 1024 * 1024); g_front_end_params->open_trace_file(); - DEBUG_CODE( - if (g_front_end_params->m_copy_params != -1) { - g_front_end_params->copy_params(g_front_end_params->m_copy_params); - TRACE("copy_params", g_params->display_params(tout);); - }); if (g_input_file && g_standard_input) { error("using standard input to read formula."); } diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp index c9dcc3fa2..759f5cee2 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/src/shell/smtlib_frontend.cpp @@ -40,7 +40,6 @@ static smtlib::solver* g_solver = 0; static cmd_context * g_cmd_context = 0; static void display_statistics() { - display_config(); clock_t end_time = clock(); if ((g_solver || g_cmd_context) && g_display_statistics) { std::cout.flush(); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 9ab21ccc5..c51a1ebc1 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3103,7 +3103,6 @@ namespace smt { m_next_progress_sample = 0; TRACE("literal_occ", display_literal_num_occs(tout);); m_timer.start(); - m_instr.start(); } void context::end_search() { @@ -3359,11 +3358,6 @@ namespace smt { return true; } - if (m_instr.is_instruction_maxed(m_fparams.m_instr_out)) { - m_last_search_failure = TIMEOUT; - return true; - } - if (m_progress_callback) { m_progress_callback->fast_progress_sample(); if (m_fparams.m_progress_sampling_freq > 0 && m_timer.ms_timeout(m_next_progress_sample + 1)) { diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 132718e9a..204a56827 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -47,7 +47,6 @@ Revision History: #include"proto_model.h" #include"model.h" #include"timer.h" -#include"instruction_count.h" #include"statistics.h" #include"progress_callback.h" @@ -77,7 +76,6 @@ namespace smt { setup m_setup; volatile bool m_cancel_flag; timer m_timer; - instruction_count m_instr; asserted_formulas m_asserted_formulas; scoped_ptr m_qmanager; scoped_ptr m_model_generator; diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index bd9196056..67c94808e 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -55,7 +55,6 @@ namespace smt { case CFG_LOGIC: setup_default(); break; case CFG_AUTO: setup_auto_config(); break; } - TRACE("setup", ini_params p; m_params.register_params(p); p.display_params(tout);); } void setup::setup_default() { diff --git a/src/test/ini_file.cpp b/src/test/ini_file.cpp deleted file mode 100644 index d3114c037..000000000 --- a/src/test/ini_file.cpp +++ /dev/null @@ -1,50 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - ini_file.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2007-05-10. - -Revision History: - ---*/ -#include -#include"ini_file.h" -#include"debug.h" - -static void tst1() { - ini_params p; - int p1; - p.register_int_param("ipar1", 0, 100, p1); - int p2; - p.register_int_param("ipar2", -100, 100, p2); - bool p3; - p.register_bool_param("bpar1", p3); - bool p4; - p.register_bool_param("bpar2", p4); - unsigned p5; - p.register_unsigned_param("upar1", 0, 100, p5); - double p6; - p.register_percentage_param("ppar1", p6); - std::istringstream in("ipar1 = 100 ipar2=-30 bpar1 = true ;; COMMENT\n bpar2 = false upar1=30 ppar1 = 10"); - p.read_ini_file(in); - SASSERT(p1 == 100); - SASSERT(p2 == -30); - SASSERT(p3); - SASSERT(!p4); - SASSERT(p5 == 30); - SASSERT(p6 == 0.1); -} - -void tst_ini_file() { - tst1(); -} - diff --git a/src/test/main.cpp b/src/test/main.cpp index acbea0761..bee889ea2 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -140,7 +140,6 @@ int main(int argc, char ** argv) { TST(diff_logic); TST(uint_set); TST_ARGV(expr_rand); - TST(ini_file); TST(list); TST(small_object_allocator); TST(timeout); diff --git a/src/util/ini_file.cpp b/src/util/ini_file.cpp deleted file mode 100644 index 48279a2ea..000000000 --- a/src/util/ini_file.cpp +++ /dev/null @@ -1,1564 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - ini_file.cpp - -Abstract: - - Configuration file support. - -Author: - - Leonardo de Moura (leonardo) 2007-05-10. - -Revision History: - ---*/ -#include"ini_file.h" -#include"util.h" -#include"trace.h" -#include"str_hashtable.h" -#include"map.h" -#include"string_buffer.h" -#include"symbol_table.h" -#include"error_codes.h" -#include - -template -class value_vector_map { - void * m_owner; - map *, ptr_hash, ptr_eq > m_mapping; - ptr_vector m_domain; - ptr_vector > m_range; - unsigned m_max_size; -public: - value_vector_map(void * owner):m_owner(owner), m_max_size(0) {} - - ~value_vector_map() { - std::for_each(m_range.begin(), m_range.end(), delete_proc >()); - } - - void insert(T * ptr, T const & value) { - SASSERT(reinterpret_cast(ptr) >= reinterpret_cast(m_owner)); - vector * vect; - if (m_mapping.find(ptr, vect)) { - vect->push_back(value); - if (vect->size() > m_max_size) - m_max_size = vect->size(); - return; - } - vect = alloc(vector); - m_range.push_back(vect); - m_domain.push_back(ptr); - vect->push_back(value); - if (m_max_size == 0) - m_max_size = 1; - m_mapping.insert(ptr, vect); - } - - void copy_params(void * curr_owner, unsigned idx) { - typename ptr_vector::iterator it = m_domain.begin(); - typename ptr_vector::iterator end = m_domain.end(); - for (; it != end; ++it) { - T * ptr = *it; - vector * vect = 0; - m_mapping.find(ptr, vect); - SASSERT(vect != 0); - if (idx < vect->size()) { - // BIG HACK - SASSERT(reinterpret_cast(ptr) >= reinterpret_cast(m_owner)); - size_t offset = reinterpret_cast(ptr) - reinterpret_cast(m_owner); - T * curr_ptr = reinterpret_cast(reinterpret_cast(curr_owner) + offset); - *curr_ptr = vect->operator[](idx); - } - } - } - - unsigned size(void) const { return m_max_size; } -}; - -struct param_vector_imp { - value_vector_map m_bool_params; - value_vector_map m_unsigned_params; - value_vector_map m_int_params; - value_vector_map m_double_params; - value_vector_map m_string_params; - value_vector_map m_symbol_params; - value_vector_map > m_symbol_list_params; - value_vector_map > m_symbol_nat_list_params; - - param_vector_imp(void * owner): - m_bool_params(owner), - m_unsigned_params(owner), - m_int_params(owner), - m_double_params(owner), - m_string_params(owner), - m_symbol_params(owner), - m_symbol_list_params(owner), - m_symbol_nat_list_params(owner) { - } - - void insert_bool_param(bool * value_ptr, bool value) { - TRACE("param_vector", tout << "insert: " << value_ptr << " -> " << value << "\n";); - m_bool_params.insert(value_ptr, value); - } - - void insert_unsigned_param(unsigned * value_ptr, unsigned value) { - TRACE("param_vector", tout << "insert: " << value_ptr << " -> " << value << "\n";); - m_unsigned_params.insert(value_ptr, value); - } - - void insert_int_param(int * value_ptr, int value) { - TRACE("param_vector", tout << "insert: " << value_ptr << " -> " << value << "\n";); - m_int_params.insert(value_ptr, value); - } - - void insert_double_param(double * value_ptr, double value) { - TRACE("param_vector", tout << "insert: " << value_ptr << " -> " << value << "\n";); - m_double_params.insert(value_ptr, value); - } - - void insert_string_param(std::string * value_ptr, std::string const & value) { - TRACE("param_vector", tout << "insert: " << value_ptr << " -> " << value << "\n";); - m_string_params.insert(value_ptr, value); - } - - void insert_symbol_param(symbol * value_ptr, symbol const & value) { - TRACE("param_vector", tout << "insert: " << value_ptr << " -> " << value << "\n";); - m_symbol_params.insert(value_ptr, value); - } - - void insert_symbol_list_param(svector * value_ptr, svector const & value) { - TRACE("param_vector", tout << "insert: " << value_ptr << " -> "; display(tout, value.begin(), value.end()); tout << "\n";); - m_symbol_list_params.insert(value_ptr, value); - } - - void insert_symbol_nat_list_param(svector * value_ptr, svector const & value) { - TRACE("param_vector", tout << "insert: " << value_ptr << " -> "; display(tout, value.begin(), value.end()); tout << "\n";); - m_symbol_nat_list_params.insert(value_ptr, value); - } - - void copy_params(void * curr_owner, unsigned idx) { - m_bool_params.copy_params(curr_owner, idx); - m_unsigned_params.copy_params(curr_owner, idx); - m_int_params.copy_params(curr_owner, idx); - m_double_params.copy_params(curr_owner, idx); - m_string_params.copy_params(curr_owner, idx); - m_symbol_params.copy_params(curr_owner, idx); - m_symbol_list_params.copy_params(curr_owner, idx); - m_symbol_nat_list_params.copy_params(curr_owner, idx); - } - - unsigned size(void) const { - unsigned ret = 0; - ret = std::max(ret, m_bool_params.size()); - ret = std::max(ret, m_unsigned_params.size()); - ret = std::max(ret, m_int_params.size()); - ret = std::max(ret, m_double_params.size()); - ret = std::max(ret, m_string_params.size()); - ret = std::max(ret, m_symbol_params.size()); - ret = std::max(ret, m_symbol_list_params.size()); - ret = std::max(ret, m_symbol_nat_list_params.size()); - return ret; - } -}; - - -param_vector::param_vector(void * owner): - m_ref_count(0) { - m_imp = alloc(param_vector_imp, owner); -} - -param_vector::~param_vector() { - dealloc(m_imp); -} - -void param_vector::inc_ref() { - m_ref_count++; -} - -void param_vector::dec_ref() { - SASSERT(m_ref_count > 0); - m_ref_count--; - if (m_ref_count == 0) - dealloc(this); -} - -void param_vector::copy_params(void * curr_owner, unsigned idx) { - m_imp->copy_params(curr_owner, idx); -} - -unsigned param_vector::size(void) const -{ - return m_imp->size(); -} - -enum itoken { - ITK_NULL, ITK_ID, ITK_NUM, ITK_DOUBLE, ITK_STRING, ITK_BAD_STRING, ITK_TRUE, ITK_FALSE, ITK_COMMA, ITK_LP, ITK_RP, ITK_LCB, ITK_RCB, ITK_CLN, ITK_EQ, ITK_BAD_ID, ITK_EOS, ITK_LAST -}; - -class ini_reserved_symbols { - typedef map str2token; - str2token m_str2token; - -public: - ini_reserved_symbols() { - m_str2token.insert("true", ITK_TRUE); - m_str2token.insert("false", ITK_FALSE); - } - - itoken string2itoken(char const * str) { - str2token::entry * e = m_str2token.find_core(const_cast(str)); - if (e) - return e->get_data().m_value; - else - return ITK_ID; - } -}; - -static char const * g_itoken2string[] = { - "", - "", - "", - "", - "", - "", - "true", - "false", - ",", - "(", - ")", - "{", - "}", - ":", - "=", - "", - "" -}; - -COMPILE_TIME_ASSERT(sizeof(g_itoken2string)/sizeof(char const*) == ITK_LAST); - -inline static const char * itoken2string(itoken t) { - return g_itoken2string[t]; -} - -inline itoken string2itoken(ini_reserved_symbols& reserved, char const * str) { - itoken r = reserved.string2itoken(str); - TRACE("token", tout << str << " -> " << itoken2string(r) << "\n";); - return r; -} - -class ini_lexer { - std::istream & m_input; - char m_curr_char; - int m_line; - int m_pos; - int m_tok_pos; - string_buffer<> m_buffer; - ini_reserved_symbols m_ini_reserved; -public: - bool eos() const { - return m_curr_char == EOF; - } - - void next() { - m_curr_char = m_input.get(); - m_pos++; - } - - void save_and_next() { - m_buffer << m_curr_char; - next(); - } - - ini_lexer(std::istream & input): - m_input(input), - m_line(1), - m_pos(0), - m_tok_pos(0), - m_ini_reserved() { - next(); - } - - itoken read_num() { - while (isdigit(m_curr_char)) { - save_and_next(); - } - if (m_curr_char == '.') { - save_and_next(); - while (isdigit(m_curr_char)) { - save_and_next(); - } - if (m_curr_char == 'e' || m_curr_char == 'E' || m_curr_char == 'd' || m_curr_char == 'D') { - save_and_next(); - if (m_curr_char == '-') { - save_and_next(); - } - while (isdigit(m_curr_char)) { - save_and_next(); - } - } - return ITK_DOUBLE; - } - return ITK_NUM; - } - - itoken read_id() { - while (!eos() && (isalpha(m_curr_char) || isdigit(m_curr_char) || m_curr_char == '_')) { - save_and_next(); - } - return string2itoken(m_ini_reserved, m_buffer.c_str()); - } - - itoken read_string() { - m_tok_pos = m_pos; - next(); - while (m_curr_char != '"' && m_curr_char != '\'') { - if (m_input.eof()) { - return ITK_BAD_STRING; - } - if (m_curr_char == '\n') { - return ITK_BAD_STRING; - } - if (m_curr_char == '\\') { - next(); // do not save the '\' - switch (m_curr_char) { - case 't': - m_buffer << '\t'; - next(); - break; - case 'n': - m_buffer << '\n'; - next(); - break; - case '\n': - m_buffer << '\n'; - next(); - break; - default: - if (!isdigit(m_curr_char)) { - save_and_next(); /* handles \\, \", \', and \? */ - } - else { /* \xxx */ - int c = 0; - int i = 0; - do { - c = 10*c + (m_curr_char-'0'); - next(); - } - while (++i<3 && isdigit(m_curr_char)); - if (c > UCHAR_MAX) { - return ITK_BAD_STRING; - } - m_buffer << static_cast(c); - } - } - } - else { - save_and_next(); - } - } - next(); - return ITK_STRING; - } - - itoken next_token() { - for(;;) { - if (eos()) { - return ITK_EOS; - } - - m_buffer.reset(); - switch (m_curr_char) { - case ';': // comment - while (m_curr_char != '\n' && !eos()) { - next(); - } - break; - case '\n': - next(); - m_line++; - break; - case '=': - m_tok_pos = m_pos; - next(); - return ITK_EQ; - case '\'': - case '\"': - return read_string(); - case '{': - m_tok_pos = m_pos; - next(); - return ITK_LCB; - case '}': - m_tok_pos = m_pos; - next(); - return ITK_RCB; - case '(': - m_tok_pos = m_pos; - next(); - return ITK_LP; - case ')': - m_tok_pos = m_pos; - next(); - return ITK_RP; - case ',': - m_tok_pos = m_pos; - next(); - return ITK_COMMA; - case ':': - m_tok_pos = m_pos; - next(); - return ITK_CLN; - default: - if (isspace(m_curr_char)) { - next(); - break; - } - else if (isdigit(m_curr_char)) { - m_tok_pos = m_pos; - save_and_next(); - return read_num(); - } - else { - char old = m_curr_char; - m_tok_pos = m_pos; - save_and_next(); - TRACE("ini_lexer", tout << "old: " << static_cast(old) << " " << old << "\n";); - if (old == '-' && isdigit(m_curr_char)) { - return read_num(); - } - else if (old == '_' || isalpha(old)) { - return read_id(); - } - else { - return ITK_BAD_ID; - } - } - } - } - } - - char const * get_token_data() const { - return m_buffer.c_str(); - } - - unsigned get_token_pos() const { - return m_tok_pos; - } -}; - - -enum ini_param_kind { - IPK_BOOL, - IPK_INT, - IPK_UNSIGNED, - IPK_DOUBLE, - IPK_PERCENTAGE, - IPK_STRING, - IPK_SYMBOL, - IPK_SYMBOL_LIST, - IPK_SYMBOL_NAT_LIST -}; - - -struct ini_param_info { - ini_param_kind m_kind; - bool m_is_mutable; - - char const * m_description; - union { - struct { - int m_int_min; - int m_int_max; - int * m_int_val; - }; - struct { - unsigned m_uint_min; - unsigned m_uint_max; - unsigned * m_uint_val; - }; - bool * m_bool_val; - double * m_double_val; - double * m_perc_val; - symbol * m_sym_val; - std::string * m_str_val; - svector * m_sym_list_val; - svector * m_sym_nat_list_val; - }; - - ini_param_info(char const * descr = 0): - m_kind(IPK_BOOL), - m_is_mutable(false), - m_description(descr), - m_bool_val(0) { - } - - ini_param_info(int min, int max, int * val, char const * descr, bool is_mutable): - m_kind(IPK_INT), - m_is_mutable(is_mutable), - m_description(descr), - m_int_min(min), - m_int_max(max), - m_int_val(val) { - } - - ini_param_info(unsigned min, unsigned max, unsigned * val, char const * descr, bool is_mutable): - m_kind(IPK_UNSIGNED), - m_is_mutable(is_mutable), - m_description(descr), - m_uint_min(min), - m_uint_max(max), - m_uint_val(val) { - } - - ini_param_info(bool * val, char const * descr, bool is_mutable): - m_kind(IPK_BOOL), - m_is_mutable(is_mutable), - m_description(descr), - m_bool_val(val) { - } - - ini_param_info(bool perc, double * val, char const * descr, bool is_mutable): - m_kind(perc ? IPK_PERCENTAGE : IPK_DOUBLE), - m_is_mutable(is_mutable), - m_description(descr), - m_perc_val(val) { - } - - ini_param_info(svector * val, char const * descr, bool is_mutable): - m_kind(IPK_SYMBOL_LIST), - m_is_mutable(is_mutable), - m_description(descr), - m_sym_list_val(val) { - } - - ini_param_info(svector * val, char const * descr, bool is_mutable): - m_kind(IPK_SYMBOL_NAT_LIST), - m_is_mutable(is_mutable), - m_description(descr), - m_sym_nat_list_val(val) { - } - - ini_param_info(symbol * s, char const * descr, bool is_mutable): - m_kind(IPK_SYMBOL), - m_is_mutable(is_mutable), - m_description(descr), - m_sym_val(s) { - } - - ini_param_info(std::string * str, char const * descr, bool is_mutable): - m_kind(IPK_STRING), - m_is_mutable(is_mutable), - m_description(descr), - m_str_val(str) { - } - -}; - -struct ini_params_imp { - bool m_abort_on_error; - ini_reserved_symbols m_ini_reserved; - ref m_param_vector; - symbol_table m_param_info; - bool m_is_frozen; - - ini_params_imp(bool abort_on_error): m_abort_on_error(abort_on_error), m_is_frozen(false) {} - - void freeze(bool f) { m_is_frozen = f; } - - void register_param_vector(param_vector * pv) { - m_param_vector = pv; - } - - void register_bool_param(symbol param_name, bool & value, char const * descr, bool is_mutable) { - SASSERT(!m_param_info.contains(param_name)); - m_param_info.insert(param_name, ini_param_info(&value, descr, is_mutable)); - } - - void register_unsigned_param(symbol param_name, unsigned min, unsigned max, unsigned & value, char const * descr, bool is_mutable) { - SASSERT(!m_param_info.contains(param_name)); - m_param_info.insert(param_name, ini_param_info(min, max, &value, descr, is_mutable)); - } - - void register_int_param(symbol param_name, int min, int max, int & value, char const * descr, bool is_mutable) { - SASSERT(!m_param_info.contains(param_name)); - m_param_info.insert(param_name, ini_param_info(min, max, &value, descr, is_mutable)); - } - - void register_percentage_param(symbol param_name, double & value, char const * descr, bool is_mutable) { - SASSERT(!m_param_info.contains(param_name)); - m_param_info.insert(param_name, ini_param_info(true, &value, descr, is_mutable)); - } - - void register_double_param(symbol param_name, double & value, char const * descr, bool is_mutable) { - SASSERT(!m_param_info.contains(param_name)); - m_param_info.insert(param_name, ini_param_info(false, &value, descr, is_mutable)); - } - - void register_string_param(symbol param_name, std::string & value, char const * descr, bool is_mutable) { - SASSERT(!m_param_info.contains(param_name)); - m_param_info.insert(param_name, ini_param_info(&value, descr, is_mutable)); - } - - void register_symbol_param(symbol param_name, symbol & value, char const * descr, bool is_mutable) { - SASSERT(!m_param_info.contains(param_name)); - m_param_info.insert(param_name, ini_param_info(&value, descr, is_mutable)); - } - - void register_symbol_list_param(symbol param_name, svector & value, char const * descr, bool is_mutable) { - SASSERT(!m_param_info.contains(param_name)); - m_param_info.insert(param_name, ini_param_info(&value, descr, is_mutable)); - } - - void register_symbol_nat_list_param(symbol param_name, svector & value, char const * descr, bool is_mutable) { - SASSERT(!m_param_info.contains(param_name)); - m_param_info.insert(param_name, ini_param_info(&value, descr, is_mutable)); - } - - struct symbol_lt_proc { - bool operator()(const symbol & s1, const symbol & s2) const { - return strcmp(s1.bare_str(), s2.bare_str()) < 0; - } - }; - - void display_param_help(char const* param_id, std::ostream& out) const { - ini_param_info info; - if (m_param_info.find(symbol(param_id), info)) { - display_param_info(out, info); - } - else { - out << "option " << param_id << " does not exist"; - } - } - - void display_param_info(std::ostream& out, ini_param_info& info) const { - switch (info.m_kind) { - case IPK_BOOL: - out << " boolean"; - out << ", default: " << (*info.m_bool_val ? "true" : "false"); - break; - case IPK_INT: - out << " integer"; - if (info.m_int_min > INT_MIN) { - out << ", min: " << info.m_int_min; - } - if (info.m_int_max < INT_MAX) { - out << ", max: " << info.m_int_max; - } - out << ", default: " << *info.m_int_val; - break; - case IPK_UNSIGNED: - out << " unsigned integer"; - if (info.m_uint_min > 0) { - out << ", min: " << info.m_uint_min; - } - if (info.m_uint_max < INT_MAX) { - out << ", max: " << info.m_uint_max; - } - out << ", default: " << *info.m_uint_val; - break; - case IPK_DOUBLE: - out << " double"; - out << ", default: " << *info.m_double_val; - break; - case IPK_PERCENTAGE: - out << " percentage"; - out << ", default: " << *info.m_perc_val; - break; - case IPK_SYMBOL: - out << " symbol"; - out << ", default: " << *info.m_sym_val; - break; - case IPK_STRING: - out << " string"; - out << ", default: " << *info.m_str_val; - break; - case IPK_SYMBOL_LIST: - out << " list of symbols (strings)"; - break; - case IPK_SYMBOL_NAT_LIST: - out << " list of pairs: symbols(strings) x unsigned"; - break; - } - if (info.m_description) { - out << ", " << info.m_description << "."; - } - out << "\n"; - } - - void display_params(std::ostream & out) const { - svector params; - m_param_info.get_dom(params); - std::sort(params.begin(), params.end(), symbol_lt_proc()); - svector::iterator it = params.begin(); - svector::iterator end = params.end(); - for (; it != end; ++it) { - out << *it << ":"; - ini_param_info info; - m_param_info.find(*it, info); - display_param_info(out, info); - } - } - - void display_params_documentation(std::ostream & out) const { - out << "// AUTOMATICALLY GENERATED FILE - DO NOT EDIT\n\n" - << "/**\n" - << " \\page config INI parameters\n\n"; - svector params; - m_param_info.get_dom(params); - std::sort(params.begin(), params.end(), symbol_lt_proc()); - svector::iterator it = params.begin(); - svector::iterator end = params.end(); - for (; it != end; ++it) { - out << "- \\c " << *it << ":"; - ini_param_info info; - m_param_info.find(*it, info); - switch (info.m_kind) { - case IPK_BOOL: - out << " \\em boolean"; - out << ", default: " << (*info.m_bool_val ? "\\c true" : "\\c false"); - break; - case IPK_INT: - out << " \\em integer"; - if (info.m_int_min > INT_MIN) { - out << ", min: \\c " << info.m_int_min; - } - if (info.m_int_max < INT_MAX) { - out << ", max: \\c " << info.m_int_max; - } - out << ", default: \\c " << *info.m_int_val; - break; - case IPK_UNSIGNED: - out << " \\em unsigned \\em integer"; - if (info.m_uint_min > 0) { - out << ", min: \\c " << info.m_uint_min; - } - if (info.m_uint_max < INT_MAX) { - out << ", max: \\c " << info.m_uint_max; - } - out << ", default: \\c " << *info.m_uint_val; - break; - case IPK_DOUBLE: - out << " \\em double"; - out << ", default: \\c " << *info.m_double_val; - break; - case IPK_PERCENTAGE: - out << " \\em percentage"; - out << ", default: \\c " << *info.m_perc_val; - break; - case IPK_STRING: - out << " \\em string"; - out << ", default: " << *info.m_str_val; - break; - case IPK_SYMBOL: - out << " \\em symbol"; - out << ", default: " << *info.m_sym_val; - break; - case IPK_SYMBOL_LIST: - out << " \\em list \\em of \\em symbols \\em (strings)"; - break; - case IPK_SYMBOL_NAT_LIST: - out << " \\em list \\em of \\em pairs: \\em symbols(strings) \\em x \\em unsigned"; - break; - } - if (info.m_description) { - out << ", " << info.m_description << "."; - } - out << "\n\n"; - } - out << "*/\n"; - } - - void error(char const * param_id, char const * msg) { - if (m_abort_on_error) { - verbose_stream() << "Error setting '" << param_id << "', reason: " << msg << "\n"; - throw z3_error(ERR_INI_FILE); - } - else { - throw set_get_param_exception(param_id, msg); - } - } - - symbol trim(char const * param_id) { - string_buffer<> m_buffer; - while (*param_id != 0 && !isspace(*param_id)) { - m_buffer.append(*param_id); - param_id++; - } - return symbol(m_buffer.c_str()); - } - - void set_param_value(char const * param_id, char const * param_value) { - TRACE("param_value", tout << param_id << " " << param_value << "\n";); - if (param_value == 0) { - error(param_id, "invalid (null) option"); - } - symbol s(param_id); - ini_param_info info; - if (!m_param_info.find(s, info)) { - s = trim(param_id); - if (!m_param_info.find(s, info)) - error(param_id, "unknown option."); - } - if (!info.m_is_mutable && m_is_frozen) { - error(param_id, "option value cannot be modified after initialization"); - } - switch (info.m_kind) { - case IPK_BOOL: - parse_bool_param(param_id, info, param_value); - break; - case IPK_INT: - parse_int_param(param_id, info, param_value); - break; - case IPK_UNSIGNED: - parse_uint_param(param_id, info, param_value); - break; - case IPK_DOUBLE: - parse_double_param(param_id, info, param_value); - break; - case IPK_PERCENTAGE: - parse_perc_param(param_id, info, param_value); - break; - case IPK_STRING: - parse_string_param(param_id, info, param_value); - break; - case IPK_SYMBOL: - // TODO: not used so far - *info.m_sym_val = param_value; - break; - case IPK_SYMBOL_LIST: - error(param_id, "this option can only be set in an INI file"); - break; - case IPK_SYMBOL_NAT_LIST: - error(param_id, "this option can only be set in an INI file"); - break; - default: - UNREACHABLE(); - } - } - - - bool get_param_value(char const * param_id, std::string& param_value) { - TRACE("param_value", tout << param_id << "\n";); - std::ostringstream buffer; - symbol s(param_id); - ini_param_info info; - if (!m_param_info.find(s, info)) { - s = trim(param_id); - if (!m_param_info.find(s, info)) { - return false; - } - } - switch (info.m_kind) { - case IPK_BOOL: - buffer << ((*info.m_bool_val)?"true":"false"); - break; - case IPK_INT: - buffer << (*info.m_int_val); - break; - case IPK_UNSIGNED: - buffer << (*info.m_uint_val); - break; - case IPK_DOUBLE: - buffer << (*info.m_double_val); - break; - case IPK_PERCENTAGE: - buffer << (*info.m_perc_val); - break; - case IPK_STRING: - buffer << (*info.m_str_val); - break; - case IPK_SYMBOL: - buffer << (info.m_sym_val->str()); - break; - case IPK_SYMBOL_LIST: - error(param_id, "this option cannot be retrieved"); - break; - case IPK_SYMBOL_NAT_LIST: - error(param_id, "this option cannot be retrieved"); - break; - default: - UNREACHABLE(); - } - param_value = buffer.str(); - return true; - } - - string_buffer<> m_buffer; - - char const * get_token_data() const { - return m_buffer.c_str(); - } - - void save_and_next(char const * & in) { - m_buffer.append(*in); - ++in; - } - - itoken read_num(char const * & in) { - while (isdigit(*in)) { - save_and_next(in); - } - TRACE("read_num", tout << "1. read_num: " << m_buffer.c_str() << ", *in: " << *in << "\n";); - if (*in == '.') { - save_and_next(in); - while (isdigit(*in)) { - save_and_next(in); - } - TRACE("read_num", tout << "2. read_num: " << m_buffer.c_str() << ", *in: " << *in << "\n";); - if (*in == 'e' || *in == 'E' || *in == 'd' || *in == 'D') { - save_and_next(in); - if (*in == '-') { - save_and_next(in); - } - while (isdigit(*in)) { - save_and_next(in); - } - } - return ITK_DOUBLE; - } - return ITK_NUM; - } - - itoken read_id(char const * & in) { - while (!*in == 0 && (isalpha(*in) || isdigit(*in) || *in == '_')) { - save_and_next(in); - } - return string2itoken(m_ini_reserved, m_buffer.c_str()); - } - - itoken read_string(char const * & in) { - ++in; - while (*in != '"' && *in != '\'') { - TRACE("read_string", tout << *in << "\n";); - if (*in == 0) - return ITK_BAD_STRING; - if (*in == '\n') - return ITK_BAD_STRING; - if (*in == '\\') { - ++in; - switch (*in) { - case 't': - m_buffer << '\t'; - ++in; - break; - case 'n': - m_buffer << '\n'; - ++in; - break; - case '\n': - m_buffer << '\n'; - ++in; - break; - default: - if (!isdigit(*in)) { - save_and_next(in); /* handles \\, \", \', and \? */ - } - else { /* \xxx */ - int c = 0; - int i = 0; - do { - c = 10*c + (*in-'0'); - ++in; - } - while (++i<3 && isdigit(*in)); - if (c > UCHAR_MAX) - return ITK_BAD_STRING; - m_buffer << static_cast(c); - } - } - } - else { - save_and_next(in); - } - } - ++in; - return ITK_STRING; - } - - itoken next_token(char const * & in) { - for(;;) { - if (*in == 0) - return ITK_EOS; - m_buffer.reset(); - switch (*in) { - case '{': - in++; - return ITK_LCB; - case '}': - in++; - return ITK_RCB; - case ',': - in++; - return ITK_COMMA; - case '"': - case '\'': - TRACE("read_string", tout << "found \"\n";); - return read_string(in); - default: - if (isspace(*in)) { - in++; - break; - } - else if (isdigit(*in)) { - TRACE("read_num", tout << "found is_digit\n";); - return read_num(in); - } - else { - char old = *in; - save_and_next(in); - if (old == '-' && isdigit(*in)) { - return read_num(in); - } - else if (old == '_' || isalpha(old)) { - return read_id(in); - } - else { - return ITK_BAD_ID; - } - } - } - } - } - - bool end_of_list(char const * param_id, char const * & param_value) { - switch (next_token(param_value)) { - case ITK_COMMA: - return false; - case ITK_RCB: - return true; - default: - error(param_id, "boolean value (true/false) expected"); - } - return false; - } - - void parse_bool_param(char const * param_id, ini_param_info & info, char const * param_value) { - switch (next_token(param_value)) { - case ITK_TRUE: - *info.m_bool_val = true; - break; - case ITK_FALSE: - *info.m_bool_val = false; - break; - default: - error(param_id, "boolean value (true/false) expected"); - } - if (m_param_vector.get() && next_token(param_value) == ITK_LCB) { - for (;;) { - switch (next_token(param_value)) { - case ITK_TRUE: - m_param_vector->m_imp->insert_bool_param(info.m_bool_val, true); - break; - case ITK_FALSE: - m_param_vector->m_imp->insert_bool_param(info.m_bool_val, false); - break; - default: - error(param_id, "boolean value (true/false) expected"); - } - if (end_of_list(param_id, param_value)) - return; - } - } - } - - void parse_int_param(char const * param_id, ini_param_info & info, char const * param_value) { - if (next_token(param_value) != ITK_NUM) - error(param_id, "integer expected"); - int val = strtol(get_token_data(), 0, 10); - if (val < info.m_int_min || val > info.m_int_max) - error(param_id, "integer out of bounds"); - *info.m_int_val = val; - if (m_param_vector.get() && next_token(param_value) == ITK_LCB) { - for (;;) { - if (next_token(param_value) != ITK_NUM) - error(param_id, "integer expected"); - int val = strtol(get_token_data(), 0, 10); - if (val < info.m_int_min || val > info.m_int_max) - error(param_id, "integer out of bounds"); - m_param_vector->m_imp->insert_int_param(info.m_int_val, val); - if (end_of_list(param_id, param_value)) - return; - } - } - } - - void parse_uint_param(char const * param_id, ini_param_info & info, char const * param_value) { - if (next_token(param_value) != ITK_NUM) - error(param_id, "integer expected"); - unsigned val = static_cast(strtol(get_token_data(), 0, 10)); - - if (val < info.m_uint_min || val > info.m_uint_max) - error(param_id, "unsigned out of bounds"); - *info.m_uint_val = val; - if (m_param_vector.get() && next_token(param_value) == ITK_LCB) { - for (;;) { - if (next_token(param_value) != ITK_NUM) - error(param_id, "integer expected"); - unsigned val = static_cast(strtol(get_token_data(), 0, 10)); - if (val < info.m_uint_min || val > info.m_uint_max) - error(param_id, "unsigned out of bounds"); - m_param_vector->m_imp->insert_unsigned_param(info.m_uint_val, val); - if (end_of_list(param_id, param_value)) - return; - } - } - } - - void parse_double_param(char const * param_id, ini_param_info & info, char const * param_value) { - itoken k = next_token(param_value); - if (k != ITK_NUM && k != ITK_DOUBLE) - error(param_id, "float expected"); - char * aux; - *info.m_double_val = strtod(get_token_data(), &aux); - if (m_param_vector.get() && next_token(param_value) == ITK_LCB) { - for (;;) { - k = next_token(param_value); - if (k != ITK_NUM && k != ITK_DOUBLE) - error(param_id, "float expected"); - m_param_vector->m_imp->insert_double_param(info.m_double_val, strtod(get_token_data(), &aux)); - if (end_of_list(param_id, param_value)) - return; - } - } - } - - void parse_perc_param(char const * param_id, ini_param_info & info, char const * param_value) { - if (next_token(param_value) != ITK_NUM) - error(param_id, "integer expected"); - int val = strtol(get_token_data(), 0, 10); - if (val < 0 || val > 100) - error(param_id, "integer between 0 and 100 expected"); - *info.m_perc_val = static_cast(val)/100.0; - if (m_param_vector.get() && next_token(param_value) == ITK_LCB) { - for (;;) { - if (next_token(param_value) != ITK_NUM) - error(param_id, "integer expected"); - int val = strtol(get_token_data(), 0, 10); - if (val < 0 || val > 100) - error(param_id, "integer between 0 and 100 expected"); - m_param_vector->m_imp->insert_double_param(info.m_perc_val, static_cast(val)/100.0); - if (end_of_list(param_id, param_value)) - return; - } - } - } - - void parse_string_param(char const * param_id, ini_param_info & info, char const * param_value) { - if (next_token(param_value) != ITK_STRING) - error(param_id, "string expected"); - *info.m_str_val = get_token_data(); - if (m_param_vector.get() && next_token(param_value) == ITK_LCB) { - for (;;) { - if (next_token(param_value) != ITK_STRING) - error(param_id, "string expected"); - m_param_vector->m_imp->insert_string_param(info.m_str_val, get_token_data()); - if (end_of_list(param_id, param_value)) - return; - } - } - } -}; - -class ini_parser { - ini_lexer m_lexer; - ini_params_imp * m_params; - itoken m_curr_token; - - void error(unsigned pos, char const * msg) { - if (m_params->m_abort_on_error) { - verbose_stream() << "Error INI file [position: " << pos << "]: " << msg << "\n"; - throw z3_error(ERR_INI_FILE); - } - else { - throw ini_parser_exception(pos, msg); - } - } - - void error(char const * msg) { - error(m_lexer.get_token_pos(), msg); - } - - itoken get_curr_token() { - if (m_curr_token == ITK_NULL) { - m_curr_token = m_lexer.next_token(); - } - SASSERT(m_curr_token != ITK_NULL); - return m_curr_token; - } - - void next() { - if (m_curr_token == ITK_NULL) { - m_lexer.next_token(); - } - else { - m_curr_token = ITK_NULL; - } - } - - char const * get_token_data() { - if (m_curr_token == ITK_NULL) { - get_curr_token(); - } - SASSERT(m_curr_token != ITK_NULL); - return m_lexer.get_token_data(); - } - - bool test_next(itoken expected) { - if (get_curr_token() == expected) { - next(); - return true; - } - else { - return false; - } - } - - void check(itoken expected) { - if (!test_next(expected)) { - string_buffer<> msg; - msg << "unexpected token '" << itoken2string(get_curr_token()) - << "', '" << itoken2string(expected) << "' expected."; - error(msg.c_str()); - } - } - -public: - ini_parser(std::istream & in, ini_params_imp * p): - m_lexer(in), - m_params(p), - m_curr_token(ITK_NULL) { - } - - void parse_param() { - symbol s(get_token_data()); - check(ITK_ID); - ini_param_info info; - if (!m_params->m_param_info.find(s, info)) { - error("unknown option."); - } - check(ITK_EQ); - switch (info.m_kind) { - case IPK_BOOL: - parse_bool_param(info); - break; - case IPK_INT: - parse_int_param(info); - break; - case IPK_UNSIGNED: - parse_uint_param(info); - break; - case IPK_DOUBLE: - parse_double_param(info); - break; - case IPK_PERCENTAGE: - parse_perc_param(info); - break; - case IPK_STRING: - parse_string_param(info); - break; - case IPK_SYMBOL: - // TODO: add support for VAL{VAL,...,VAL} - *info.m_sym_val = get_token_data(); - check(ITK_STRING); - break; - case IPK_SYMBOL_NAT_LIST: - parse_symbol_nat_list(info); - break; - case IPK_SYMBOL_LIST: - parse_symbol_list(info); - break; - default: - UNREACHABLE(); - } - } - - bool end_of_list() { - switch (get_curr_token()) { - case ITK_COMMA: - next(); - return false; - case ITK_RCB: - next(); - return true; - default: - error("boolean value expected"); - } - return false; - } - - void parse_bool_param(ini_param_info & info) { - if (get_curr_token() != ITK_TRUE && get_curr_token() != ITK_FALSE) - error("boolean value expected"); - *info.m_bool_val = get_curr_token() == ITK_TRUE; - next(); - if (m_params->m_param_vector.get() && get_curr_token() == ITK_LCB) { - next(); - for (;;) { - if (get_curr_token() != ITK_TRUE && get_curr_token() != ITK_FALSE) - error("boolean value expected"); - m_params->m_param_vector->m_imp->insert_bool_param(info.m_bool_val, get_curr_token() == ITK_TRUE); - next(); - if (end_of_list()) - return; - } - } - } - - void parse_int_param(ini_param_info & info) { - if (get_curr_token() != ITK_NUM) - error("integer expected"); - int val = strtol(get_token_data(), 0, 10); - if (val < info.m_int_min || val > info.m_int_max) - error("integer out of bounds"); - *info.m_int_val = val; - next(); - TRACE("int_param", tout << "val: " << val << "\n";); - if (m_params->m_param_vector.get() && get_curr_token() == ITK_LCB) { - next(); - for (;;) { - if (get_curr_token() != ITK_NUM) - error("integer expected"); - int val = strtol(get_token_data(), 0, 10); - if (val < info.m_int_min || val > info.m_int_max) - error("integer out of bounds"); - m_params->m_param_vector->m_imp->insert_int_param(info.m_int_val, val); - next(); - if (end_of_list()) - return; - } - } - } - - void parse_uint_param(ini_param_info & info) { - if (get_curr_token() != ITK_NUM) - error("integer expected"); - long val = strtol(get_token_data(), 0, 10); - if (val < static_cast(info.m_uint_min) || val > static_cast(info.m_uint_max)) - error("integer out of bounds"); - *info.m_uint_val = val; - next(); - if (m_params->m_param_vector.get() && get_curr_token() == ITK_LCB) { - next(); - for (;;) { - if (get_curr_token() != ITK_NUM) - error("integer expected"); - long val = strtol(get_token_data(), 0, 10); - if (val < static_cast(info.m_uint_min) || val > static_cast(info.m_uint_max)) - error("integer out of bounds"); - m_params->m_param_vector->m_imp->insert_unsigned_param(info.m_uint_val, val); - next(); - if (end_of_list()) - return; - } - } - } - - void parse_double_param(ini_param_info & info) { - if (get_curr_token() != ITK_NUM && get_curr_token() != ITK_DOUBLE) - error("float expected"); - char * aux; - *info.m_double_val = strtod(get_token_data(), &aux); - next(); - if (m_params->m_param_vector.get() && get_curr_token() == ITK_LCB) { - next(); - for (;;) { - if (get_curr_token() != ITK_NUM && get_curr_token() != ITK_DOUBLE) - error("float expected"); - m_params->m_param_vector->m_imp->insert_double_param(info.m_double_val, strtod(get_token_data(), &aux)); - next(); - if (end_of_list()) - return; - } - } - } - - void parse_perc_param(ini_param_info & info) { - if (get_curr_token() != ITK_NUM) - error("integer expected"); - int val = strtol(get_token_data(), 0, 10); - if (val < 0 || val > 100) - error("integer between 0 and 100 expected"); - *info.m_perc_val = static_cast(val)/100.0; - next(); - if (m_params->m_param_vector.get() && get_curr_token() == ITK_LCB) { - next(); - for (;;) { - if (get_curr_token() != ITK_NUM) - error("integer expected"); - int val = strtol(get_token_data(), 0, 10); - if (val < 0 || val > 100) - error("integer between 0 and 100 expected"); - m_params->m_param_vector->m_imp->insert_double_param(info.m_perc_val, static_cast(val)/100.0); - next(); - if (end_of_list()) - return; - } - } - } - - void parse_string_param(ini_param_info & info) { - if (get_curr_token() != ITK_STRING) - error("string expected"); - *info.m_str_val = get_token_data(); - next(); - if (m_params->m_param_vector.get() && get_curr_token() == ITK_LCB) { - next(); - for (;;) { - if (get_curr_token() != ITK_STRING) - error("string expected"); - m_params->m_param_vector->m_imp->insert_string_param(info.m_str_val, get_token_data()); - next(); - if (end_of_list()) - return; - } - } - } - - void parse_s_list(svector & result) { - check(ITK_LP); - for (;;) { - symbol s(get_token_data()); - result.push_back(s); - check(ITK_ID); - if (!test_next(ITK_COMMA)) { - check(ITK_RP); - return; - } - } - } - - void parse_symbol_list(ini_param_info & info) { - parse_s_list(*(info.m_sym_list_val)); - if (m_params->m_param_vector.get() && test_next(ITK_LCB)) { - for (;;) { - svector lst; - parse_s_list(lst); - m_params->m_param_vector->m_imp->insert_symbol_list_param(info.m_sym_list_val, lst); - if (!test_next(ITK_COMMA)) { - check(ITK_RCB); - return; - } - } - } - } - - void parse_sn_list(svector & result) { - check(ITK_LP); - for (;;) { - symbol s(get_token_data()); - check(ITK_ID); - check(ITK_CLN); - unsigned val = strtol(get_token_data(), 0, 10); - check(ITK_NUM); - result.push_back(std::make_pair(s, val)); - if (!test_next(ITK_COMMA)) { - check(ITK_RP); - return; - } - } - } - - void parse_symbol_nat_list(ini_param_info & info) { - parse_sn_list(*(info.m_sym_nat_list_val)); - if (m_params->m_param_vector.get() && test_next(ITK_LCB)) { - for (;;) { - svector lst; - parse_sn_list(lst); - m_params->m_param_vector->m_imp->insert_symbol_nat_list_param(info.m_sym_nat_list_val, lst); - if (!test_next(ITK_COMMA)) { - check(ITK_RCB); - return; - } - } - } - } - - void parse() { - while (get_curr_token() != ITK_EOS) { - parse_param(); - } - } -}; - -ini_params::ini_params(bool abort_on_error) { - m_imp = alloc(ini_params_imp, abort_on_error); -} - -ini_params::~ini_params() { - dealloc(m_imp); -} - -void ini_params::register_bool_param(char const * param_name, bool & value, char const * descr, bool is_mutable) { - m_imp->register_bool_param(symbol(param_name), value, descr, is_mutable); -} - -void ini_params::register_unsigned_param(char const * param_name, unsigned min, unsigned max, unsigned & value, char const * descr, bool is_mutable) { - m_imp->register_unsigned_param(symbol(param_name), min, max, value, descr, is_mutable); -} - -void ini_params::register_int_param(char const * param_name, int min, int max, int & value, char const * descr, bool is_mutable) { - m_imp->register_int_param(symbol(param_name), min, max, value, descr, is_mutable); -} - -void ini_params::register_double_param(char const * param_name, double & value, char const * descr, bool is_mutable) { - m_imp->register_double_param(symbol(param_name), value, descr, is_mutable); -} - -void ini_params::register_percentage_param(char const * param_name, double & value, char const * descr, bool is_mutable) { - m_imp->register_percentage_param(symbol(param_name), value, descr, is_mutable); -} - -void ini_params::register_string_param(char const * param_name, std::string & value, char const * descr, bool is_mutable) { - m_imp->register_string_param(symbol(param_name), value, descr, is_mutable); -} - -void ini_params::register_symbol_param(char const * param_name, symbol & value, char const * descr, bool is_mutable) { - m_imp->register_symbol_param(symbol(param_name), value, descr, is_mutable); -} - -void ini_params::register_symbol_list_param(char const * param_name, svector & value, char const * descr, bool is_mutable) { - m_imp->register_symbol_list_param(symbol(param_name), value, descr, is_mutable); -} - -void ini_params::register_symbol_nat_list_param(char const * param_name, svector & value, char const * descr, bool is_mutable) { - m_imp->register_symbol_nat_list_param(symbol(param_name), value, descr, is_mutable); -} - -void ini_params::register_param_vector(param_vector * pv) { - m_imp->register_param_vector(pv); -} - -void ini_params::read_ini_file(std::istream & in) { - ini_parser p(in, m_imp); - p.parse(); -} - -void ini_params::display_params(std::ostream & out) const { - m_imp->display_params(out); -} - -void ini_params::display_parameter_help(char const* param_id, std::ostream & out) const { - m_imp->display_param_help(param_id, out); -} - -void ini_params::display_params_documentation(std::ostream & out) const { - m_imp->display_params_documentation(out); -} - -void ini_params::set_param_value(char const * param_id, char const * param_value) { - m_imp->set_param_value(param_id, param_value); -} -bool ini_params::get_param_value(char const * param_id, std::string& param_value) { - return m_imp->get_param_value(param_id, param_value); -} - -void ini_params::freeze(bool f) { - m_imp->freeze(f); -} - - - diff --git a/src/util/ini_file.h b/src/util/ini_file.h deleted file mode 100644 index cb884b916..000000000 --- a/src/util/ini_file.h +++ /dev/null @@ -1,117 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - ini_file.h - -Abstract: - - Configuration file support. - -Author: - - Leonardo de Moura (leonardo) 2007-05-10. - -Revision History: - ---*/ -#ifndef _INI_FILE_H_ -#define _INI_FILE_H_ - -#include -#include -#include - -#include"symbol.h" -#include"vector.h" -#include"ref.h" - -#ifdef _EXTERNAL_RELEASE -#define PRIVATE_PARAMS(CODE) ((void) 0) -#else -#define PRIVATE_PARAMS(CODE) { CODE } -#endif - -struct param_vector_imp; -struct ini_params_imp; -class ini_parser; - -typedef std::pair symbol_nat_pair; - -inline std::ostream & operator<<(std::ostream & out, symbol_nat_pair const & p) { - out << p.first << ":" << p.second; - return out; -} - -/** - \brief Support for multiple values for a parameter. The values are used to configure - different cores. -*/ -class param_vector { - unsigned m_ref_count; - param_vector_imp * m_imp; - friend struct ini_params_imp; - friend class ini_parser; -public: - // TODO: onwer is a big hack - param_vector(void * owner); - ~param_vector(); - void inc_ref(); - void dec_ref(); - void copy_params(void * curr_owner, unsigned idx); - unsigned size(void) const; -}; - -class set_get_param_exception { - std::string m_id; - std::string m_msg; -public: - set_get_param_exception(char const * id, char const * msg):m_id(id), m_msg(msg) {} - char const * get_param_id() const { return m_id.c_str(); } - char const * get_msg() const { return m_msg.c_str(); } -}; - -class ini_parser_exception { - unsigned m_pos; - std::string m_msg; -public: - ini_parser_exception(unsigned pos, char const * msg):m_pos(pos), m_msg(msg) {} - unsigned get_pos() const { return m_pos; } - char const * get_msg() const { return m_msg.c_str(); } -}; - -class ini_params { - ini_params_imp * m_imp; -public: - ini_params(bool abort_on_error = true); - ~ini_params(); - void freeze(bool f = true); - void register_bool_param(char const * param_name, bool & value, char const * descr = 0, bool is_mutable = false); - void register_unsigned_param(char const * param_name, unsigned min, unsigned max, unsigned & value, char const * descr = 0, bool is_mutable = false); - void register_unsigned_param(char const * param_name, unsigned & value, char const * descr = 0, bool is_mutable = false) { - register_unsigned_param(param_name, 0, INT_MAX, value, descr, is_mutable); - } - void register_int_param(char const * param_name, int min, int max, int & value, char const * descr = 0, bool is_mutable = false); - void register_int_param(char const * param_name, int & value, char const * descr = 0, bool is_mutable = false) { - register_int_param(param_name, INT_MIN, INT_MAX, value, descr, is_mutable); - } - void register_double_param(char const * param_name, double & value, char const * descr = 0,bool is_mutable = false); - void register_percentage_param(char const * param_name, double & value, char const * descr = 0, bool is_mutable = false); - void register_string_param(char const * param_name, std::string & value, char const * descr = 0, bool is_mutable = false); - void register_symbol_param(char const * param_name, symbol & value, char const * descr = 0, bool is_mutable = false); - void register_symbol_list_param(char const * param_name, svector & value, char const * descr = 0, bool is_mutable = false); - void register_symbol_nat_list_param(char const * param_name, svector & value, char const * descr = 0, bool is_mutable = false); - void register_param_vector(param_vector * pv); - - void read_ini_file(std::istream & in); - void display_params(std::ostream & out) const; - void display_parameter_help(char const* param_id, std::ostream & out) const; - void set_param_value(char const * param_id, char const * param_value); - void set_param_mutable(char const * param_id); - bool get_param_value(char const * param_id, std::string& param_value); - void display_params_documentation(std::ostream & out) const; -}; - -#endif /* _INI_FILE_H_ */ - diff --git a/src/util/instruction_count.cpp b/src/util/instruction_count.cpp deleted file mode 100644 index 6dd5bcb85..000000000 --- a/src/util/instruction_count.cpp +++ /dev/null @@ -1,41 +0,0 @@ -#ifdef _WINDOWS -#include -#endif -#include "instruction_count.h" - -#ifdef _WINDOWS -typedef BOOL (WINAPI *QTCP)(HANDLE, PULONG64); -static QTCP QTCP_proc; -BOOL WINAPI dummy_qtcp(HANDLE h, PULONG64 u) -{ - *u = 0; - return 0; -} - -inline void check_handler() -{ - if (!QTCP_proc) { - QTCP_proc = (QTCP) GetProcAddress(GetModuleHandle(TEXT("kernel32.dll")), "QueryThreadCycleTime"); - if (!QTCP_proc) - QTCP_proc = &dummy_qtcp; - } -} -#endif - -void instruction_count::start() { - m_count = 0; -#ifdef _WINDOWS - check_handler(); - QTCP_proc(GetCurrentThread(), &m_count); -#endif -} - -double instruction_count::get_num_instructions() { - unsigned long long current = 0; -#ifdef _WINDOWS - check_handler(); - QTCP_proc(GetCurrentThread(), ¤t); -#endif - return static_cast(current - m_count); -} - diff --git a/src/util/instruction_count.h b/src/util/instruction_count.h deleted file mode 100644 index 29fa0c45b..000000000 --- a/src/util/instruction_count.h +++ /dev/null @@ -1,43 +0,0 @@ -/*++ -Copyright (c) 2009 Microsoft Corporation - -Module Name: - - instruction_count.h - -Abstract: - - - -Author: - - Nikolaj Bjorner (nbjorner) 2009-03-04. - -Revision History: - ---*/ -#ifndef _INSTRUCTION_COUNT_H_ -#define _INSTRUCTION_COUNT_H_ - - -/** - \brief Wrapper for an instruction counter. -*/ -class instruction_count { - unsigned long long m_count; -public: - instruction_count() : m_count(0) {} - - ~instruction_count() {} - - void start(); - - double get_num_instructions(); - - bool is_instruction_maxed(double max_instr) { - return max_instr > 0.0 && get_num_instructions() > max_instr; - } -}; - -#endif /* _INSTRUcTION_COUNT_H_ */ - diff --git a/src/util/util.cpp b/src/util/util.cpp index c2795b637..3e5ced813 100644 --- a/src/util/util.cpp +++ b/src/util/util.cpp @@ -18,7 +18,6 @@ Revision History: --*/ #include"util.h" -#include"ini_file.h" unsigned g_verbosity_level = 0; @@ -30,8 +29,9 @@ unsigned get_verbosity_level() { return g_verbosity_level; } -void register_verbosity_level(ini_params & p) { - p.register_unsigned_param("VERBOSE", g_verbosity_level, "be verbose, where the value is the verbosity level", true); +void register_verbosity_level() { + // PARAM-TODO + // p.register_unsigned_param("VERBOSE", g_verbosity_level, "be verbose, where the value is the verbosity level", true); } static std::ostream* g_verbose_stream = &std::cerr; diff --git a/src/util/warning.cpp b/src/util/warning.cpp index 4ab54f203..19c0dac90 100644 --- a/src/util/warning.cpp +++ b/src/util/warning.cpp @@ -23,7 +23,6 @@ Revision History: #include "util.h" #include "buffer.h" #include "vector.h" -#include "ini_file.h" #ifdef _WINDOWS #define PRF sprintf_s @@ -83,8 +82,9 @@ void set_warning_stream(std::ostream* strm) { g_warning_stream = strm; } -void register_warning(ini_params & p) { - p.register_bool_param("WARNING", g_warning_msgs, "enable/disable warning messages", true); +void register_warning() { + // PARAM-TODO + // p.register_bool_param("WARNING", g_warning_msgs, "enable/disable warning messages", true); } void disable_error_msg_prefix() {