Skip to content

Commit c7ea496

Browse files
NikolajBjornerNikolajBjorner
committedNov 17, 2024·
bug fixes to sls
·
z3-4.14.1z3-4.13.4
1 parent e380903 commit c7ea496

File tree

7 files changed

+84
-139
lines changed

7 files changed

+84
-139
lines changed
 

Diff for: ‎src/ast/sls/sls_arith_base.cpp

+23-98
Original file line numberDiff line numberDiff line change
@@ -59,8 +59,6 @@ namespace sls {
5959
}
6060
}
6161

62-
63-
6462
template<typename num_t>
6563
std::ostream& arith_base<num_t>::ineq::display(std::ostream& out) const {
6664
bool first = true;
@@ -118,7 +116,7 @@ namespace sls {
118116
template<typename num_t>
119117
void arith_base<num_t>::save_best_values() {
120118
for (auto& v : m_vars)
121-
v.m_best_value = v.m_value;
119+
v.set_best_value(v.value());
122120
check_ineqs();
123121
}
124122

@@ -168,8 +166,8 @@ namespace sls {
168166
template<typename num_t>
169167
num_t arith_base<num_t>::dtt(bool sign, ineq const& ineq, var_t v, num_t const& new_value) const {
170168
for (auto const& [coeff, w] : ineq.m_args)
171-
if (w == v)
172-
return dtt(sign, ineq.m_args_value + coeff * (new_value - m_vars[v].m_value), ineq);
169+
if (w == v)
170+
return dtt(sign, ineq.m_args_value + coeff * (new_value - m_vars[v].value()), ineq);
173171
return num_t(1);
174172
}
175173

@@ -444,17 +442,19 @@ namespace sls {
444442

445443
delta_out = delta;
446444

447-
if (m_last_var == v && m_last_delta == -delta)
448-
return false;
445+
if (m_last_var == v && m_last_delta == -delta)
446+
return false;
449447

450-
if (m_use_tabu && vi.is_tabu(m_stats.m_num_steps, delta))
448+
if (m_use_tabu && vi.is_tabu(m_stats.m_num_steps, delta))
451449
return false;
450+
452451

453452
auto old_value = value(v);
454453
auto new_value = old_value + delta;
455454
if (!vi.in_range(new_value))
456455
return false;
457456

457+
458458
if (m_use_tabu && !in_bounds(v, new_value) && in_bounds(v, old_value)) {
459459
auto const& lo = m_vars[v].m_lo;
460460
auto const& hi = m_vars[v].m_hi;
@@ -490,9 +490,7 @@ namespace sls {
490490
void arith_base<num_t>::add_update(var_t v, num_t delta) {
491491
num_t delta_out;
492492
if (!is_permitted_update(v, delta, delta_out))
493-
return;
494-
495-
493+
return;
496494
m_updates.push_back({ v, delta_out, 0 });
497495
}
498496

@@ -647,7 +645,7 @@ namespace sls {
647645
bool arith_base<num_t>::update(var_t v, num_t const& new_value) {
648646
auto& vi = m_vars[v];
649647
expr* e = vi.m_expr;
650-
auto old_value = vi.m_value;
648+
auto old_value = vi.value();
651649
if (old_value == new_value)
652650
return true;
653651
if (!vi.in_range(new_value))
@@ -665,15 +663,10 @@ namespace sls {
665663
}
666664
}
667665
catch (overflow_exception const&) {
666+
verbose_stream() << "overflow1\n";
668667
return false;
669668
}
670669

671-
#if 0
672-
if (!check_update(v, new_value))
673-
return false;
674-
apply_checked_update();
675-
#else
676-
677670
buffer<sat::bool_var> to_flip;
678671
for (auto const& [coeff, bv] : vi.m_bool_vars) {
679672
auto& ineq = *atom(bv);
@@ -687,12 +680,13 @@ namespace sls {
687680

688681
}
689682
IF_VERBOSE(5, verbose_stream() << "repair: v" << v << " := " << old_value << " -> " << new_value << "\n");
690-
vi.m_value = new_value;
683+
vi.set_value(new_value);
691684
ctx.new_value_eh(e);
692685
m_last_var = v;
693686

694687
for (auto bv : to_flip) {
695-
ctx.flip(bv);
688+
if (dtt(sign(bv), *atom(bv)) != 0)
689+
ctx.flip(bv);
696690
SASSERT(dtt(sign(bv), *atom(bv)) == 0);
697691
}
698692

@@ -711,6 +705,7 @@ namespace sls {
711705
prod *= power_of(value(w), p);
712706
}
713707
catch (overflow_exception const&) {
708+
verbose_stream() << "overflow\n";
714709
return false;
715710
}
716711
if (value(w) != prod && !update(w, prod))
@@ -727,82 +722,10 @@ namespace sls {
727722
if (!update(ad.m_var, sum))
728723
return false;
729724
}
730-
#endif
731-
732-
return true;
733-
}
734-
735-
template<typename num_t>
736-
bool arith_base<num_t>::check_update(var_t v, num_t new_value) {
737-
738-
++m_update_timestamp;
739-
if (m_update_timestamp == 0) {
740-
for (auto& vi : m_vars)
741-
vi.set_update_value(num_t(0), 0);
742-
++m_update_timestamp;
743-
}
744-
auto& vi = m_vars[v];
745-
m_update_trail.reset();
746-
m_update_trail.push_back(v);
747-
vi.set_update_value(new_value, m_update_timestamp);
748-
749-
num_t delta;
750-
for (unsigned i = 0; i < m_update_trail.size(); ++i) {
751-
auto v = m_update_trail[i];
752-
auto& vi = m_vars[v];
753-
for (auto idx : vi.m_muls) {
754-
auto const& [w, monomial] = m_muls[idx];
755-
num_t prod(1);
756-
try {
757-
for (auto [w, p] : monomial)
758-
prod *= power_of(get_update_value(w), p);
759-
}
760-
catch (overflow_exception const&) {
761-
return false;
762-
}
763-
if (get_update_value(w) != prod && (!is_permitted_update(w, prod - value(w), delta) || prod - value(w) != delta))
764-
return false;
765-
m_update_trail.push_back(w);
766-
m_vars[w].set_update_value(prod, m_update_timestamp);
767-
}
768725

769-
for (auto idx : vi.m_adds) {
770-
auto const& ad = m_adds[idx];
771-
auto w = ad.m_var;
772-
num_t sum(ad.m_coeff);
773-
for (auto const& [coeff, w] : ad.m_args)
774-
sum += coeff * get_update_value(w);
775-
if (get_update_value(v) != sum && !(is_permitted_update(w, sum - value(w), delta) || sum - value(w) != delta))
776-
return false;
777-
m_update_trail.push_back(w);
778-
m_vars[w].set_update_value(sum, m_update_timestamp);
779-
}
780-
}
781726
return true;
782727
}
783-
784-
template<typename num_t>
785-
void arith_base<num_t>::apply_checked_update() {
786-
for (auto v : m_update_trail) {
787-
auto & vi = m_vars[v];
788-
auto old_value = vi.m_value;
789-
vi.m_value = vi.get_update_value(m_update_timestamp);
790-
auto new_value = vi.m_value;
791-
ctx.new_value_eh(vi.m_expr);
792-
for (auto const& [coeff, bv] : vi.m_bool_vars) {
793-
auto& ineq = *atom(bv);
794-
bool old_sign = sign(bv);
795-
sat::literal lit(bv, old_sign);
796-
SASSERT(ctx.is_true(lit));
797-
ineq.m_args_value += coeff * (new_value - old_value);
798-
num_t dtt_new = dtt(old_sign, ineq);
799-
if (dtt_new != 0)
800-
ctx.flip(bv);
801-
SASSERT(dtt(sign(bv), ineq) == 0);
802-
}
803-
}
804-
}
805-
728+
806729
template<typename num_t>
807730
typename arith_base<num_t>::ineq& arith_base<num_t>::new_ineq(ineq_kind op, num_t const& coeff) {
808731
auto* i = alloc(ineq);
@@ -906,7 +829,7 @@ namespace sls {
906829
m_vars[w].m_muls.push_back(idx), prod *= power_of(value(w), p);
907830
m_vars[v].m_def_idx = idx;
908831
m_vars[v].m_op = arith_op_kind::OP_MUL;
909-
m_vars[v].m_value = prod;
832+
m_vars[v].set_value(prod);
910833
add_arg(term, coeff, v);
911834
break;
912835
}
@@ -972,7 +895,7 @@ namespace sls {
972895
m_ops.push_back({v, k, v, w});
973896
m_vars[v].m_def_idx = idx;
974897
m_vars[v].m_op = k;
975-
m_vars[v].m_value = val;
898+
m_vars[v].set_value(val);
976899
return v;
977900
}
978901

@@ -993,7 +916,7 @@ namespace sls {
993916
m_vars[w].m_adds.push_back(idx), sum += c * value(w);
994917
m_vars[v].m_def_idx = idx;
995918
m_vars[v].m_op = arith_op_kind::OP_ADD;
996-
m_vars[v].m_value = sum;
919+
m_vars[v].set_value(sum);
997920
return v;
998921
}
999922

@@ -1055,6 +978,7 @@ namespace sls {
1055978
else {
1056979
SASSERT(!a.is_arith_expr(e));
1057980
}
981+
1058982
}
1059983

1060984
template<typename num_t>
@@ -1345,6 +1269,7 @@ namespace sls {
13451269
hi_valid = false;
13461270
}
13471271
catch (overflow_exception&) {
1272+
verbose_stream() << "overflow3\n";
13481273
hi_valid = false;
13491274
}
13501275
}
@@ -2021,7 +1946,7 @@ namespace sls {
20211946
if (is_num(e, n))
20221947
return expr_ref(a.mk_numeral(n.to_rational(), a.is_int(e)), m);
20231948
auto v = mk_term(e);
2024-
return expr_ref(a.mk_numeral(m_vars[v].m_value.to_rational(), a.is_int(e)), m);
1949+
return expr_ref(a.mk_numeral(m_vars[v].value().to_rational(), a.is_int(e)), m);
20251950
}
20261951

20271952
template<typename num_t>
@@ -2112,7 +2037,7 @@ namespace sls {
21122037
auto const& vi = m_vars[v];
21132038
auto const& lo = vi.m_lo;
21142039
auto const& hi = vi.m_hi;
2115-
out << "v" << v << " := " << vi.m_value << " ";
2040+
out << "v" << v << " := " << vi.value() << " ";
21162041
if (lo || hi) {
21172042
if (lo)
21182043
out << (lo->is_strict ? "(": "[") << lo->value;

Diff for: ‎src/ast/sls/sls_arith_base.h

+33-23
Original file line numberDiff line numberDiff line change
@@ -76,13 +76,14 @@ namespace sls {
7676

7777
class var_info {
7878
num_t m_range{ 100000000 };
79-
num_t m_update_value{ 0 };
80-
unsigned m_update_timestamp = 0;
79+
unsigned m_num_out_of_range = 0;
80+
unsigned m_num_in_range = 0;
81+
num_t m_value{ 0 };
82+
num_t m_best_value{ 0 };
8183
public:
8284
var_info(expr* e, var_sort k): m_expr(e), m_sort(k) {}
8385
expr* m_expr;
84-
num_t m_value{ 0 };
85-
num_t m_best_value{ 0 };
86+
8687
var_sort m_sort;
8788
arith_op_kind m_op = arith_op_kind::LAST_ARITH_OP;
8889
unsigned m_def_idx = UINT_MAX;
@@ -91,23 +92,27 @@ namespace sls {
9192
unsigned_vector m_adds;
9293
optional<bound> m_lo, m_hi;
9394

94-
// retrieve temporary value during an update.
95-
void set_update_value(num_t const& v, unsigned timestamp) {
96-
m_update_value = v;
97-
m_update_timestamp = timestamp;
98-
}
99-
num_t const& get_update_value(unsigned ts) const {
100-
return ts == m_update_timestamp ? m_update_value : m_value;
101-
}
95+
num_t const& value() const { return m_value; }
96+
void set_value(num_t const& v) { m_value = v; }
97+
98+
num_t const& best_value() const { return m_best_value; }
99+
void set_best_value(num_t const& v) { m_best_value = v; }
102100

103-
bool in_range(num_t const& n) const {
101+
bool in_range(num_t const& n) {
104102
if (-m_range < n && n < m_range)
105103
return true;
104+
bool result = false;
106105
if (m_lo && !m_hi)
107-
return n < m_lo->value + m_range;
108-
if (!m_lo && m_hi)
109-
return n > m_hi->value - m_range;
110-
return false;
106+
result = n < m_lo->value + m_range;
107+
else if (!m_lo && m_hi)
108+
result = n > m_hi->value - m_range;
109+
#if 0
110+
if (!result)
111+
out_of_range();
112+
else
113+
++m_num_in_range;
114+
#endif
115+
return result;
111116
}
112117
unsigned m_tabu_pos = 0, m_tabu_neg = 0;
113118
unsigned m_last_pos = 0, m_last_neg = 0;
@@ -120,6 +125,15 @@ namespace sls {
120125
else
121126
m_tabu_neg = tabu_step, m_last_neg = step;
122127
}
128+
void out_of_range() {
129+
++m_num_out_of_range;
130+
if (m_num_out_of_range < 1000 * (1 + m_num_in_range))
131+
return;
132+
IF_VERBOSE(2, verbose_stream() << "increase range " << m_range << "\n");
133+
m_range *= 2;
134+
m_num_out_of_range = 0;
135+
m_num_in_range = 0;
136+
}
123137
};
124138

125139
struct mul_def {
@@ -187,10 +201,7 @@ namespace sls {
187201

188202
void add_update(var_t v, num_t delta);
189203
bool is_permitted_update(var_t v, num_t const& delta, num_t& delta_out);
190-
unsigned m_update_timestamp = 0;
191-
svector<var_t> m_update_trail;
192-
bool check_update(var_t v, num_t new_value);
193-
void apply_checked_update();
204+
194205

195206
num_t value1(var_t v);
196207

@@ -247,8 +258,7 @@ namespace sls {
247258

248259
bool is_int(var_t v) const { return m_vars[v].m_sort == var_sort::INT; }
249260

250-
num_t value(var_t v) const { return m_vars[v].m_value; }
251-
num_t const& get_update_value(var_t v) const { return m_vars[v].get_update_value(m_update_timestamp); }
261+
num_t value(var_t v) const { return m_vars[v].value(); }
252262
bool is_num(expr* e, num_t& i);
253263
expr_ref from_num(sort* s, num_t const& n);
254264
void check_ineqs();

Diff for: ‎src/ast/sls/sls_arith_plugin.cpp

+3-7
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ namespace sls {
2727
return m_arith64->_fn_;\
2828
}\
2929
catch (overflow_exception&) {\
30-
throw;\
30+
IF_VERBOSE(1, verbose_stream() << "revert to bignum solver " << #_fn_ << "\n");\
3131
init_backup();\
3232
}\
3333
}\
@@ -39,7 +39,7 @@ namespace sls {
3939
m_arith64->_fn_;\
4040
}\
4141
catch (overflow_exception&) {\
42-
throw;\
42+
IF_VERBOSE(1, verbose_stream() << "revert to bignum solver " << #_fn_ << "\n");\
4343
init_backup();\
4444
}\
4545
}\
@@ -49,11 +49,7 @@ namespace sls {
4949
plugin(ctx), m_shared(ctx.get_manager()) {
5050
m_arith64 = alloc(arith_base<checked_int64<true>>, ctx);
5151
m_arith = alloc(arith_base<rational>, ctx);
52-
m_arith64 = nullptr;
53-
if (m_arith)
54-
m_fid = m_arith->fid();
55-
else
56-
m_fid = m_arith64->fid();
52+
m_fid = m_arith->fid();
5753
}
5854

5955
void arith_plugin::init_backup() {

Diff for: ‎src/ast/sls/sls_smt_plugin.cpp

+7-4
Original file line numberDiff line numberDiff line change
@@ -115,7 +115,7 @@ namespace sls {
115115
m_ddfw->rlimit().pop();
116116
}
117117

118-
void smt_plugin::finalize(model_ref& mdl, ::statistics& st) {
118+
void smt_plugin::finalize(model_ref& mdl) {
119119
auto* d = m_ddfw;
120120
if (!d)
121121
return;
@@ -126,7 +126,6 @@ namespace sls {
126126
if (m_thread.joinable())
127127
m_thread.join();
128128
SASSERT(m_completed);
129-
st.copy(m_st);
130129
mdl = nullptr;
131130
if (m_result == l_true && m_sls_model) {
132131
ast_translation tr(m_sls, m);
@@ -140,6 +139,10 @@ namespace sls {
140139
dealloc(d);
141140
}
142141

142+
void smt_plugin::collect_statistics(::statistics& st) const {
143+
st.copy(m_st);
144+
}
145+
143146
void smt_plugin::get_shared_clauses(vector<sat::literal_vector>& _clauses) {
144147
_clauses.reset();
145148
for (auto const& clause : clauses()) {
@@ -257,7 +260,7 @@ namespace sls {
257260
void smt_plugin::sls_phase_to_smt() {
258261
if (!m_has_new_sls_phase)
259262
return;
260-
IF_VERBOSE(2, verbose_stream() << "SLS -> SMT phase\n");
263+
IF_VERBOSE(2, verbose_stream() << "SLS -> SMT phase " << m_min_unsat_size << "\n");
261264
for (auto v : m_shared_bool_vars)
262265
ctx.force_phase(sat::literal(v, !m_sls_phase[v]));
263266
m_has_new_sls_phase = false;
@@ -290,7 +293,7 @@ namespace sls {
290293
}
291294

292295
void smt_plugin::export_from_sls() {
293-
if (unsat().size() > m_min_unsat_size)
296+
if (unsat().size() >= m_min_unsat_size)
294297
return;
295298
m_min_unsat_size = unsat().size();
296299
export_phase_from_sls();

Diff for: ‎src/ast/sls/sls_smt_plugin.h

+2-1
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,8 @@ namespace sls {
106106

107107
// interface to calling solver:
108108
void check(expr_ref_vector const& fmls, vector <sat::literal_vector> const& clauses);
109-
void finalize(model_ref& md, ::statistics& st);
109+
void collect_statistics(::statistics& st) const;
110+
void finalize(model_ref& md);
110111
void get_shared_clauses(vector<sat::literal_vector>& clauses);
111112
void updt_params(params_ref& p) {}
112113
std::ostream& display(std::ostream& out) override;

Diff for: ‎src/sat/smt/sls_solver.cpp

+4-2
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,8 @@ namespace sls {
7272
if (!m_smt_plugin)
7373
return;
7474

75-
m_smt_plugin->finalize(m_model, m_st);
75+
m_smt_plugin->collect_statistics(m_st);
76+
m_smt_plugin->finalize(m_model);
7677
m_model = nullptr;
7778
m_smt_plugin = nullptr;
7879
}
@@ -89,7 +90,8 @@ namespace sls {
8990
return false;
9091
if (!m_smt_plugin->completed())
9192
return false;
92-
m_smt_plugin->finalize(m_model, m_st);
93+
m_smt_plugin->collect_statistics(m_st);
94+
m_smt_plugin->finalize(m_model);
9395
m_smt_plugin = nullptr;
9496
return true;
9597
}

Diff for: ‎src/smt/theory_sls.cpp

+12-4
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,8 @@ namespace smt {
6262
}
6363

6464
bool theory_sls::get_smt_value(expr* v, expr_ref& value) {
65+
if (!ctx.e_internalized(v))
66+
return false;
6567
auto* n = ctx.get_enode(v);
6668
return n && ctx.get_value(n, value);
6769
}
@@ -78,7 +80,8 @@ namespace smt {
7880
if (!m_smt_plugin)
7981
return;
8082

81-
m_smt_plugin->finalize(m_model, m_st);
83+
m_smt_plugin->collect_statistics(m_st);
84+
m_smt_plugin->finalize(m_model);
8285
m_model = nullptr;
8386
m_smt_plugin = nullptr;
8487
}
@@ -98,7 +101,8 @@ namespace smt {
98101
else if (!m_parallel_mode)
99102
propagate_local_search();
100103
else if (m_smt_plugin->completed()) {
101-
m_smt_plugin->finalize(m_model, m_st);
104+
m_smt_plugin->collect_statistics(m_st);
105+
m_smt_plugin->finalize(m_model);
102106
m_smt_plugin = nullptr;
103107
}
104108
}
@@ -184,7 +188,10 @@ namespace smt {
184188
}
185189

186190
void theory_sls::collect_statistics(::statistics& st) const {
187-
st.copy(m_st);
191+
if (m_smt_plugin)
192+
m_smt_plugin->collect_statistics(st);
193+
else
194+
st.copy(m_st);
188195
}
189196

190197
void theory_sls::restart_eh() {
@@ -205,7 +212,8 @@ namespace smt {
205212
void theory_sls::bounded_run(unsigned num_steps) {
206213
m_smt_plugin->bounded_run(num_steps);
207214
if (m_smt_plugin->result() == l_true) {
208-
m_smt_plugin->finalize(m_model, m_st);
215+
m_smt_plugin->collect_statistics(m_st);
216+
m_smt_plugin->finalize(m_model);
209217
m_smt_plugin = nullptr;
210218
}
211219
}

0 commit comments

Comments
 (0)
Please sign in to comment.