Skip to content

Commit b4e768c

Browse files
NikolajBjornerNikolajBjorner
committed
adding plugin for local search strings
1 parent 3672575 commit b4e768c

File tree

4 files changed

+389
-1
lines changed

4 files changed

+389
-1
lines changed

‎src/ast/sls/CMakeLists.txt

+1
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ z3_add_component(ast_sls
1515
sls_context.cpp
1616
sls_datatype_plugin.cpp
1717
sls_euf_plugin.cpp
18+
sls_seq_plugin.cpp
1819
sls_smt_plugin.cpp
1920
sls_smt_solver.cpp
2021
COMPONENT_DEPENDENCIES

‎src/ast/sls/sls_seq_plugin.cpp

+306
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,306 @@
1+
/*++
2+
Copyright (c) 2024 Microsoft Corporation
3+
4+
Module Name:
5+
6+
sls_seq_plugin.cpp
7+
8+
Abstract:
9+
10+
Sequence/String SLS
11+
12+
Author:
13+
14+
Nikolaj Bjorner (nbjorner) 2024-11-22
15+
16+
--*/
17+
18+
#include "ast/sls/sls_seq_plugin.h"
19+
#include "ast/sls/sls_context.h"
20+
21+
22+
namespace sls {
23+
24+
seq_plugin::seq_plugin(context& c):
25+
plugin(c),
26+
seq(c.get_manager())
27+
{}
28+
29+
void seq_plugin::propagate_literal(sat::literal lit) {
30+
}
31+
32+
expr_ref seq_plugin::get_value(expr* e) {
33+
return expr_ref(m);
34+
}
35+
36+
bool seq_plugin::propagate() {
37+
return false;
38+
}
39+
40+
bool seq_plugin::is_sat() {
41+
return true;
42+
}
43+
44+
void seq_plugin::register_term(expr* e) {
45+
}
46+
47+
std::ostream& seq_plugin::display(std::ostream& out) const {
48+
return out;
49+
}
50+
51+
bool seq_plugin::set_value(expr* e, expr* v) {
52+
return false;
53+
}
54+
55+
zstring& seq_plugin::strval0(expr* e) {
56+
SASSERT(seq.is_string(e->get_sort()));
57+
unsigned id = e->get_id();
58+
m_values.reserve(id + 1);
59+
if (!m_values[id])
60+
m_values.set(id, alloc(eval, m));
61+
return m_values[id]->val0.svalue;
62+
}
63+
64+
bool seq_plugin::bval1(expr* e) {
65+
SASSERT(is_app(e));
66+
if (to_app(e)->get_family_id() == seq.get_family_id())
67+
return bval1_seq(to_app(e));
68+
69+
NOT_IMPLEMENTED_YET();
70+
return false;
71+
}
72+
73+
bool seq_plugin::bval1_seq(app* e) {
74+
expr* a, *b;
75+
switch (e->get_decl_kind()) {
76+
case OP_SEQ_CONTAINS: {
77+
VERIFY(seq.str.is_contains(e, a, b));
78+
if (seq.is_string(a->get_sort()))
79+
return strval0(a).contains(strval0(b));
80+
else {
81+
NOT_IMPLEMENTED_YET();
82+
}
83+
break;
84+
}
85+
case OP_SEQ_PREFIX:
86+
case OP_SEQ_SUFFIX:
87+
case OP_SEQ_NTH:
88+
case OP_SEQ_NTH_I:
89+
case OP_SEQ_NTH_U:
90+
case OP_SEQ_IN_RE:
91+
case OP_SEQ_FOLDL:
92+
case OP_SEQ_FOLDLI:
93+
case OP_STRING_LT:
94+
case OP_STRING_LE:
95+
case OP_STRING_IS_DIGIT:
96+
NOT_IMPLEMENTED_YET();
97+
break;
98+
default:
99+
break;
100+
}
101+
return false;
102+
}
103+
104+
zstring const& seq_plugin::strval1(expr* e) {
105+
SASSERT(is_app(e));
106+
SASSERT(seq.is_string(e->get_sort()));
107+
if (to_app(e)->get_family_id() == seq.get_family_id()) {
108+
switch (to_app(e)->get_decl_kind()) {
109+
case OP_SEQ_UNIT:
110+
case OP_SEQ_EMPTY:
111+
case OP_SEQ_CONCAT:
112+
case OP_SEQ_EXTRACT:
113+
case OP_SEQ_REPLACE:
114+
case OP_SEQ_AT:
115+
case OP_SEQ_NTH:
116+
case OP_SEQ_NTH_I:
117+
case OP_SEQ_NTH_U:
118+
case OP_SEQ_LENGTH:
119+
case OP_SEQ_INDEX:
120+
case OP_SEQ_LAST_INDEX:
121+
case OP_SEQ_TO_RE:
122+
case OP_SEQ_IN_RE:
123+
case OP_SEQ_REPLACE_RE_ALL:
124+
case OP_SEQ_REPLACE_RE:
125+
case OP_SEQ_REPLACE_ALL:
126+
case OP_SEQ_MAP:
127+
case OP_SEQ_MAPI:
128+
case OP_SEQ_FOLDL:
129+
case OP_SEQ_FOLDLI:
130+
case OP_RE_PLUS:
131+
case OP_RE_STAR:
132+
case OP_RE_OPTION:
133+
case OP_RE_RANGE:
134+
case OP_RE_CONCAT:
135+
case OP_RE_UNION:
136+
case OP_RE_DIFF:
137+
case OP_RE_INTERSECT:
138+
case OP_RE_LOOP:
139+
case OP_RE_POWER:
140+
case OP_RE_COMPLEMENT:
141+
case OP_RE_EMPTY_SET:
142+
case OP_RE_FULL_SEQ_SET:
143+
case OP_RE_FULL_CHAR_SET:
144+
case OP_RE_OF_PRED:
145+
case OP_RE_REVERSE:
146+
case OP_RE_DERIVATIVE:
147+
case OP_STRING_CONST:
148+
case OP_STRING_ITOS:
149+
case OP_STRING_STOI:
150+
case OP_STRING_UBVTOS:
151+
case OP_STRING_SBVTOS:
152+
case OP_STRING_LT:
153+
case OP_STRING_LE:
154+
case OP_STRING_IS_DIGIT:
155+
case OP_STRING_TO_CODE:
156+
case OP_STRING_FROM_CODE:
157+
NOT_IMPLEMENTED_YET();
158+
break;
159+
default:
160+
UNREACHABLE();
161+
break;
162+
}
163+
}
164+
auto const& v = strval0(e);
165+
m_values[e->get_id()]->val1.svalue = v;
166+
return m_values[e->get_id()]->val1.svalue;
167+
}
168+
169+
void seq_plugin::repair_up(app* e) {
170+
}
171+
172+
bool seq_plugin::repair_down(app* e) {
173+
switch (e->get_decl_kind()) {
174+
case OP_SEQ_UNIT:
175+
case OP_SEQ_EMPTY:
176+
case OP_SEQ_CONCAT:
177+
case OP_SEQ_PREFIX:
178+
case OP_SEQ_SUFFIX:
179+
case OP_SEQ_CONTAINS:
180+
return repair_contains(e);
181+
case OP_SEQ_EXTRACT:
182+
case OP_SEQ_REPLACE:
183+
case OP_SEQ_AT:
184+
case OP_SEQ_NTH:
185+
case OP_SEQ_NTH_I:
186+
case OP_SEQ_NTH_U:
187+
case OP_SEQ_LENGTH:
188+
case OP_SEQ_INDEX:
189+
case OP_SEQ_LAST_INDEX:
190+
case OP_SEQ_TO_RE:
191+
case OP_SEQ_IN_RE:
192+
case OP_SEQ_REPLACE_RE_ALL:
193+
case OP_SEQ_REPLACE_RE:
194+
case OP_SEQ_REPLACE_ALL:
195+
case OP_SEQ_MAP:
196+
case OP_SEQ_MAPI:
197+
case OP_SEQ_FOLDL:
198+
case OP_SEQ_FOLDLI:
199+
case OP_RE_PLUS:
200+
case OP_RE_STAR:
201+
case OP_RE_OPTION:
202+
case OP_RE_RANGE:
203+
case OP_RE_CONCAT:
204+
case OP_RE_UNION:
205+
case OP_RE_DIFF:
206+
case OP_RE_INTERSECT:
207+
case OP_RE_LOOP:
208+
case OP_RE_POWER:
209+
case OP_RE_COMPLEMENT:
210+
case OP_RE_EMPTY_SET:
211+
case OP_RE_FULL_SEQ_SET:
212+
case OP_RE_FULL_CHAR_SET:
213+
case OP_RE_OF_PRED:
214+
case OP_RE_REVERSE:
215+
case OP_RE_DERIVATIVE:
216+
case OP_STRING_CONST:
217+
case OP_STRING_ITOS:
218+
case OP_STRING_STOI:
219+
case OP_STRING_UBVTOS:
220+
case OP_STRING_SBVTOS:
221+
case OP_STRING_LT:
222+
case OP_STRING_LE:
223+
case OP_STRING_IS_DIGIT:
224+
case OP_STRING_TO_CODE:
225+
case OP_STRING_FROM_CODE:
226+
default:
227+
break;
228+
}
229+
return false;
230+
}
231+
232+
bool seq_plugin::repair_contains(expr* e) {
233+
expr* a, *b;
234+
VERIFY(seq.str.is_contains(e, a, b));
235+
zstring sa = strval0(a);
236+
zstring sb = strval0(b);
237+
unsigned lena = sa.length();
238+
unsigned lenb = sb.length();
239+
240+
m_str_updates.reset();
241+
if (ctx.is_true(e)) {
242+
// add b to a in front
243+
// add b to a in back
244+
// add part of b to a front/back
245+
// take random subsequence of a and set it to b
246+
// reduce size of b
247+
248+
m_str_updates.push_back({ a, sb + sa, 1 });
249+
m_str_updates.push_back({ a, sa + sb, 1 });
250+
if (lena > 1) {
251+
unsigned mid = ctx.rand(lena-2) + 1;
252+
zstring sa1 = sa.extract(0, mid);
253+
zstring sa2 = sa.extract(mid, lena - mid);
254+
m_str_updates.push_back({ a, sa1 + sb + sa2, 1});
255+
}
256+
if (lenb > 0) {
257+
m_str_updates.push_back({ b, sb.extract(0, lenb-1), 1});
258+
m_str_updates.push_back({ b, sb.extract(1, lenb-1), 1});
259+
}
260+
}
261+
else {
262+
// remove occurrences of b in a, if b is non-empty
263+
// append character to b
264+
// set b to be a + character
265+
//
266+
}
267+
return apply_str_update();
268+
}
269+
270+
bool seq_plugin::apply_str_update() {
271+
double sum_scores = 0;
272+
for (auto const& [e, val, score] : m_str_updates)
273+
sum_scores += score;
274+
275+
while (!m_str_updates.empty()) {
276+
unsigned i = m_str_updates.size();
277+
double lim = sum_scores * ((double)ctx.rand() / random_gen().max_value());
278+
do {
279+
lim -= m_str_updates[--i].m_score;
280+
}
281+
while (lim >= 0 && i > 0);
282+
283+
auto [e, value, score] = m_str_updates[i];
284+
285+
if (update(e, value))
286+
return true;
287+
288+
sum_scores -= score;
289+
m_str_updates[i] = m_str_updates.back();
290+
m_str_updates.pop_back();
291+
}
292+
293+
return false;
294+
}
295+
296+
bool seq_plugin::update(expr* e, zstring const& value) {
297+
strval0(e) = value;
298+
ctx.new_value_eh(e);
299+
return true;
300+
}
301+
302+
303+
void seq_plugin::repair_literal(sat::literal lit) {
304+
}
305+
306+
}

‎src/ast/sls/sls_seq_plugin.h

+81
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
/*++
2+
Copyright (c) 2024 Microsoft Corporation
3+
4+
Module Name:
5+
6+
sls_seq_plugin.h
7+
8+
Abstract:
9+
10+
Sequence/String SLS
11+
12+
Author:
13+
14+
Nikolaj Bjorner (nbjorner) 2024-11-22
15+
16+
--*/
17+
#pragma once
18+
19+
#include "ast/sls/sls_context.h"
20+
#include "ast/seq_decl_plugin.h"
21+
22+
23+
namespace sls {
24+
25+
class seq_plugin : public plugin {
26+
struct value {
27+
value(ast_manager& m): evalue(m) {}
28+
zstring svalue;
29+
expr_ref evalue;
30+
};
31+
32+
struct eval {
33+
eval(ast_manager& m):
34+
val0(m), val1(m) {}
35+
value val0;
36+
value val1;
37+
};
38+
39+
seq_util seq;
40+
scoped_ptr_vector<eval> m_values;
41+
42+
struct str_update {
43+
expr* e;
44+
zstring value;
45+
unsigned m_score;
46+
};
47+
vector<str_update> m_str_updates;
48+
bool apply_str_update();
49+
bool update(expr* e, zstring const& value);
50+
51+
bool bval1(expr* e);
52+
bool bval1_seq(app* e);
53+
zstring& strval0(expr* e);
54+
zstring const& strval1(expr* e);
55+
56+
bool repair_contains(expr* e);
57+
58+
public:
59+
seq_plugin(context& c);
60+
~seq_plugin() override {}
61+
expr_ref get_value(expr* e) override;
62+
void initialize() override {}
63+
void start_propagation() override {}
64+
void propagate_literal(sat::literal lit) override;
65+
bool propagate() override;
66+
bool is_sat() override;
67+
void register_term(expr* e) override;
68+
std::ostream& display(std::ostream& out) const override;
69+
bool set_value(expr* e, expr* v) override;
70+
bool include_func_interp(func_decl* f) const override { return true; }
71+
72+
void repair_up(app* e) override;
73+
bool repair_down(app* e) override;
74+
void repair_literal(sat::literal lit) override;
75+
76+
void collect_statistics(statistics& st) const override {}
77+
void reset_statistics() override {}
78+
79+
};
80+
81+
}

0 commit comments

Comments
 (0)