Skip to content

Commit fe1622b

Browse files
NikolajBjornerNikolajBjorner
committed
sls fixes for ABV. Axiomatization required as saturation can produce conflicts by congruence closure
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
1 parent 2050fc3 commit fe1622b

File tree

4 files changed

+109
-39
lines changed

4 files changed

+109
-39
lines changed

‎src/ast/sls/sls_array_plugin.cpp

Lines changed: 63 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ namespace sls {
2424

2525
array_plugin::array_plugin(context& ctx):
2626
plugin(ctx),
27+
euf(ctx.euf()),
2728
a(m)
2829
{
2930
m_fid = a.get_family_id();
@@ -36,36 +37,67 @@ namespace sls {
3637
m_kv = nullptr;
3738
init_egraph(*m_g);
3839
saturate(*m_g);
39-
#if 0
4040
if (m_g->inconsistent()) {
4141
resolve_conflict();
4242
return false;
4343
}
44-
#endif
4544
return !m_g->inconsistent();
4645
}
4746

4847

4948
void array_plugin::resolve_conflict() {
49+
++m_stats.m_num_conflicts;
5050
auto& g = *m_g;
5151
SASSERT(g.inconsistent());
52-
unsigned n = 0;
53-
sat::literal_vector lits;
5452
ptr_vector<size_t> explain;
5553
g.begin_explain();
5654
g.explain<size_t>(explain, nullptr);
5755
g.end_explain();
5856

59-
verbose_stream() << "conflict\n";
57+
IF_VERBOSE(3, verbose_stream() << "array conflict\n");
58+
bool has_missing_axiom = false;
6059
for (auto p : explain) {
61-
if (is_literal(p)) {
62-
sat::literal l = to_literal(p);
63-
verbose_stream() << l << " " << mk_bounded_pp(ctx.atom(l.var()), m) << " " << ctx.is_unit(l) << "\n";
60+
if (is_index(p)) {
61+
has_missing_axiom = true;
62+
unsigned idx = to_index(p);
63+
auto [t, sto, sel] = m_delayed_axioms[idx];
64+
switch (t) {
65+
case store_axiom1:
66+
add_store_axiom1(sto->get_app());
67+
break;
68+
case store_axiom2_down:
69+
case store_axiom2_up:
70+
add_store_axiom2(sto->get_app(), sel->get_app());
71+
break;
72+
case map_axiom:
73+
case const_axiom:
74+
add_eq_axiom(sto, sel);
75+
break;
76+
default:
77+
UNREACHABLE();
78+
break;
79+
}
6480
}
65-
else {
66-
verbose_stream() << mk_bounded_pp(to_expr(p), m) << " == " << mk_bounded_pp(ctx.get_value(to_expr(p)), m) << "\n";
81+
}
82+
if (has_missing_axiom)
83+
return;
84+
85+
sat::literal_vector lits;
86+
for (auto p : explain) {
87+
if (is_enode(p)) {
88+
auto n = to_enode(p);
89+
auto v = ctx.get_value(n->get_expr());
90+
lits.push_back(~ctx.mk_literal(m.mk_eq(n->get_expr(), v)));
91+
if (a.is_store(n->get_expr()))
92+
add_store_axiom1(n->get_app());
6793
}
94+
else if (is_literal(p)) {
95+
sat::literal l = to_literal(p);
96+
lits.push_back(~l);
97+
}
6898
}
99+
IF_VERBOSE(3, verbose_stream() << "add conflict clause\n");
100+
ctx.add_clause(lits);
69101
}
70102

71103
// b ~ a[i -> v]
@@ -141,13 +173,12 @@ namespace sls {
141173
if (nmap->get_root() == nsel->get_root())
142174
return;
143175
if (!are_distinct(nsel, nmap)) {
144-
g.merge(nmap, nsel, nullptr);
176+
g.merge(nmap, nsel, to_ptr(map_axiom_index(nmap, nsel)));
145177
g.propagate();
146178
if (!g.inconsistent())
147179
return;
148180
}
149-
expr_ref eq(m.mk_eq(nmap->get_expr(), nsel->get_expr()), m);
150-
ctx.add_theory_axiom(eq);
181+
add_eq_axiom(nmap, nsel);
151182
}
152183

153184
euf::enode* array_plugin::mk_select(euf::egraph& g, euf::enode* b, euf::enode* sel) {
@@ -175,10 +206,10 @@ namespace sls {
175206
auto nsel = mk_select(g, n, n);
176207
VERIFY(!g.inconsistent());
177208
if (!are_distinct(nsel, val)) {
178-
g.merge(nsel, val, nullptr);
209+
g.merge(nsel, val, to_ptr(store_axiom1_index(n)));
179210
g.propagate();
180211
if (!g.inconsistent())
181-
return;
212+
return;
182213
}
183214
add_store_axiom1(n->get_app());
184215
}
@@ -195,7 +226,7 @@ namespace sls {
195226
return;
196227
auto nsel = mk_select(g, sto->get_arg(0), sel);
197228
if (!are_distinct(nsel, sel)) {
198-
g.merge(nsel, sel, nullptr);
229+
g.merge(nsel, sel, to_ptr(store_axiom2_down_index(sto, sel)));
199230
g.propagate();
200231
if (!g.inconsistent())
201232
return;
@@ -215,7 +246,7 @@ namespace sls {
215246
return;
216247
auto nsel = mk_select(g, sto, sel);
217248
if (!are_distinct(nsel, sel)) {
218-
g.merge(nsel, sel, nullptr);
249+
g.merge(nsel, sel, to_ptr(store_axiom2_up_index(sto, sel)));
219250
g.propagate();
220251
if (!g.inconsistent())
221252
return;
@@ -234,13 +265,13 @@ namespace sls {
234265
auto val = cn->get_arg(0);
235266
auto nsel = mk_select(g, cn, sel);
236267
if (!are_distinct(nsel, sel)) {
237-
g.merge(nsel, sel, nullptr);
268+
g.merge(nsel, sel, to_ptr(const_axiom_index(val, nsel)));
238269
g.propagate();
239270
if (!g.inconsistent())
240271
return;
241272
}
242-
expr_ref eq(m.mk_eq(val->get_expr(), nsel->get_expr()), m);
243-
ctx.add_theory_axiom(eq);
273+
++m_stats.m_num_axioms;
274+
add_eq_axiom(val, nsel);
244275
}
245276

246277
bool array_plugin::are_distinct(euf::enode* a, euf::enode* b) {
@@ -270,6 +301,7 @@ namespace sls {
270301
expr_ref sel(a.mk_select(args), m);
271302
expr_ref eq(m.mk_eq(sel, to_app(sto)->get_arg(sto->get_num_args() - 1)), m);
272303
IF_VERBOSE(3, verbose_stream() << "add store axiom 1 " << mk_bounded_pp(sto, m) << "\n");
304+
++m_stats.m_num_axioms;
273305
ctx.add_theory_axiom(eq);
274306
}
275307

@@ -291,6 +323,7 @@ namespace sls {
291323
for (unsigned i = 1; i < sel->get_num_args() - 1; ++i)
292324
ors.push_back(m.mk_eq(sel->get_arg(i), sto->get_arg(i)));
293325
IF_VERBOSE(3, verbose_stream() << "add store axiom 2 " << mk_bounded_pp(sto, m) << " " << mk_bounded_pp(sel, m) << "\n");
326+
++m_stats.m_num_axioms;
294327
ctx.add_theory_axiom(m.mk_or(ors));
295328
}
296329

@@ -307,21 +340,24 @@ namespace sls {
307340
n1 = n1 ? n1 : g.mk(t, 0, args.size(), args.data());
308341
if (a.is_array(t))
309342
continue;
343+
if (m.is_bool(t))
344+
continue;
310345
auto v = ctx.get_value(t);
311346
IF_VERBOSE(3, verbose_stream() << "init " << mk_bounded_pp(t, m) << " := " << mk_bounded_pp(v, m) << " " << g.inconsistent() << "\n");
312347
n2 = g.find(v);
313348
n2 = n2 ? n2: g.mk(v, 0, 0, nullptr);
314-
g.merge(n1, n2, to_ptr(t));
349+
g.merge(n1, n2, to_ptr(n1));
315350
}
316351
for (auto lit : ctx.root_literals()) {
317352
if (!ctx.is_true(lit) || lit.sign())
318353
continue;
319354
auto e = ctx.atom(lit.var());
320355
expr* x = nullptr, * y = nullptr;
321356
if (e && m.is_eq(e, x, y))
322-
g.merge(g.find(x), g.find(y), to_ptr(lit));
357+
g.merge(g.find(x), g.find(y), nullptr);
323358

324359
}
360+
g.propagate();
325361

326362
IF_VERBOSE(3, display(verbose_stream()));
327363

@@ -388,4 +424,9 @@ namespace sls {
388424
}
389425
return out;
390426
}
427+
428+
void array_plugin::collect_statistics(statistics& st) const {
429+
st.update("sls-array-conflicts", m_stats.m_num_conflicts);
430+
st.update("sls-array-axioms", m_stats.m_num_axioms);
431+
}
391432
}

‎src/ast/sls/sls_array_plugin.h

Lines changed: 42 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -22,22 +22,24 @@ Module Name:
2222

2323
namespace sls {
2424

25+
class euf_plugin;
26+
2527
class array_plugin : public plugin {
2628
struct select_args {
2729
euf::enode* sel = nullptr;
2830
select_args(euf::enode* s) : sel(s) {}
2931
select_args() {}
3032
};
3133
struct select_args_hash {
32-
unsigned operator()(select_args const& a) const {
34+
unsigned operator()(select_args const& a) const {
3335
unsigned h = 0;
3436
for (unsigned i = 1; i < a.sel->num_args(); ++i)
35-
h ^= a.sel->get_arg(i)->get_root()->hash();
37+
h ^= a.sel->get_arg(i)->get_root()->hash();
3638
return h;
3739
};
3840
};
3941
struct select_args_eq {
40-
bool operator()(select_args const& a, select_args const& b) const {
42+
bool operator()(select_args const& a, select_args const& b) const {
4143
SASSERT(a.sel->num_args() == b.sel->num_args());
4244
for (unsigned i = 1; i < a.sel->num_args(); ++i)
4345
if (a.sel->get_arg(i)->get_root() != b.sel->get_arg(i)->get_root())
@@ -47,12 +49,37 @@ namespace sls {
4749
};
4850
typedef map<select_args, euf::enode*, select_args_hash, select_args_eq> select2value;
4951
typedef obj_map<euf::enode, select2value> kv;
52+
struct stats {
53+
unsigned m_num_conflicts = 0;
54+
unsigned m_num_axioms = 0;
55+
void reset() { memset(this, 0, sizeof(*this)); }
56+
};
5057

58+
euf_plugin& euf;
5159
array_util a;
5260
scoped_ptr<euf::egraph> m_g;
53-
scoped_ptr<kv> m_kv;
54-
bool m_add_conflicts = true;
55-
bool m_has_arrays = false;
61+
scoped_ptr<kv> m_kv;
62+
bool m_add_conflicts = true;
63+
bool m_has_arrays = false;
64+
stats m_stats;
65+
66+
enum axiom_t { store_axiom1, store_axiom2_down, store_axiom2_up, map_axiom, const_axiom };
67+
struct axiom_instance {
68+
axiom_t t;
69+
euf::enode* sto; euf::enode* sel;
70+
};
71+
svector<axiom_instance> m_delayed_axioms;
72+
unsigned store_axiom1_index(euf::enode* n) { m_delayed_axioms.push_back({ store_axiom1, n, nullptr }); return m_delayed_axioms.size() - 1; }
73+
unsigned store_axiom2_down_index(euf::enode* sto, euf::enode* sel) { m_delayed_axioms.push_back({ store_axiom2_down, sto, sel }); return m_delayed_axioms.size() - 1; }
74+
unsigned store_axiom2_up_index(euf::enode* sto, euf::enode* sel) { m_delayed_axioms.push_back({ store_axiom2_up, sto, sel }); return m_delayed_axioms.size() - 1; }
75+
unsigned map_axiom_index(euf::enode* sto, euf::enode* sel) { m_delayed_axioms.push_back({ map_axiom, sto, sel }); return m_delayed_axioms.size() - 1; }
76+
unsigned const_axiom_index(euf::enode* val, euf::enode* sel) { m_delayed_axioms.push_back({ const_axiom, val, sel }); return m_delayed_axioms.size() - 1; }
77+
78+
void add_eq_axiom(euf::enode* x, euf::enode* y) {
79+
++m_stats.m_num_axioms;
80+
expr_ref eq(m.mk_eq(x->get_expr(), y->get_expr()), m);
81+
ctx.add_theory_axiom(eq);
82+
}
5683

5784
void init_egraph(euf::egraph& g);
5885
void init_kv(euf::egraph& g, kv& kv);
@@ -73,10 +100,14 @@ namespace sls {
73100

74101
void resolve_conflict();
75102
size_t* to_ptr(sat::literal l) { return reinterpret_cast<size_t*>((size_t)(l.index() << 4)); };
76-
size_t* to_ptr(expr* t) { return reinterpret_cast<size_t*>((reinterpret_cast<size_t>(t) << 4) + 1); }
77-
bool is_literal(size_t* p) { return (reinterpret_cast<size_t>(p) & 1) == 0; }
103+
size_t* to_ptr(euf::enode* t) { return reinterpret_cast<size_t*>((reinterpret_cast<size_t>(t) << 4) + 1); }
104+
size_t* to_ptr(unsigned n) { return reinterpret_cast<size_t*>((size_t)(n << 4) + 3); }
105+
bool is_literal(size_t* p) { return (reinterpret_cast<size_t>(p) & 3) == 0; }
106+
bool is_index(size_t* p) { return (reinterpret_cast<size_t>(p) & 3) == 3; }
107+
bool is_enode(size_t* p) { return (reinterpret_cast<size_t>(p) & 3) == 1; }
78108
sat::literal to_literal(size_t* p) { return sat::to_literal(static_cast<unsigned>(reinterpret_cast<size_t>(p) >> 4)); };
79-
expr* to_expr(size_t* p) { return reinterpret_cast<expr*>(reinterpret_cast<size_t>(p) >> 4); }
109+
euf::enode* to_enode(size_t* p) { return reinterpret_cast<euf::enode*>(reinterpret_cast<size_t>(p) >> 4); }
110+
unsigned to_index(size_t* p) { return static_cast<unsigned>(reinterpret_cast<size_t>(p) >> 4); }
80111

81112
public:
82113
array_plugin(context& ctx);
@@ -95,8 +126,8 @@ namespace sls {
95126
void on_restart() override {}
96127
std::ostream& display(std::ostream& out) const override;
97128
bool set_value(expr* e, expr* v) override { return false; }
98-
void collect_statistics(statistics& st) const override {}
99-
void reset_statistics() override {}
129+
void collect_statistics(statistics& st) const override;
130+
void reset_statistics() override { m_stats.reset(); }
100131
};
101132

102133
}

‎src/ast/sls/sls_context.cpp

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -315,11 +315,9 @@ namespace sls {
315315
auto p = m_plugins.get(fid, nullptr);
316316
if (p)
317317
return p->get_value(e);
318-
if (m.is_bool(e)) {
319-
sat::bool_var v = m_atom2bool_var.get(e->get_id(), sat::null_bool_var);
320-
if (v != sat::null_bool_var)
321-
return expr_ref(m.mk_bool_val(is_true(v)), m);
322-
}
318+
if (m.is_bool(e))
319+
return expr_ref(m.mk_bool_val(is_true(e)), m);
320+
323321
verbose_stream() << fid << " " << m.get_family_name(fid) << " " << mk_pp(e, m) << "\n";
324322
UNREACHABLE();
325323
return expr_ref(e, m);

‎src/ast/sls/sls_euf_plugin.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -90,7 +90,7 @@ namespace sls {
9090
g.explain<size_t>(explain, nullptr);
9191
g.end_explain();
9292
double reward = -1;
93-
TRACE("enf",
93+
TRACE("euf",
9494
for (auto p : explain) {
9595
sat::literal l = to_literal(p);
9696
tout << l << " " << mk_pp(ctx.atom(l.var()), m) << " " << ctx.is_unit(l) << "\n";

0 commit comments

Comments
 (0)