purge smt.timeout, use timeout instead to control solver timing #2354

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

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

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"),

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

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

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

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

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)'),