From b76d588c281c4ca1d08bec4477f903490cd7d412 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 21 Mar 2015 16:10:30 +0000 Subject: [PATCH] Renamed the soft_timeout option to just timeout. Signed-off-by: Christoph M. Wintersteiger --- src/muz/base/dl_context.cpp | 2 +- src/muz/base/dl_context.h | 2 +- src/muz/clp/clp_context.cpp | 2 +- src/muz/rel/rel_context.cpp | 4 ++-- src/muz/tab/tab_context.cpp | 2 +- src/smt/params/smt_params.cpp | 2 +- src/smt/params/smt_params.h | 4 ++-- src/smt/params/smt_params_helper.pyg | 2 +- src/smt/smt_context.cpp | 2 +- 9 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 7c9c5813b..30dd08ff4 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -288,7 +288,7 @@ namespace datalog { bool context::unbound_compressor() const { return m_params->unbound_compressor(); } bool context::similarity_compressor() const { return m_params->similarity_compressor(); } unsigned context::similarity_compressor_threshold() const { return m_params->similarity_compressor_threshold(); } - unsigned context::soft_timeout() const { return m_fparams.m_soft_timeout; } + unsigned context::timeout() const { return m_fparams.m_timeout; } unsigned context::initial_restart_timeout() const { return m_params->initial_restart_timeout(); } bool context::generate_explanations() const { return m_params->generate_explanations(); } bool context::explanations_on_relation_level() const { return m_params->explanations_on_relation_level(); } diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index cf2c53913..8a881d71b 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -258,7 +258,7 @@ namespace datalog { bool unbound_compressor() const; bool similarity_compressor() const; unsigned similarity_compressor_threshold() const; - unsigned soft_timeout() const; + unsigned timeout() const; unsigned initial_restart_timeout() const; bool generate_explanations() const; bool explanations_on_relation_level() const; diff --git a/src/muz/clp/clp_context.cpp b/src/muz/clp/clp_context.cpp index 0cd08e5b3..11f6ae1db 100644 --- a/src/muz/clp/clp_context.cpp +++ b/src/muz/clp/clp_context.cpp @@ -59,7 +59,7 @@ namespace datalog { { // m_fparams.m_relevancy_lvl = 0; m_fparams.m_mbqi = false; - m_fparams.m_soft_timeout = 1000; + m_fparams.m_timeout = 1000; } ~imp() {} diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index 02b00be39..4e219b2f7 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -128,8 +128,8 @@ namespace datalog { lbool rel_context::saturate(scoped_query& sq) { m_context.ensure_closed(); - bool time_limit = m_context.soft_timeout()!=0; - unsigned remaining_time_limit = m_context.soft_timeout(); + bool time_limit = m_context.timeout()!=0; + unsigned remaining_time_limit = m_context.timeout(); unsigned restart_time = m_context.initial_restart_timeout(); instruction_block termination_code; diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp index 83842a68b..f13590e35 100644 --- a/src/muz/tab/tab_context.cpp +++ b/src/muz/tab/tab_context.cpp @@ -1367,7 +1367,7 @@ namespace datalog { { // m_fparams.m_relevancy_lvl = 0; m_fparams.m_mbqi = false; - m_fparams.m_soft_timeout = 1000; + m_fparams.m_timeout = 1000; } ~imp() {} diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 2f8d9c1ee..a0f56663c 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -34,7 +34,7 @@ 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_soft_timeout = p.soft_timeout(); + m_timeout = p.timeout(); model_params mp(_p); m_model_compact = mp.compact(); if (_p.get_bool("arith.greatest_error_pivot", false)) diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 256c5a646..2fbc9b6d4 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -202,7 +202,7 @@ 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_soft_timeout; + unsigned m_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; @@ -270,7 +270,7 @@ 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_soft_timeout(0), + m_timeout(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 39818e621..97a326e4d 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -15,7 +15,7 @@ def_module_params(module_name='smt', ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ingored if delay_units is false'), ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'), ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'), - ('soft_timeout', UINT, 0, 'soft timeout (0 means no timeout)'), + ('timeout', UINT, 0, 'timeout (0 means no timeout)'), ('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'), ('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'), ('mbqi.max_cexs_incr', UINT, 0, 'increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI'), diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 957d5ebe7..d7e18461b 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3355,7 +3355,7 @@ namespace smt { if (m_last_search_failure != OK) return true; - if (m_timer.ms_timeout(m_fparams.m_soft_timeout)) { + if (m_timer.ms_timeout(m_fparams.m_timeout)) { m_last_search_failure = TIMEOUT; return true; }