move to generic state

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

Author: NikolajBjorner

src/smt/smt_parallel.cpp

@@ -70,11 +70,14 @@ namespace smt {
         lbool r = l_undef;
         try {
             r = ctx->check();
-        } catch (z3_error &err) {
+        } 
+        catch (z3_error &err) {
             b.set_exception(err.error_code());
-        } catch (z3_exception &ex) {
+        } 
+        catch (z3_exception &ex) {
             b.set_exception(ex.what());
-        } catch (...) {
+        } 
+        catch (...) {
             b.set_exception("unknown exception");
         }
         return r;
@@ -130,6 +133,52 @@ namespace smt {
         return best_param_state_idx;
     }
 
+    void parallel::param_generator::init_param_state() {
+        // param_descrs smt_desc;
+        // smt_params_helper::collect_param_descrs(smt_desc);
+        smt_params_helper smtp(m_p);
+        m_my_param_state.insert(symbol("smt.arith.nl.branching"), smtp.arith_nl_branching());
+        m_my_param_state.insert(symbol("smt.arith.nl.cross_nested"), smtp.arith_nl_cross_nested());
+        m_my_param_state.insert(symbol("smt.arith.nl.delay"), smtp.arith_nl_delay());
+        m_my_param_state.insert(symbol("smt.arith.nl.expensive_patching"), smtp.arith_nl_expensive_patching());
+        m_my_param_state.insert(symbol("smt.arith.nl.gb"), smtp.arith_nl_gb());
+        m_my_param_state.insert(symbol("smt.arith.nl.horner"), smtp.arith_nl_horner());
+        m_my_param_state.insert(symbol("smt.arith.nl.horner_frequency"), smtp.arith_nl_horner_frequency());
+        m_my_param_state.insert(symbol("smt.arith.nl.optimize_bounds"), smtp.arith_nl_optimize_bounds());
+        m_my_param_state.insert(symbol("smt.arith.nl.propagate_linear_monomials"), smtp.arith_nl_propagate_linear_monomials());
+        m_my_param_state.insert(symbol("smt.arith.nl.tangents"), smtp.arith_nl_tangents());
+    };
+
+    // TODO: this should mutate only one field at a time an mutate it based on m_my_param_state to keep it generic.
+
+    smt_params parallel::param_generator::mutate_param_state() {
+        smt_params p = m_param_state;
+        random_gen m_rand;
+
+        auto flip_bool = [&](bool &x) {
+            if (m_rand(2) == 0)
+                x = !x;
+        };
+
+        auto mutate_uint = [&](unsigned &x, unsigned lo, unsigned hi) {
+            if ((m_rand() % 2) == 0)
+                x = lo + (m_rand((hi - lo + 1)));
+        };
+
+        flip_bool(p.m_nl_arith_branching);
+        flip_bool(p.m_nl_arith_cross_nested);
+        mutate_uint(p.m_nl_arith_delay, 5, 20);
+        flip_bool(p.m_nl_arith_expensive_patching);
+        flip_bool(p.m_nl_arith_gb);
+        flip_bool(p.m_nl_arith_horner);
+        mutate_uint(p.m_nl_arith_horner_frequency, 2, 6);
+        flip_bool(p.m_nl_arith_optimize_bounds);
+        flip_bool(p.m_nl_arith_propagate_linear_monomials);
+        flip_bool(p.m_nl_arith_tangents);
+
+        return p;
+    }
+
     void parallel::param_generator::protocol_iteration() {
         IF_VERBOSE(1, verbose_stream() << " PARAM TUNER running protocol iteration\n");
         ctx->get_fparams().m_max_conflicts = m_max_prefix_conflicts;
@@ -144,6 +193,8 @@ namespace smt {
 
         switch (r) {
             case l_undef: {
+            // TODO, change from smt_params to a generic param state representation based on params_ref
+                // only params_ref have effect on updates.
                 smt_params best_param_state = m_param_state;
                 vector<smt_params> candidate_param_states;
 

src/smt/smt_parallel.h

@@ -20,6 +20,7 @@ Revision History:
 
 #include "smt/smt_context.h"
 #include "util/search_tree.h"
+#include <variant>
 // #include "util/util.h"
 #include <thread>
 #include <mutex>
@@ -127,74 +128,37 @@ namespace smt {
         // 4. update current configuration with the winner
 
         class param_generator {
-            parallel& p;
-            batch_manager& b;
+            parallel &p;
+            batch_manager &b;
             ast_manager m;
             scoped_ptr<context> ctx;
             ast_translation m_l2g;
-            
-            unsigned N = 4; // number of prefix permutations to test (including current)
+
+            unsigned N = 4;  // number of prefix permutations to test (including current)
             unsigned m_max_prefix_conflicts = 1000;
-            
+
             scoped_ptr<context> m_prefix_solver;
             scoped_ptr_vector<context> m_param_probe_contexts;
             smt_params m_param_state;
             params_ref m_p;
-            
-            private:
-                void init_param_state() {
-                    m_param_state.m_nl_arith_branching = true;
-                    m_param_state.m_nl_arith_cross_nested = true;
-                    m_param_state.m_nl_arith_delay = 10;
-                    m_param_state.m_nl_arith_expensive_patching = false;
-                    m_param_state.m_nl_arith_gb = true;
-                    m_param_state.m_nl_arith_horner = true;
-                    m_param_state.m_nl_arith_horner_frequency = 4;
-                    m_param_state.m_nl_arith_optimize_bounds = true;
-                    m_param_state.m_nl_arith_propagate_linear_monomials = true;
-                    m_param_state.m_nl_arith_tangents = true;
-
-                    m_param_state.updt_params(m_p);
-                    ctx->updt_params(m_p);
-                };
-
-                smt_params mutate_param_state() {
-                    smt_params p = m_param_state;
-                    random_gen m_rand;
-
-                    auto flip_bool = [&](bool &x) {
-                        if ((m_rand() % 2) == 0)
-                            x = !x;
-                    };
-
-                    auto mutate_uint = [&](unsigned &x, unsigned lo, unsigned hi) {
-                        if ((m_rand() % 2) == 0)
-                            x = lo + (m_rand() % (hi - lo + 1));
-                    };
-
-                    flip_bool(p.m_nl_arith_branching);
-                    flip_bool(p.m_nl_arith_cross_nested);
-                    mutate_uint(p.m_nl_arith_delay, 5, 20);
-                    flip_bool(p.m_nl_arith_expensive_patching);
-                    flip_bool(p.m_nl_arith_gb);
-                    flip_bool(p.m_nl_arith_horner);
-                    mutate_uint(p.m_nl_arith_horner_frequency, 2, 6);
-                    flip_bool(p.m_nl_arith_optimize_bounds);
-                    flip_bool(p.m_nl_arith_propagate_linear_monomials);
-                    flip_bool(p.m_nl_arith_tangents);
-
-                    return p;
-                }
-
-            public:
-                param_generator(parallel& p);
-                lbool run_prefix_step();
-                void protocol_iteration();
-                unsigned replay_proof_prefixes(vector<smt_params> candidate_param_states, unsigned max_conflicts_epsilon);
-
-                reslimit& limit() {
-                    return m.limit();
-                }
+
+            using param_value = std::variant<unsigned, bool, double>;
+            symbol_table<param_value> m_my_param_state;
+
+        private:
+            void init_param_state();
+
+            smt_params mutate_param_state();
+
+        public:
+            param_generator(parallel &p);
+            lbool run_prefix_step();
+            void protocol_iteration();
+            unsigned replay_proof_prefixes(vector<smt_params> candidate_param_states, unsigned max_conflicts_epsilon);
+
+            reslimit &limit() {
+                return m.limit();
+            }
         };
 
         class worker {