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

annotate arith_sls

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-02-12 20:55:44 -08:00
parent bb81bc5452
commit 7956cf1201
3 changed files with 16 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/sat/sat_ddfw.h
View file

@ -52,6 +52,7 @@ namespace sat {
p(p), i(lit.index()) {}
unsigned const* begin() { return p.m_flat_use_list.data() + p.m_use_list_index[i]; }
unsigned const* end() { return p.m_flat_use_list.data() + p.m_use_list_index[i + 1]; }
unsigned size() const { return p.m_use_list_index[i + 1] - p.m_use_list_index[i]; }
};
protected:

13
src/sat/smt/arith_sls.cpp
View file

@ -90,6 +90,7 @@ namespace arith {
rational new_value_(new_value, rational::i64());
lp::impq val(new_value_, rational::zero());
s.lp().set_value_for_nbasic_column(vj.index(), val);
// TODO - figure out why this leads to unsound (unsat).
}
}
}
@ -147,6 +148,11 @@ namespace arith {
}
}
//
// dtt is high overhead. It walks ineq.m_args
// m_vars[w].m_value can be computed outside and shared among calls
// different data-structures for storing coefficients
//
int64_t sls::dtt(ineq const& ineq, var_t v, int64_t new_value) const {
auto new_args_value = ineq.m_args_value;
for (auto const& [coeff, w] : ineq.m_args) {
@ -302,6 +308,12 @@ namespace arith {
return score;
}
//
// cm_score is costly. It involves several cache misses.
// Note that
// - m_bool_search->get_use_list(lit).size() is "often" 1 or 2
// - dtt_old can be saved
//
int sls::cm_score(var_t v, int64_t new_value) {
int score = 0;
auto& vi = m_vars[v];
@ -309,6 +321,7 @@ namespace arith {
auto const& ineq = *atom(lit);
int64_t dtt_old = dtt(ineq);
int64_t dtt_new = dtt(ineq, v, new_value);
for (auto cl : m_bool_search->get_use_list(lit)) {
auto const& clause = get_clause_info(cl);
if (!clause.is_true()) {

7
src/sat/smt/euf_local_search.cpp
View file

@ -81,11 +81,8 @@ namespace euf {
return;
}
euf::enode* n = m_egraph.find(m_bool_var2expr.get(l.var(), nullptr));
for (auto const& thv : enode_th_vars(n)) {
auto* th = m_id2solver.get(thv.get_id(), nullptr);
if (th)
th->set_bounds(n);
}
for (auto* s : m_solvers)
s->set_bounds(n);
};
for (auto cl : bool_search.unsat_set()) {