diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 32d764658..73fdea20f 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -259,8 +259,12 @@ namespace sat { throw sat_param_exception("invalid PB lemma format: 'cardinality' or 'pb' expected"); m_card_solver = p.cardinality_solver(); - m_xor_solver = false; // prevent users from playing with this option - + m_xor_enable = p.xor_enable(); + m_xor_gauss_max_matrix_rows = p.xor_gauss_max_matrix_rows(); + m_xor_gauss_min_matrix_rows = p.xor_gauss_min_matrix_rows(); + m_xor_gauss_max_matrix_columns = p.xor_gauss_max_matrix_columns(); + m_xor_gauss_max_num_matrices = p.xor_gauss_max_num_matrices(); + sat_simplifier_params ssp(_p); m_elim_vars = ssp.elim_vars(); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index ae19c63ea..fca046d73 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -186,7 +186,6 @@ namespace sat { bool m_drat_activity; bool m_card_solver; - bool m_xor_solver; pb_resolve m_pb_resolve; pb_lemma_format m_pb_lemma_format; @@ -202,6 +201,14 @@ namespace sat { // simplifier configurations used outside of sat_simplifier bool m_elim_vars; + // xor + bool m_xor_enable; + unsigned m_xor_gauss_max_matrix_rows; + unsigned m_xor_gauss_min_matrix_rows; + unsigned m_xor_gauss_max_matrix_columns; + unsigned m_xor_gauss_max_num_matrices; + + config(params_ref const & p); void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index a5edca25a..26a18f273 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -126,7 +126,7 @@ def_module_params('sat', # Each reward function also comes with its own variant of "mix_diff", which # is the function for combining reward metrics for the positive and negative variant of a literal. # Xor parameters - ('xor.enable', BOOL, False, 'enable xor solver plugin in combination with pure SAT solving')) + ('xor.enable', BOOL, False, 'enable xor solver plugin in combination with pure SAT solving'), # Pull in other xor parameters as they are determined to be relevant # ('xor.max_to_find', UINT, 'tbd'), @@ -135,13 +135,13 @@ def_module_params('sat', # ('xor.allow_elim_vars', BOOL, 'tbd'), # ('xor.var_per_cut', UINT, 'tbd'), # ('xor.force_preserve_xors', BOOL, 'tbd'), - # ('xor.gauss.max_matrix_columns', UINT, 'tbd'), - # ('xor.gauss.max_matrix_rows', UINT, 'The maximum matrix size -- no. of rows'), - # ('xor.gauss.min_matrix_rows', UINT, 'The minimum matrix size -- no. of rows'), - # ('xor.gauss.max_num_matrices', UINT, 'Maximum number of matrices'), + ('xor.gauss.max_matrix_columns', UINT, UINT_MAX, 'tbd'), + ('xor.gauss.max_matrix_rows', UINT, UINT_MAX, 'The maximum matrix size -- no. of rows'), + ('xor.gauss.min_matrix_rows', UINT, 0, 'The minimum matrix size -- no. of rows'), + ('xor.gauss.max_num_matrices', UINT, UINT_MAX, 'Maximum number of matrices'), # ('xor.gauss.autodisable', BOOL, False, 'tbd'), # ('xor.gauss.min_usefulness_cutoff', DOUBLE, 0, 'tbd'), # ('xor.gauss.do_matrix_find', BOOL, True, 'tbd'), # ('xor.gauss.min_xor_clauses', UINT, 2, 'tbd'), # ('xor.gauss.max_xor_clauses, UINT, 500000, 'tbd') - ) + )) diff --git a/src/sat/smt/xor_matrix_finder.cpp b/src/sat/smt/xor_matrix_finder.cpp index 56954525e..a2883faeb 100644 --- a/src/sat/smt/xor_matrix_finder.cpp +++ b/src/sat/smt/xor_matrix_finder.cpp @@ -106,7 +106,6 @@ namespace xr { } uint32_t xor_matrix_finder::set_matrixes() { - return 0; svector matrix_shapes; svector> xors_in_matrix(m_matrix_no); @@ -116,7 +115,7 @@ namespace xr { matrix_shapes[i].m_num = i; matrix_shapes[i].m_cols = m_reverseTable[i].size(); } -#if 0 + for (constraint* x : m_xor.m_constraints) { //take 1st variable to check which matrix it's in. const uint32_t matrix = m_table[(*x)[0]]; @@ -127,14 +126,14 @@ namespace xr { matrix_shapes[matrix].m_sum_xor_sizes += x->get_size(); xors_in_matrix[matrix].push_back(x); } - m_solver->m_constraints.clear(); + + m_xor.m_constraints.clear(); - for(auto& m: matrix_shapes) { - if (m.tot_size() > 0) { + for (auto& m: matrix_shapes) + if (m.tot_size() > 0) m.m_density = (double)m.m_sum_xor_sizes / (double)(m.tot_size()); - } - } - + + std::sort(matrix_shapes.begin(), matrix_shapes.end(), m_sorter); uint32_t realMatrixNum = 0; @@ -144,65 +143,61 @@ namespace xr { for (unsigned a = m_matrix_no; a-- > 0; ) { matrix_shape& m = matrix_shapes[a]; uint32_t i = m.m_num; - if (m.m_rows == 0) { - continue; - } + if (m.m_rows == 0) + continue; bool use_matrix = true; - - //Over- or undersized - if (use_matrix && m.m_rows > m_solver->conf.gaussconf.max_matrix_rows) { + // Over- or undersized + + // Too many rows in matrix + if (use_matrix && m.m_rows > m_sat.get_config().m_xor_gauss_max_matrix_rows) use_matrix = false; - // Too many rows in matrix - } - if (use_matrix && m.m_cols > m_solver->conf.gaussconf.max_matrix_columns) { + + // Too many columns in matrix + if (use_matrix && m.m_cols > m_sat.get_config().m_xor_gauss_max_matrix_columns) use_matrix = false; - // Too many columns in matrix - } + + // Too few rows in matrix + if (use_matrix && m.m_rows < m_sat.get_config().m_xor_gauss_min_matrix_rows) + use_matrix = false, too_few_rows_matrix++; - if (use_matrix && m.m_rows < m_solver->conf.gaussconf.min_matrix_rows) { + // Over the max number of matrixes + if (use_matrix && realMatrixNum >= m_sat.get_config().m_xor_gauss_max_num_matrices) use_matrix = false; - too_few_rows_matrix++; - // Too few rows in matrix - } - - //Over the max number of matrixes - if (use_matrix && realMatrixNum >= m_solver->conf.gaussconf.max_num_matrices) { - // above max number of matrixes - use_matrix = false; - } - - //if already detached, we MUST use the matrix - for(const auto& x: xors_in_matrix[i]) { + + // if already detached, we MUST use the matrix + for (const auto& x: xors_in_matrix[i]) { if (x->is_detached()) { use_matrix = true; break; } } - if (m_solver->conf.force_use_all_matrixes) { +#if 0 + if (m_sat.get_config().force_use_all_matrixes) { use_matrix = true; } +#endif +#if 0 if (use_matrix) { - m_solver->gmatrices.push_back( - new EGaussian(m_solver, realMatrixNum, xors_in_matrix[i])); - m_solver->gqueuedata.resize(m_solver->gmatrices.size()); + m_xor.gmatrices.push_back( + alloc(EGaussian, m_xor, realMatrixNum, xors_in_matrix[i])); + m_xor.gqueuedata.resize(m_solver->gmatrices.size()); realMatrixNum++; SASSERT(m_solver->gmatrices.size() == realMatrixNum); - } else { + } + else { for (auto& x: xors_in_matrix[i]) { - m_solver->xorclauses_unused.push_back(x); - //cout<< "c [matrix]xor not in matrix, now unused_xors size: " << unused_xors.size() << endl; + m_xor.xorclauses_unused.push_back(x); clash_vars_unused.insert(x.clash_vars.begin(), x.clash_vars.end()); } unusedMatrix++; } - } - - return realMatrixNum; #endif + } + return realMatrixNum; } } diff --git a/src/sat/smt/xor_solver.h b/src/sat/smt/xor_solver.h index 6613c3a6d..c06ea0e52 100644 --- a/src/sat/smt/xor_solver.h +++ b/src/sat/smt/xor_solver.h @@ -19,7 +19,7 @@ Abstract: namespace xr { class constraint { - size_t m_size; + unsigned m_size; bool m_detached; size_t m_obj_size; bool m_rhs; @@ -37,7 +37,7 @@ namespace xr { void deallocate(small_object_allocator& a) { a.deallocate(m_obj_size, sat::constraint_base::mem2base_ptr(this)); } sat::bool_var operator[](unsigned i) const { return m_vars[i]; } bool is_detached() const { return m_detached; } - size_t get_size() const { return m_size; } + unsigned get_size() const { return m_size; } bool get_rhs() const { return m_rhs; } sat::bool_var const* begin() const { return m_vars; } sat::bool_var const* end() const { return m_vars + m_size; } @@ -50,8 +50,14 @@ namespace xr { }; class solver : public euf::th_solver { + friend class xor_matrix_finder; + + euf::solver* m_ctx = nullptr; sat::sat_internalizer& si; + + ptr_vector m_constraints; + public: solver(euf::solver& ctx); solver(ast_manager& m, sat::sat_internalizer& si, euf::theory_id id);