mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

avoid crash on quantifiers + sequences

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-05-03 16:24:12 -07:00
parent 52e367417f
commit d11d9bd1de
2 changed files with 25 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_seq.cpp
View file

@ -2380,7 +2380,7 @@ void theory_seq::init_model(expr_ref_vector const& es) {
}
void theory_seq::init_model(model_generator & mg) {
m_factory = alloc(seq_factory, get_manager(), get_family_id());
m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model());
mg.register_factory(m_factory);
for (unsigned j = 0; j < m_nqs.size(); ++j) {
ne const& n = m_nqs[j];
@ -2469,7 +2469,9 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
for (unsigned i = 0; i < concats.size(); ++i) {
expr* c = concats[i], *c1;
if (m_util.str.is_unit(c, c1)) {
sv->add_dependency(ctx.get_enode(c1));
if (ctx.e_internalized(c1)) {
sv->add_dependency(ctx.get_enode(c1));
}
}
else if (m_util.str.is_string(c)) {
sv->add_string(c);

25
src/smt/theory_seq_empty.h
View file

@ -25,6 +25,7 @@ Revision History:
namespace smt {
class seq_factory : public value_factory {
typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
proto_model& m_model;
ast_manager& m;
seq_util u;
symbol_set m_strings;
@ -34,8 +35,9 @@ namespace smt {
expr_ref_vector m_trail;
public:
seq_factory(ast_manager & m, family_id fid):
seq_factory(ast_manager & m, family_id fid, proto_model& md):
value_factory(m, fid),
m_model(md),
m(m),
u(m),
m_next(0),
@ -78,6 +80,17 @@ namespace smt {
v2 = u.str.mk_string(symbol("b"));
return true;
}
sort* ch;
if (u.is_seq(s, ch)) {
if (m_model.get_some_values(ch, v1, v2)) {
v1 = u.str.mk_unit(v1);
v2 = u.str.mk_unit(v2);
return true;
}
else {
return false;
}
}
NOT_IMPLEMENTED_YET();
return false;
}
@ -92,7 +105,7 @@ namespace smt {
return u.str.mk_string(sym);
}
}
sort* seq = 0;
sort* seq = 0, *ch = 0;
if (u.is_re(s, seq)) {
expr* v0 = get_fresh_value(seq);
return u.re.mk_to_re(v0);
@ -102,7 +115,11 @@ namespace smt {
//return u.str.mk_char(zstring(s), 0);
return u.str.mk_char(zstring("a"), 0);
}
NOT_IMPLEMENTED_YET();
if (u.is_seq(s, ch)) {
expr* v = m_model.get_fresh_value(ch);
return u.str.mk_unit(v);
}
UNREACHABLE();
return 0;
}
virtual void register_value(expr* n) {
@ -126,7 +143,7 @@ namespace smt {
public:
theory_seq_empty(ast_manager& m):theory(m.mk_family_id("seq")), m_used(false) {}
virtual void init_model(model_generator & mg) {
mg.register_factory(alloc(seq_factory, get_manager(), get_family_id()));
mg.register_factory(alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()));
}
};