Renamed the soft_timeout option to just timeout.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

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

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;

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

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;
+        bool time_limit = m_context.timeout()!=0;
-        unsigned remaining_time_limit = m_context.soft_timeout();
+        unsigned remaining_time_limit = m_context.timeout();
         unsigned restart_time = m_context.initial_restart_timeout();
                         
         instruction_block termination_code;

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

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

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

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

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