From 9bd4fd969ac859c4bcfb48727d96a37359950596 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 1 Dec 2012 18:50:26 -0800 Subject: [PATCH] cleanning Signed-off-by: Leonardo de Moura --- src/front_end_params/front_end_params.cpp | 1 - src/front_end_params/front_end_params.h | 6 +----- src/front_end_params/smt_params.h | 6 +++--- src/shell/dimacs_frontend.cpp | 8 +++----- src/shell/dimacs_frontend.h | 2 +- src/shell/main.cpp | 20 ++------------------ 6 files changed, 10 insertions(+), 33 deletions(-) diff --git a/src/front_end_params/front_end_params.cpp b/src/front_end_params/front_end_params.cpp index 0d51d94fb..32692180f 100644 --- a/src/front_end_params/front_end_params.cpp +++ b/src/front_end_params/front_end_params.cpp @@ -36,7 +36,6 @@ void front_end_params::register_params(ini_params & p) { p.register_int_param("proof_mode", 0, 2, reinterpret_cast(m_proof_mode), "select proof generation mode: 0 - disabled, 1 - coarse grain, 2 - fine grain"); p.register_bool_param("trace", m_trace, "enable tracing for the Axiom Profiler tool"); p.register_string_param("trace_file_name", m_trace_file_name, "tracing file name"); - p.register_bool_param("display_config", m_display_config, "display configuration used by Z3"); #ifdef _WINDOWS // The non-windows memory manager does not have access to memory sizes. diff --git a/src/front_end_params/front_end_params.h b/src/front_end_params/front_end_params.h index c3fa9fa95..2c7dbfa2e 100644 --- a/src/front_end_params/front_end_params.h +++ b/src/front_end_params/front_end_params.h @@ -33,8 +33,6 @@ struct front_end_params : public smt_params { bool m_trace; std::string m_trace_file_name; std::fstream* m_trace_stream; - bool m_display_config; - bool m_dump_goal_as_smt; front_end_params(): m_well_sorted_check(true), @@ -45,9 +43,7 @@ struct front_end_params : public smt_params { m_debug_ref_count(false), m_trace(false), m_trace_file_name("z3.log"), - m_trace_stream(NULL), - m_display_config(false), - m_dump_goal_as_smt(false) { + m_trace_stream(NULL) { } void open_trace_file(); diff --git a/src/front_end_params/smt_params.h b/src/front_end_params/smt_params.h index 6e7755458..24479de16 100644 --- a/src/front_end_params/smt_params.h +++ b/src/front_end_params/smt_params.h @@ -204,6 +204,7 @@ struct smt_params : public preprocessor_params, unsigned m_soft_timeout; 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_dump_goal_as_smt; smt_params(): m_display_proof(false), @@ -270,9 +271,8 @@ struct smt_params : public preprocessor_params, m_user_theory_persist_axioms(false), m_soft_timeout(0), m_at_labels_cex(false), - m_check_at_labels(false) - { - + m_check_at_labels(false), + m_dump_goal_as_smt(false) { } }; diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp index 2dbb0adf8..0acd222dd 100644 --- a/src/shell/dimacs_frontend.cpp +++ b/src/shell/dimacs_frontend.cpp @@ -22,7 +22,6 @@ Revision History: #include"timeout.h" #include"dimacs.h" #include"sat_solver.h" -#include"front_end_params.h" extern bool g_display_statistics; static sat::solver * g_solver = 0; @@ -64,12 +63,12 @@ static void display_model(sat::solver const & s) { std::cout << "\n"; } -unsigned read_dimacs(char const * file_name, front_end_params & front_end_params) { +unsigned read_dimacs(char const * file_name) { g_start_time = clock(); register_on_timeout_proc(on_timeout); signal(SIGINT, on_ctrl_c); params_ref p; - p.set_bool("produce_models", front_end_params.m_model); + p.set_bool("produce_models", true); sat::solver solver(p, 0); g_solver = &solver; @@ -90,8 +89,7 @@ unsigned read_dimacs(char const * file_name, front_end_params & front_end_params switch (r) { case l_true: std::cout << "sat\n"; - if (front_end_params.m_model) - display_model(solver); + display_model(solver); break; case l_undef: std::cout << "unknown\n"; diff --git a/src/shell/dimacs_frontend.h b/src/shell/dimacs_frontend.h index 22ab63529..9521c8256 100644 --- a/src/shell/dimacs_frontend.h +++ b/src/shell/dimacs_frontend.h @@ -19,7 +19,7 @@ Revision History: #ifndef _DIMACS_FRONTEND_H_ #define _DIMACS_FRONTEND_H_ -unsigned read_dimacs(char const * benchmark_file, front_end_params & front_end_params); +unsigned read_dimacs(char const * benchmark_file); #endif /* _DATALOG_FRONTEND_H_ */ diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 5434206cc..b08d02812 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -77,7 +77,7 @@ void display_usage() { std::cout << " " << OPT << "version prints version number of Z3.\n"; std::cout << " " << OPT << "v:level be verbose, where is the verbosity level.\n"; std::cout << " " << OPT << "nw disable warning messages.\n"; - std::cout << " " << OPT << "ps display all available parameters.\n"; + std::cout << " " << OPT << "ps display Z3 global (and module) parameters.\n"; std::cout << " --" << " all remaining arguments are assumed to be part of the input file name. This option allows Z3 to read files with strange names such as: -foo.smt2.\n"; std::cout << "\nResources:\n"; // timeout and memout are now available on Linux and OSX too. @@ -87,8 +87,6 @@ void display_usage() { // std::cout << "\nOutput:\n"; std::cout << " " << OPT << "st display statistics.\n"; - std::cout << "\nSearch heuristics:\n"; - std::cout << " " << OPT << "rs:num random seed.\n"; #if defined(Z3DEBUG) || defined(_TRACE) std::cout << "\nDebugging support:\n"; #endif @@ -226,20 +224,6 @@ void parse_cmd_line_args(int argc, char ** argv) { } g_front_end_params->m_relevancy_lvl = strtol(opt_arg, 0, 10); } - else if (strcmp(opt_name, "rd") == 0) { - if (!opt_arg) { - error("optional argument (/rd:num) is missing."); - } - g_front_end_params->m_random_var_freq = static_cast(strtol(opt_arg, 0, 10)) / 100.0; - } - else if (strcmp(opt_name, "rs") == 0) { - if (!opt_arg) { - error("optional argument (/rs:num) is missing."); - } - long seed = strtol(opt_arg, 0, 10); - g_front_end_params->m_random_seed = seed; - g_front_end_params->m_arith_random_seed = seed; - } else if (strcmp(opt_name, "T") == 0) { if (!opt_arg) error("option argument (/T:timeout) is missing."); @@ -382,7 +366,7 @@ int main(int argc, char ** argv) { return_value = read_smtlib2_commands(g_input_file, *g_front_end_params); break; case IN_DIMACS: - return_value = read_dimacs(g_input_file, *g_front_end_params); + return_value = read_dimacs(g_input_file); break; case IN_DATALOG: read_datalog(g_input_file, *g_extra_params, *g_front_end_params);