mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

updates to equality solving search

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-12-02 13:41:18 -08:00
parent e6feb8423a
commit aec867586a
2 changed files with 12 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2191,7 +2191,7 @@ namespace sls {
auto const& vi = m_vars[v];
if (vi.m_def_idx == UINT_MAX)
return true;
IF_VERBOSE(2, verbose_stream() << " repair def " << mk_bounded_pp(vi.m_expr, m) << "\n");
IF_VERBOSE(4, verbose_stream() << vi.m_op << " repair def " << mk_bounded_pp(vi.m_expr, m) << "\n");
TRACE("sls", tout << "repair def " << mk_bounded_pp(vi.m_expr, m) << "\n");
switch (vi.m_op) {
case arith_op_kind::LAST_ARITH_OP:

11
src/ast/sls/sls_seq_plugin.cpp
View file

@ -605,11 +605,15 @@ namespace sls {
zstring ch(m_chars[ctx.rand(m_chars.size())]);
m_str_updates.push_back({ x, strval1(y) + ch, 1 });
m_str_updates.push_back({ x, ch + strval1(y), 1 });
m_str_updates.push_back({ x, ch, 1 });
m_str_updates.push_back({ x, zstring(), 1 });
}
if (!is_value(y) && !m_chars.empty()) {
zstring ch(m_chars[ctx.rand(m_chars.size())]);
m_str_updates.push_back({ y, strval1(x) + ch, 1 });
m_str_updates.push_back({ y, ch + strval1(x), 1 });
m_str_updates.push_back({ x, ch, 1 });
m_str_updates.push_back({ x, zstring(), 1});
}
}
return apply_update();
@ -826,6 +830,7 @@ namespace sls {
expr* x, * y;
VERIFY(seq.str.is_at(e, x, y));
zstring se = strval0(e);
verbose_stream() << "repair down at " << mk_pp(e, m) << " " << se << "\n";
if (se.length() > 1)
return false;
zstring sx = strval0(x);
@ -886,6 +891,12 @@ namespace sls {
if (offset_r.is_unsigned())
offset_u = offset_r.get_unsigned();
// set to not a member:
if (value == -1) {
m_str_updates.push_back({ y, zstring(m_chars[ctx.rand(m_chars.size())]), 1 });
if (lenx > 0)
m_str_updates.push_back({ x, zstring(), 1 });
}
// change x:
// insert y into x at offset
if (offset_r.is_unsigned() && 0 <= value && offset_u + value <= lenx && leny > 0) {