diff --git a/src/params/smt_parallel.pyg b/src/params/smt_parallel.pyg new file mode 100644 index 000000000..9a81f6c25 --- /dev/null +++ b/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') + )) \ No newline at end of file diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 4f73671ea..c0a2f3a4d 100644 --- a/src/smt/smt_context.cpp +++ b/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 { diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index aa33e73e4..b711394d9 100644 --- a/src/smt/smt_parallel.cpp +++ b/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 #include diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index 3c47d818d..f3fa7371b 100644 --- a/src/smt/smt_parallel.h +++ b/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 prefix_solver; + scoped_ptr_vector testers; // N testers + + }; + class worker { struct config { unsigned m_threads_max_conflicts = 1000; diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index 20c7380eb..8e23a6644 100644 --- a/src/smt/smt_theory.h +++ b/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(m_var2enode.size())); return m_var2enode[v]; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 2c58400ba..59c750306 100644 --- a/src/smt/theory_lra.cpp +++ b/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); } diff --git a/src/smt/theory_lra.h b/src/smt/theory_lra.h index 1624bab0a..64d200506 100644 --- a/src/smt/theory_lra.h +++ b/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& s) override; + + void updt_params() override; void display(std::ostream & out) const override;