From e0a44894cf480908ddc8110b1761e682af4e4644 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Jun 2019 16:56:24 +0200 Subject: [PATCH] purge smt.timeout, use timeout instead to control solver timing #2354 Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_context.cpp | 2 +- src/muz/base/fp_params.pyg | 1 + src/muz/clp/clp_context.cpp | 1 - src/muz/tab/tab_context.cpp | 1 - src/smt/params/smt_params.cpp | 4 ---- src/smt/params/smt_params.h | 4 ---- src/smt/params/smt_params_helper.pyg | 2 -- 7 files changed, 2 insertions(+), 13 deletions(-) diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index f5c8f649c..ccbed6b70 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -288,9 +288,9 @@ namespace datalog { bool context::compile_with_widening() const { return m_params->datalog_compile_with_widening(); } bool context::unbound_compressor() const { return m_unbound_compressor; } void context::set_unbound_compressor(bool f) { m_unbound_compressor = f; } + unsigned context::soft_timeout() const { return m_params->datalog_timeout(); } bool context::similarity_compressor() const { return m_params->datalog_similarity_compressor(); } unsigned context::similarity_compressor_threshold() const { return m_params->datalog_similarity_compressor_threshold(); } - unsigned context::soft_timeout() const { return m_fparams.m_timeout; } unsigned context::initial_restart_timeout() const { return m_params->datalog_initial_restart_timeout(); } bool context::generate_explanations() const { return m_params->datalog_generate_explanations(); } bool context::explanations_on_relation_level() const { return m_params->datalog_explanations_on_relation_level(); } diff --git a/src/muz/base/fp_params.pyg b/src/muz/base/fp_params.pyg index 325ecaaa6..71aaf1881 100644 --- a/src/muz/base/fp_params.pyg +++ b/src/muz/base/fp_params.pyg @@ -41,6 +41,7 @@ def_module_params('fp', ('datalog.initial_restart_timeout', UINT, 0, "length of saturation run before the first restart (in ms), " + "zero means no restarts"), + ('datalog.timeout', UINT, 0, "Time limit used for saturation"), ('datalog.output_profile', BOOL, False, "determines whether profile information should be " + "output when outputting Datalog rules or instructions"), diff --git a/src/muz/clp/clp_context.cpp b/src/muz/clp/clp_context.cpp index f6ebfbfb4..61d1fd418 100644 --- a/src/muz/clp/clp_context.cpp +++ b/src/muz/clp/clp_context.cpp @@ -57,7 +57,6 @@ namespace datalog { { // m_fparams.m_relevancy_lvl = 0; m_fparams.m_mbqi = false; - m_fparams.m_timeout = 1000; } ~imp() {} diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp index 3b8fd2ee0..e580f84e1 100644 --- a/src/muz/tab/tab_context.cpp +++ b/src/muz/tab/tab_context.cpp @@ -1354,7 +1354,6 @@ namespace datalog { { // m_fparams.m_relevancy_lvl = 0; m_fparams.m_mbqi = false; - m_fparams.m_timeout = 1000; } ~imp() {} diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 4b42e0339..c38b9fbb2 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -37,8 +37,6 @@ void smt_params::updt_local_params(params_ref const & _p) { m_delay_units = p.delay_units(); m_delay_units_threshold = p.delay_units_threshold(); m_preprocess = _p.get_bool("preprocess", true); // hidden parameter - m_timeout = p.timeout(); - m_rlimit = p.rlimit(); m_max_conflicts = p.max_conflicts(); m_restart_max = p.restart_max(); m_core_validate = p.core_validate(); @@ -159,8 +157,6 @@ void smt_params::display(std::ostream & out) const { DISPLAY_PARAM(m_preprocess); DISPLAY_PARAM(m_user_theory_preprocess_axioms); DISPLAY_PARAM(m_user_theory_persist_axioms); - DISPLAY_PARAM(m_timeout); - DISPLAY_PARAM(m_rlimit); DISPLAY_PARAM(m_at_labels_cex); DISPLAY_PARAM(m_check_at_labels); DISPLAY_PARAM(m_dump_goal_as_smt); diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index b4423f933..9c2cb26e3 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -215,8 +215,6 @@ struct smt_params : public preprocessor_params, bool m_preprocess; // temporary hack for disabling all preprocessing.. bool m_user_theory_preprocess_axioms; bool m_user_theory_persist_axioms; - unsigned m_timeout; - unsigned m_rlimit; 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; @@ -304,8 +302,6 @@ struct smt_params : public preprocessor_params, m_preprocess(true), // temporary hack for disabling all preprocessing.. m_user_theory_preprocess_axioms(false), m_user_theory_persist_axioms(false), - m_timeout(0), - m_rlimit(0), m_at_labels_cex(false), m_check_at_labels(false), m_dump_goal_as_smt(false), diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 41adc907e..f81cbfa44 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -18,8 +18,6 @@ def_module_params(module_name='smt', ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ignored if delay_units is false'), ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'), ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'), - ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'), - ('rlimit', UINT, 0, 'resource limit (0 means no limit)'), ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'), ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'), ('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),