Merge remote-tracking branch 'upstream/parallel' into param-tuning

src/params/smt_parallel.pyg

@@ -0,0 +1,25 @@
+def_module_params('smt_parallel', 
+                  export=True,
+                  description='Experimental parameters for parallel solving',
+                  params=(
+                        ('share_units', BOOL, True, 'share units'),
+                        ('share_conflicts', BOOL, True, 'share conflicts'),
+                        ('never_cube', BOOL, False, 'never cube'),
+                        ('frugal_cube_only', BOOL, False, 'only apply frugal cube strategy'),
+                        ('relevant_units_only', BOOL, True, 'only share relvant units'),
+                        ('max_conflict_mul', DOUBLE, 1.5, 'increment multiplier for max-conflicts'),
+                        ('share_units_initial_only', BOOL, True, 'share only initial Boolean atoms as units'),
+                        ('cube_initial_only', BOOL, False, 'cube only on initial Boolean atoms'),
+                        ('max_cube_depth', UINT, 20, 'maximum depth (size) of a cube to share'),
+                        ('max_greedy_cubes', UINT, 1000, 'maximum number of cube to greedily share before switching to frugal'),
+                        ('num_split_lits', UINT, 2, 'how many literals, k, we split on to create 2^k cubes'),
+                        ('depth_splitting_only', BOOL, False, 'only apply frugal cube strategy, and only on deepest (biggest) cubes from the batch manager'),
+                        ('backbone_detection', BOOL, False, 'apply backbone literal heuristic'),
+                        ('iterative_deepening', BOOL, False, 'deepen cubes based on iterative hardness cutoff heuristic'),
+                        ('beam_search', BOOL, False, 'use beam search with PQ to rank cubes given to threads'),
+                        ('explicit_hardness', BOOL, False, 'use explicit hardness metric for cube'),
+                        ('cubetree', BOOL, False, 'use cube tree data structure for storing cubes'),
+                        ('searchtree', BOOL, False, 'use search tree implementation (parallel2)'),
+                        ('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification'),
+                        ('inprocessing_delay', UINT, 0, 'number of undef before invoking simplification')
+              ))

src/smt/smt_context.cpp

@@ -120,6 +120,10 @@ namespace smt {
         if (!m_setup.already_configured()) {
             m_fparams.updt_params(p);
         }
+        for (auto th : m_theory_set)
+            if (th)
+                th->updt_params();
+
     }
 
     unsigned context::relevancy_lvl() const {

src/smt/smt_parallel.cpp

@@ -25,6 +25,7 @@ Author:
 #include "smt/smt_parallel.h"
 #include "smt/smt_lookahead.h"
 #include "solver/solver_preprocess.h"
+// #include "params/smt_parallel_params.hpp"
 
 #include <cmath>
 #include <mutex>

src/smt/smt_parallel.h

@@ -100,6 +100,20 @@ namespace smt {
             lbool get_result() const;
         };
 
+        // life cycle of 
+        // 1. proof prefix with cubes
+        // 2. restart N separate contexts to check N new permutations of parameters.
+        //    - one of the contexts uses the current configuration.
+        // 3. pick winner configuration if any are better than current.
+        // 4. update current configuration with the winner
+
+        class parameter_generator_thread {
+            unsigned N; // number of prefix permutation testers
+            scoped_ptr<context> prefix_solver;
+            scoped_ptr_vector<context> testers; // N testers
+
+        };
+
         class worker {
             struct config {
                 unsigned m_threads_max_conflicts = 1000;

src/smt/smt_theory.h

@@ -417,6 +417,8 @@ namespace smt {
 
         smt_params const& get_fparams() const;
 
+        virtual void updt_params() {}
+
         enode * get_enode(theory_var v) const {
             SASSERT(v < static_cast<int>(m_var2enode.size()));
             return m_var2enode[v];

src/smt/theory_lra.cpp

@@ -870,16 +870,12 @@ public:
         get_zero(true);
         get_zero(false);
 
+
         lp().updt_params(ctx().get_params());
         lp().settings().set_resource_limit(m_resource_limit);
-        lp().settings().bound_propagation() = bound_prop_mode::BP_NONE != propagation_mode();
-
-        // todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts
-        unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio;
-        lp().set_cut_strategy(branch_cut_ratio);
-        
-        lp().settings().set_run_gcd_test(ctx().get_fparams().m_arith_gcd_test);
-        lp().settings().set_random_seed(ctx().get_fparams().m_random_seed);
+        lp().settings().bound_propagation() = bound_prop_mode::BP_NONE != propagation_mode(); // propagation_mode() is state dependent.
+        lp().settings().set_random_seed(ctx().get_fparams().m_random_seed);      // suffice to set once
+        lp().settings().set_run_gcd_test(ctx().get_fparams().m_arith_gcd_test);  // this is not exposed to the user yet.
         m_lia = alloc(lp::int_solver, *m_solver.get());
     }
         
@@ -4199,6 +4195,13 @@ public:
         m_bound_predicate = nullptr;
     }
 
+    void updt_params() {
+        if (m_solver)
+            m_solver->updt_params(ctx().get_params());
+        if (m_nla)
+            m_nla->updt_params(ctx().get_params());
+    }
+
 
     void validate_model(proto_model& mdl) {
 
@@ -4359,6 +4362,10 @@ void theory_lra::setup() {
     m_imp->setup();
 }
 
+void theory_lra::updt_params() {
+    m_imp->updt_params();
+}
+
 void theory_lra::validate_model(proto_model& mdl) {
     m_imp->validate_model(mdl);
 }

src/smt/theory_lra.h

@@ -94,6 +94,8 @@ namespace smt {
         bool get_lower(enode* n, rational& r, bool& is_strict);
         bool get_upper(enode* n, rational& r, bool& is_strict);
         void solve_for(vector<solution>& s) override;
+
+        void updt_params() override;
                 
         void display(std::ostream & out) const override;