mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
e1d2b88a82
commit
780346c7ca
|
@ -1130,7 +1130,7 @@ expr* seq_decl_plugin::get_some_value(sort* s) {
|
|||
}
|
||||
|
||||
app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range) {
|
||||
SASSERT(range);
|
||||
SASSERT(range);
|
||||
parameter param(name);
|
||||
func_decl* f = m.mk_func_decl(get_family_id(), _OP_SEQ_SKOLEM, 1, ¶m, n, args, range);
|
||||
return m.mk_app(f, n, args);
|
||||
|
|
|
@ -86,7 +86,7 @@ public:
|
|||
return true;
|
||||
}
|
||||
else {
|
||||
return false;
|
||||
return false;
|
||||
}
|
||||
}
|
||||
NOT_IMPLEMENTED_YET();
|
||||
|
@ -106,7 +106,7 @@ public:
|
|||
sort* seq = nullptr, *ch = nullptr;
|
||||
if (u.is_re(s, seq)) {
|
||||
expr* v0 = get_fresh_value(seq);
|
||||
return u.re.mk_to_re(v0);
|
||||
return u.re.mk_to_re(v0);
|
||||
}
|
||||
if (u.is_char(s)) {
|
||||
//char s[2] = { ++m_char, 0 };
|
||||
|
@ -115,9 +115,23 @@ public:
|
|||
}
|
||||
if (u.is_seq(s, ch)) {
|
||||
expr* v = m_model.get_fresh_value(ch);
|
||||
if (!v) return nullptr;
|
||||
return u.str.mk_unit(v);
|
||||
if (v) {
|
||||
return u.str.mk_unit(v);
|
||||
}
|
||||
else {
|
||||
v = u.str.mk_unit(m_model.get_some_value(ch));
|
||||
expr* uniq = nullptr;
|
||||
if (m_unique_sequences.find(s, uniq)) {
|
||||
uniq = u.str.mk_concat(v, uniq);
|
||||
}
|
||||
else {
|
||||
uniq = v;
|
||||
}
|
||||
m_trail.push_back(uniq);
|
||||
m_unique_sequences.insert(s, uniq);
|
||||
return uniq;
|
||||
}
|
||||
}
|
||||
UNREACHABLE();
|
||||
return nullptr;
|
||||
}
|
||||
|
|
|
@ -46,7 +46,9 @@ expr_ref seq_skolem::mk(symbol const& s, expr* e1, expr* e2, expr* e3, expr* e4,
|
|||
if (!range) {
|
||||
range = m.get_sort(e1);
|
||||
}
|
||||
return expr_ref(seq.mk_skolem(s, len, es, range), m);
|
||||
expr_ref result(seq.mk_skolem(s, len, es, range), m);
|
||||
m_rewrite(result);
|
||||
return result;
|
||||
}
|
||||
|
||||
expr_ref seq_skolem::mk_max_unfolding_depth(unsigned depth) {
|
||||
|
@ -113,13 +115,11 @@ decompose_main:
|
|||
head = seq.str.mk_unit(seq.str.mk_nth_i(s, idx));
|
||||
tail = mk(m_tail, s, idx);
|
||||
m_rewrite(head);
|
||||
m_rewrite(tail);
|
||||
}
|
||||
else {
|
||||
head = seq.str.mk_unit(seq.str.mk_nth_i(e, a.mk_int(0)));
|
||||
tail = mk(m_tail, e, a.mk_int(0));
|
||||
m_rewrite(head);
|
||||
m_rewrite(tail);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue