update dependencies

scripts/mk_project.py

@@ -21,10 +21,10 @@ def init_project_def():
     add_lib('hilbert', ['util'], 'math/hilbert')
     add_lib('automata', ['util'], 'math/automata')
     add_lib('params', ['util'])
-    add_lib('smt_params', ['params'], 'smt/params')
     add_lib('realclosure', ['interval'], 'math/realclosure')
     add_lib('subpaving', ['interval'], 'math/subpaving')
     add_lib('ast', ['util', 'polynomial'])
+    add_lib('smt_params', ['ast', 'params'], 'smt/params')
     add_lib('parser_util', ['ast'], 'parsers/util')
     add_lib('euf', ['ast'], 'ast/euf')
     add_lib('grobner', ['ast', 'dd', 'simplex'], 'math/grobner')    

src/smt/params/CMakeLists.txt

@@ -12,6 +12,7 @@ z3_add_component(smt_params
     theory_str_params.cpp
   COMPONENT_DEPENDENCIES
     params
+    ast
   PYG_FILES
     smt_params_helper.pyg
 )

src/smt/params/smt_params.cpp

@@ -292,6 +292,18 @@ void smt_params::setup_QF_LIA(static_features const& st) {
     }
 }
 
+void smt_params::setup_QF_UFIDL() {
+    m_relevancy_lvl = 0;
+    m_arith_reflect = false;
+    m_nnf_cnf = false;
+    m_arith_eq_bounds = true;
+    m_arith_eq2ineq = true;
+    // m_params.m_phase_selection  = PS_THEORY;
+    m_restart_strategy = RS_GEOMETRIC;
+    m_restart_factor = 1.5;
+    m_restart_adaptive = false;
+}
+
 void smt_params::setup_QF_UFLIA() {
     m_relevancy_lvl       = 0;
     m_arith_reflect       = false; 

src/smt/params/smt_params.h

@@ -274,6 +274,8 @@ struct smt_params : public preprocessor_params,
 
     void setup_QF_LIA(static_features const& st);
 
+    void setup_QF_UFIDL();
+
     void setup_QF_UFLIA();
 
     void setup_QF_UFLRA();

src/smt/smt_setup.cpp

@@ -377,15 +377,7 @@ namespace smt {
 
     void setup::setup_QF_UFIDL() {
         TRACE("setup", tout << "setup_QF_UFIDL()\n";);
-        m_params.m_relevancy_lvl    = 0;
-        m_params.m_arith_reflect    = false;
-        m_params.m_nnf_cnf          = false;
-        m_params.m_arith_eq_bounds  = true;
-        m_params.m_arith_eq2ineq    = true;
-        // m_params.m_phase_selection  = PS_THEORY;
-        m_params.m_restart_strategy = RS_GEOMETRIC;
-        m_params.m_restart_factor   = 1.5;
-        m_params.m_restart_adaptive = false;
+        m_params.setup_QF_UFIDL();
         setup_lra_arith();
     }
 
@@ -624,8 +616,6 @@ namespace smt {
         }
     }
 
-
-
     void setup::setup_arith() {
         static_features    st(m_manager);
         IF_VERBOSE(100, verbose_stream() << "(smt.collecting-features)\n";);