mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-04 10:20:23 +00:00
Code Activity

more

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-10-28 20:27:53 -07:00
parent 47fd9d8e18
commit 31a6992609
2 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -63,7 +63,7 @@ namespace xr {
finder.move_xors_without_connecting_vars_to_unused(); finder.move_xors_without_connecting_vars_to_unused();
finder.clean_equivalent_xors(m_solver->xorclauses); finder.clean_equivalent_xors(m_solver->xorclauses);
for(const auto& x: m_xor.xorclauses_unused) for (const auto& x: m_xor.xorclauses_unused)
clash_vars_unused.insert(x.clash_vars.begin(), x.clash_vars.end()); clash_vars_unused.insert(x.clash_vars.begin(), x.clash_vars.end());
if (m_xor.xorclauses.size() < m_sat.get_config().m_min_gauss_xor_clauses) { if (m_xor.xorclauses.size() < m_sat.get_config().m_min_gauss_xor_clauses) {
@ -73,9 +73,9 @@ namespace xr {
//Just one giant matrix. //Just one giant matrix.
// if (m_sat.get_config().m_xor_gauss_do_matrix_find) // if (m_sat.get_config().m_xor_gauss_do_matrix_find)
if (!m_solver->conf.gaussconf.doMatrixFind) { if (!m_sat.get_config().m_xor_doMatrixFind) {
m_solver->gmatrices.push_back(new EGaussian(m_solver, 0, m_solver->xorclauses)); m_xor.gmatrices.push_back(new EGaussian(m_xor, 0, m_xor.xorclauses));
m_solver->gqueuedata.resize(m_solver->gmatrices.size()); m_xor.gqueuedata.resize(m_xor.gmatrices.size());
return true; return true;
} }

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

@ -20,7 +20,7 @@ namespace xr {
class constraint { class constraint {
unsigned m_size; unsigned m_size;
bool m_detached; bool m_detached = false;
size_t m_obj_size; size_t m_obj_size;
bool m_rhs; bool m_rhs;
sat::bool_var m_vars[0]; sat::bool_var m_vars[0];
@ -28,7 +28,7 @@ namespace xr {
public: public:
static size_t get_obj_size(unsigned num_lits) { return sat::constraint_base::obj_size(sizeof(constraint) + num_lits * sizeof(sat::bool_var)); } static size_t get_obj_size(unsigned num_lits) { return sat::constraint_base::obj_size(sizeof(constraint) + num_lits * sizeof(sat::bool_var)); }
constraint(const svector<sat::bool_var>& ids, bool expected_result) : m_size(ids.size()), m_detached(false), m_obj_size(get_obj_size(ids.size())), m_rhs(expected_result) { constraint(const svector<sat::bool_var>& ids, bool expected_result) : m_size(ids.size()), m_obj_size(get_obj_size(ids.size())), m_rhs(expected_result) {
unsigned i = 0; unsigned i = 0;
for (auto v : ids) for (auto v : ids)
m_vars[i++] = v; m_vars[i++] = v;