mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-02 17:30:23 +00:00
Code Activity

Bugfix polarity + Bugfix memory allocation

Browse source
This commit is contained in:
CEisenhofer 2022-12-05 15:22:59 +01:00
parent 662019ee17
commit f22aa0eec5
3 changed files with 23 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/sat/smt/xor_gaussian.cpp
View file

@ -98,11 +98,12 @@ gret PackedRow::propGause(
PackedRow& tmp_col2, PackedRow& tmp_col2,
PackedRow& cols_vals, PackedRow& cols_vals,
PackedRow& cols_unset, PackedRow& cols_unset,
sat::literal& ret_lit_prop) { literal& ret_lit_prop) {
unsigned pop = tmp_col.set_and_until_popcnt_atleast2(*this, cols_unset); unsigned pop = tmp_col.set_and_until_popcnt_atleast2(*this, cols_unset);
//Find new watch // There are still at least 2 unassigned elements in the matrix row
// Find new watch ==> a variable not yet having a row responsible for it
if (pop >= 2) { if (pop >= 2) {
for (int i = 0; i < size; i++) { for (int i = 0; i < size; i++) {
if (!tmp_col.mp[i]) if (!tmp_col.mp[i])
@ -130,7 +131,7 @@ gret PackedRow::propGause(
} }
} }
//Calc value of row // Calc value of row by bitwise-anding the current model and the row
tmp_col2.set_and(*this, cols_vals); tmp_col2.set_and(*this, cols_vals);
unsigned pop_t = tmp_col2.popcnt() + (unsigned)rhs(); unsigned pop_t = tmp_col2.popcnt() + (unsigned)rhs();
@ -153,7 +154,7 @@ gret PackedRow::propGause(
unsigned col = (at - 1) + i * 64; unsigned col = (at - 1) + i * 64;
SASSERT(tmp_col[col] == 1); SASSERT(tmp_col[col] == 1);
unsigned var = column_to_var[col]; unsigned var = column_to_var[col];
ret_lit_prop = literal(var,pop_t % 2); ret_lit_prop = literal(var, !(pop_t % 2));
return gret::prop; return gret::prop;
} }
@ -1049,7 +1050,7 @@ bool EGaussian::check_row_satisfied(unsigned row) {
bool fin = m_mat[row].rhs(); bool fin = m_mat[row].rhs();
for (unsigned i = 0; i < m_num_cols; i++) { for (unsigned i = 0; i < m_num_cols; i++) {
if (m_mat[row][i]) { if (m_mat[row][i]) {
unsigned var = m_column_to_var[i]; bool_var var = m_column_to_var[i];
auto val = m_solver.s().value(var); auto val = m_solver.s().value(var);
if (val == l_undef) { if (val == l_undef) {
TRACE("xor", tout << "Var " << var+1 << " col: " << i << " is undef!\n";); TRACE("xor", tout << "Var " << var+1 << " col: " << i << " is undef!\n";);

15
src/sat/smt/xor_solver.cpp
View file

@ -22,11 +22,14 @@ Abstract:
namespace xr { namespace xr {
solver::solver(euf::solver& ctx) : solver::solver(euf::solver& ctx) :
solver(ctx.get_manager(), ctx.get_manager().mk_family_id("xor")) { euf::th_solver(
m_ctx = &ctx; ctx.get_manager(), symbol("xor"),
} ctx.get_manager().mk_family_id("xor")),
m_ctx(&ctx), m_region() { }
solver::solver(ast_manager& m, euf::theory_id id) : euf::th_solver(m, symbol("xor"), id) { } solver::solver(ast_manager& m, euf::theory_id id) :
euf::th_solver(m, symbol("xor"), id),
m_ctx(nullptr), m_region(region()) { }
solver::~solver() { solver::~solver() {
/*for (justification* j : m_justifications) { /*for (justification* j : m_justifications) {
@ -551,8 +554,8 @@ namespace xr {
} }
} }
sat::justification solver::mk_justification(const int level, const unsigned int matrix_no, const unsigned int row_i) { sat::justification solver::mk_justification(int level, unsigned matrix_no, unsigned row_i) {
void* mem = m_ctx->get_region().allocate(justification::get_obj_size()); void* mem = get_region().allocate(justification::get_obj_size());
sat::constraint_base::initialize(mem, this); sat::constraint_base::initialize(mem, this);
auto* constraint = new (sat::constraint_base::ptr2mem(mem)) justification(matrix_no, row_i); auto* constraint = new (sat::constraint_base::ptr2mem(mem)) justification(matrix_no, row_i);
return sat::justification::mk_ext_justification(level, constraint->to_index()); return sat::justification::mk_ext_justification(level, constraint->to_index());

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

@ -37,6 +37,8 @@ namespace xr {
// ptr_vector<justification> m_justifications; // ptr_vector<justification> m_justifications;
// unsigned_vector m_justifications_lim; // unsigned_vector m_justifications_lim;
optional<region> m_region;
bool_var_vector m_tmp_xor_clash_vars; bool_var_vector m_tmp_xor_clash_vars;
vector<xor_clause> m_xorclauses; vector<xor_clause> m_xorclauses;
@ -66,6 +68,10 @@ namespace xr {
void push_core(); void push_core();
void pop_core(unsigned num_scopes); void pop_core(unsigned num_scopes);
region& get_region() {
return m_ctx != nullptr ? m_ctx->get_region() : *m_region;
}
bool xor_has_interesting_var(const xor_clause& x); bool xor_has_interesting_var(const xor_clause& x);
void clean_xor_no_prop(literal_vector& ps, bool& rhs); void clean_xor_no_prop(literal_vector& ps, bool& rhs);
@ -125,7 +131,7 @@ namespace xr {
bool xor_together_xors(vector<xor_clause>& xors); bool xor_together_xors(vector<xor_clause>& xors);
sat::justification mk_justification(const int level, const unsigned int matrix_no, const unsigned int row_i); sat::justification mk_justification(int level, unsigned matrix_no, unsigned row_i);
std::ostream& display(std::ostream& out) const override; std::ostream& display(std::ostream& out) const override;
std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override; std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;