mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

don't store full use list of clauses to avoid space overhead

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-01-21 13:23:13 -08:00
parent fb0eb029a8
commit eebff13f8b
3 changed files with 30 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/ast/sls/sls_arith_base.cpp
View file

@ -1436,13 +1436,6 @@ namespace sls {
for (auto const& [coeff, bv] : ui.m_linear_occurs) for (auto const& [coeff, bv] : ui.m_linear_occurs)
vi.m_bool_vars_of.insert(bv); vi.m_bool_vars_of.insert(bv);
} }
;
for (auto bv : vi.m_bool_vars_of) {
for (auto i : ctx.get_use_list(sat::literal(bv, true)))
vi.m_clauses_of.insert(i);
for (auto i : ctx.get_use_list(sat::literal(bv, false)))
vi.m_clauses_of.insert(i);
}
} }
template<typename num_t> template<typename num_t>

1
src/ast/sls/sls_arith_base.h
View file

@ -120,7 +120,6 @@ namespace sls {
unsigned m_def_idx = UINT_MAX; unsigned m_def_idx = UINT_MAX;
vector<std::pair<num_t, sat::bool_var>> m_linear_occurs; vector<std::pair<num_t, sat::bool_var>> m_linear_occurs;
indexed_uint_set m_bool_vars_of; indexed_uint_set m_bool_vars_of;
indexed_uint_set m_clauses_of;
unsigned_vector m_muls; unsigned_vector m_muls;
unsigned_vector m_adds; unsigned_vector m_adds;
optional<bound> m_lo, m_hi; optional<bound> m_lo, m_hi;

55
src/ast/sls/sls_arith_clausal.cpp
View file

@ -286,32 +286,38 @@ namespace sls {
if (!a.update_num(v, delta)) if (!a.update_num(v, delta))
return -1; return -1;
double score = 0; double score = 0;
for (auto ci : vi.m_clauses_of) { for (auto bv : vi.m_bool_vars_of) {
auto const& c = ctx.get_clause(ci); for (auto lit : { sat::literal(bv, false), sat::literal(bv, true) }) {
unsigned num_true = 0; for (auto ci : ctx.get_use_list(lit)) {
for (auto lit : c) { auto const& c = ctx.get_clause(ci);
auto bv = lit.var(); unsigned num_true = 0;
auto ineq = a.get_ineq(bv); for (auto lit : c) {
if (ineq) { auto bv = lit.var();
if (ineq->is_true() != lit.sign()) auto ineq = a.get_ineq(bv);
++num_true; if (ineq) {
if (ineq->is_true() != lit.sign())
++num_true;
}
else if (ctx.is_true(lit))
++num_true;
}
CTRACE("arith_verbose", c.m_num_trues != num_true && (c.m_num_trues == 0 || num_true == 0),
tout << "clause: " << c
<< " v" << v << " += " << delta
<< " new-true lits: " << num_true
<< " old-true lits: " << c.m_num_trues
<< " w: " << c.m_weight << "\n";
for (auto lit : c)
if (a.get_ineq(lit.var()))
tout << lit << " " << *a.get_ineq(lit.var()) << "\n";);
if (c.m_num_trues > 0 && num_true == 0)
score -= c.m_weight;
else if (c.m_num_trues == 0 && num_true > 0)
score += c.m_weight;
} }
else if (ctx.is_true(lit))
++num_true;
} }
CTRACE("arith_verbose", c.m_num_trues != num_true && (c.m_num_trues == 0 || num_true == 0),
tout << "clause: " << c
<< " v" << v << " += " << delta
<< " new-true lits: " << num_true
<< " old-true lits: " << c.m_num_trues
<< " w: " << c.m_weight << "\n";
for (auto lit : c)
if (a.get_ineq(lit.var()))
tout << lit << " " << *a.get_ineq(lit.var()) << "\n";);
if (c.m_num_trues > 0 && num_true == 0)
score -= c.m_weight;
else if (c.m_num_trues == 0 && num_true > 0)
score += c.m_weight;
} }
// revert the update // revert the update
@ -336,7 +342,6 @@ namespace sls {
else else
vi.set_value(num_t(0)); vi.set_value(num_t(0));
vi.m_bool_vars_of.reset(); vi.m_bool_vars_of.reset();
vi.m_clauses_of.reset();
} }
initialize(); initialize();
} }