This PR moves the axioms (assuming N is a numeral)
from (str.len s) = N create (str.len s) = N => s \in \Sigma^N
from (str.len s) <= N create (str.len s) <= N => s \in \Sigma^(0..N)
from (str.to_int s) = N create (str.to_int s) = N => s \in 0*N
from theory_str_noodler into the rewriter. I already tried doing this in #120, but I forgot that I tried this.
Does not work correctly for full_str_int + there is performance degradation (see z3-noodler-43f4868-d95fe13).
This PR moves the axioms (assuming
Nis a numeral)(str.len s) = Ncreate(str.len s) = N => s \in \Sigma^N(str.len s) <= Ncreate(str.len s) <= N => s \in \Sigma^(0..N)(str.to_int s) = Ncreate(str.to_int s) = N => s \in 0*Nfromtheory_str_noodlerinto the rewriter. I already tried doing this in #120, but I forgot that I tried this.Does not work correctly for
full_str_int+ there is performance degradation (seez3-noodler-43f4868-d95fe13).