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

model generation with strings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-13 10:39:38 +01:00
parent 9909c056f0
commit 57e1d4dc1f
2 changed files with 13 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/ast/rewriter/seq_rewriter.cpp
View file

@ -938,7 +938,6 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change) { bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change) {
expr* a, *b; expr* a, *b;
zstring s; zstring s;
bool lchange = false; bool lchange = false;
SASSERT(lhs.empty()); SASSERT(lhs.empty());
// solve from back // solve from back
@ -1327,6 +1326,13 @@ bool seq_rewriter::is_subsequence(unsigned szl, expr* const* l, unsigned szr, ex
found = !rpos.contains(j) && l[i] == r[j]; found = !rpos.contains(j) && l[i] == r[j];
} }
if (!found) { if (!found) {
#if 0
std::cout << mk_pp(l[i], m()) << " not found in ";
for (unsigned j = 0; j < szr; ++j) {
std::cout << mk_pp(r[j], m()) << " ";
}
std::cout << "\n";
#endif
return false; return false;
} }
SASSERT(0 < j && j <= szr); SASSERT(0 < j && j <= szr);

8
src/smt/theory_seq.cpp
View file

@ -1325,7 +1325,10 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
if (concats.size() > 1) { if (concats.size() > 1) {
for (unsigned i = 0; i < concats.size(); ++i) { for (unsigned i = 0; i < concats.size(); ++i) {
sv->add_dependency(ctx.get_enode(concats[i])); expr* e = concats[i];
if (!m_util.str.is_string(e)) {
sv->add_dependency(ctx.get_enode(e));
}
} }
} }
else if (m_util.str.is_unit(e, e1)) { else if (m_util.str.is_unit(e, e1)) {
@ -1361,7 +1364,8 @@ app* theory_seq::mk_value(app* e) {
unsigned sz; unsigned sz;
if (bv.is_numeral(result, val, sz) && sz == zstring().num_bits()) { if (bv.is_numeral(result, val, sz) && sz == zstring().num_bits()) {
unsigned v = val.get_unsigned(); unsigned v = val.get_unsigned();
if ((v < 7) || (14 <= v && v < 32) || v == 127) { if (false && ((v < 7) || (14 <= v && v < 32) || v == 127)) {
// disabled: use escape characters.
result = m_util.str.mk_unit(result); result = m_util.str.mk_unit(result);
} }
else { else {