mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

porting more

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-10-28 19:52:37 -07:00
parent bfb3db8b13
commit d08e61219b
5 changed files with 65 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/sat/sat_config.cpp
View file

@ -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();

9
src/sat/sat_config.h
View file

@ -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);

12
src/sat/sat_params.pyg
View file

@ -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')
)
))

79
src/sat/smt/xor_matrix_finder.cpp
View file

@ -106,7 +106,6 @@ namespace xr {
}
uint32_t xor_matrix_finder::set_matrixes() {
return 0;
svector<matrix_shape> matrix_shapes;
svector<ptr_vector<constraint>> 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;
}
}

10
src/sat/smt/xor_solver.h
View file

@ -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<constraint> m_constraints;
public:
solver(euf::solver& ctx);
solver(ast_manager& m, sat::sat_internalizer& si, euf::theory_id id);