updates related to issue #5140 #5463
Conversation
src/ast/seq_decl_plugin.cpp
Outdated
| @@ -1068,6 +1069,10 @@ std::ostream& seq_util::rex::pp::compact_helper_seq(std::ostream& out, expr* s) | |||
| for (expr* e : es) | |||
| compact_helper_seq(out, e); | |||
| } | |||
| else if (re.u.str.is_string(s, z)) { | |||
| for (int i=0; i < z.length(); i++) | |||
src/ast/rewriter/seq_rewriter.cpp
Outdated
| */ | ||
| void seq_rewriter::replace_all_subvectors(expr_ref_vector const& a, expr_ref_vector const& b, expr* c, expr_ref_vector& result) { | ||
| int i = 0; | ||
| int k = b.size(); |
There was a problem hiding this comment.
use unsigned for i, k, j, b.size() is unsigned.
src/ast/rewriter/seq_rewriter.cpp
Outdated
| expr_ref_vector a_vals(m()); | ||
| expr_ref_vector b_vals(m()); | ||
| if (try_get_unit_values(a, a_vals) && try_get_unit_values(b, b_vals)) | ||
| { |
There was a problem hiding this comment.
{ after if is not on separate line (contrast to typical C# conventions).
There was a problem hiding this comment.
fixed this and the ones above in the following commit
| expr_ref seq_rewriter::mk_seq_first(expr* t) { | ||
| expr_ref result(m()); | ||
| expr* s, * j, * k; | ||
| if (str().is_extract(t, s, j, k)) |
There was a problem hiding this comment.
Is this sound?
if j < 0, then extract evaluates to an empty string, then the result should be the same as nth("",0). But you pass nth(s, j) which is under-specified. The rewrite would then restrict interpretations for nth(s, j) for j negative to nth("",0).
A further potential issue is the use of nth_i, which is the interpreted version of nth. It gets introduced as a rewrite nth(s, k) = if 0 <= k < len(s) then nth_i(s, k) else nth_u(s, k).
There was a problem hiding this comment.
the constraint of the use of mk_seq_first (in the derivation) is that the context implies is that |t|>0 which should imply that 0 <= j < |t| and also that j + k <= |t|.
This is because mk_seq_first(t) always occurs in conjunction with not(t = ()).
This is why I dropped the additional checks I had originally.
src/ast/rewriter/seq_rewriter.cpp
Outdated
| expr_ref seq_rewriter::mk_seq_rest(expr* t) { | ||
| expr_ref result(m()); | ||
| expr* s, * j, * k; | ||
| expr* one = m_autil.mk_int(1); |
There was a problem hiding this comment.
Pin the reference for uniformity:
expr_ref one(m_autil.mk_int(1), m());
|
In the last commit, I added also a missing case for get_re_head_tail_reversed but disabled it for now because it should not affect correctness but hides a bug I'm chasing. |
|
the last commit fixes 2 bugs
Also enables a missing case in get_re_head_tail_reversed that trteats e.g. (.A)B |
Fixed some bugs in issue #5140 (work in progress, not all are fixed yet).
Added functionality for dealing with derivatives over nonground sequences s without introducing the mkderivative OP in the ast.
Essentially D(e,s) = ite(s!=()& first(s)=e, rest(s), [])
This avoids stuck-situations -- that I believe lead to unsound unsat results in some cases.
Also, if s in uninterpreted, then
D(e,reverse(s)) = ite(s!=()& last(s)=e, reverse(butlast(s)), [])
Currently:
butlast(s) = substr(s,0,|s|-1)
and the pattern butlast(butlast(s)) is simplified to substr(s,0,|s|-2)
Similarly:
rest(s) = substr(s,1,|s|-1)
rest(rest(s)) = ..TBD.. = substr(s,2,|s|-2)
first(rest(s)) = nth(2,s)
etc..
Fixed also some rex:pp issues (still some TBD).