mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

strengthen support for int.to.str and length reasoning. Issue #589

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-05-28 12:36:50 -07:00
parent c3f498a640
commit cddf8091b5
1 changed files with 6 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/theory_seq.cpp
View file

@ -827,7 +827,7 @@ bool theory_seq::propagate_length_coherence(expr* e) {
expr_ref head(m), tail(m); expr_ref head(m), tail(m);
rational lo, hi; rational lo, hi;
if (!is_var(e) || !m_rep.is_root(e)) { if (!is_var(e) || !m_rep.is_root(e) || m_util.str.is_itos(e)) {
return false; return false;
} }
if (!lower_bound(e, lo) || !lo.is_pos() || lo >= rational(2048)) { if (!lower_bound(e, lo) || !lo.is_pos() || lo >= rational(2048)) {
@ -872,7 +872,7 @@ bool theory_seq::propagate_length_coherence(expr* e) {
bool theory_seq::check_length_coherence(expr* e) { bool theory_seq::check_length_coherence(expr* e) {
if (is_var(e) && m_rep.is_root(e)) { if (is_var(e) && m_rep.is_root(e) && !m_util.str.is_itos(e)) {
if (!check_length_coherence0(e)) { if (!check_length_coherence0(e)) {
expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m); expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
expr_ref head(m), tail(m); expr_ref head(m), tail(m);
@ -2438,9 +2438,10 @@ public:
} }
else { else {
zstring zs; zstring zs;
VERIFY(th.m_util.str.is_string(m_strings[k++], zs)); if (th.m_util.str.is_string(m_strings[k++], zs)) {
for (unsigned l = 0; l < zs.length(); ++l) { for (unsigned l = 0; l < zs.length(); ++l) {
sbuffer.push_back(zs[l]); sbuffer.push_back(zs[l]);
}
} }
} }
} }