mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

removed ini_file

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-01 16:30:39 -08:00
parent 823dd6ca47
commit 9374a4e20a
38 changed files with 82 additions and 1971 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/cmd_context/cmd_context.cpp
View file

@ -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) {

3
src/front_end_params/arith_simplifier_params.cpp
View file

@ -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

4
src/front_end_params/arith_simplifier_params.h
View file

@ -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_ */

4
src/front_end_params/bit_blaster_params.h
View file

@ -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_ */

4
src/front_end_params/bv_simplifier_params.h
View file

@ -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_ */

3
src/front_end_params/dyn_ack_params.cpp
View file

@ -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<int&>(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

3
src/front_end_params/dyn_ack_params.h
View file

@ -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);
};

10
src/front_end_params/front_end_params.cpp
View file

@ -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);

25
src/front_end_params/front_end_params.h
View file

@ -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<param_vector> 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:

3
src/front_end_params/pattern_inference_params.cpp
View file

@ -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

4
src/front_end_params/pattern_inference_params.h
View file

@ -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_ */

3
src/front_end_params/preprocessor_params.h
View file

@ -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_ */

7
src/front_end_params/qi_params.h
View file

@ -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_ */

2
src/front_end_params/smt_params.cpp
View file

@ -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

7
src/front_end_params/smt_params.h
View file

@ -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_ */

2
src/front_end_params/theory_arith_params.cpp
View file

@ -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<int&>(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

4
src/front_end_params/theory_arith_params.h
View file

@ -19,7 +19,7 @@ Revision History:
#ifndef _THEORY_ARITH_PARAMS_H_
#define _THEORY_ARITH_PARAMS_H_
#include"ini_file.h"
#include<limits.h>
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_ */

5
src/front_end_params/theory_array_params.h
View file

@ -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<int&>(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
};

4
src/front_end_params/theory_bv_params.h
View file

@ -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<int&>(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_ */

4
src/front_end_params/theory_datatype_params.h
View file

@ -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
};

6
src/muz_qe/dl_cmds.cpp
View file

@ -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) {

16
src/muz_qe/dl_context.cpp
View file

@ -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);

22
src/muz_qe/pdr_dl_interface.cpp
View file

@ -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");

8
src/shell/datalog_frontend.cpp
View file

@ -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,

2
src/shell/datalog_frontend.h
View file

@ -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);

55
src/shell/main.cpp
View file

@ -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<size_t>(g_front_end_params->m_memory_high_watermark) * 1024 * 1024);
memory::set_max_size(static_cast<size_t>(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.");
}

1
src/shell/smtlib_frontend.cpp
View file

@ -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();

6
src/smt/smt_context.cpp
View file

@ -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)) {

2
src/smt/smt_context.h
View file

@ -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<quantifier_manager> m_qmanager;
scoped_ptr<model_generator> m_model_generator;

1
src/smt/smt_setup.cpp
View file

@ -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() {

50
src/test/ini_file.cpp
View file

@ -1,50 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
ini_file.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2007-05-10.
Revision History:
--*/
#include<sstream>
#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();
}

1
src/test/main.cpp
View file

@ -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);

1564
src/util/ini_file.cpp
View file

File diff suppressed because it is too large Load diff

117
src/util/ini_file.h
View file

@ -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<iostream>
#include<limits.h>
#include<string>
#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, unsigned> 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<symbol> & value, char const * descr = 0, bool is_mutable = false);
void register_symbol_nat_list_param(char const * param_name, svector<symbol_nat_pair> & 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_ */

41
src/util/instruction_count.cpp
View file

@ -1,41 +0,0 @@
#ifdef _WINDOWS
#include <windows.h>
#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(), &current);
#endif
return static_cast<double>(current - m_count);
}

43
src/util/instruction_count.h
View file

@ -1,43 +0,0 @@
/*++
Copyright (c) 2009 Microsoft Corporation
Module Name:
instruction_count.h
Abstract:
<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_ */

6
src/util/util.cpp
View file

@ -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;

6
src/util/warning.cpp
View file

@ -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() {