mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fixup startswith/endswith to prefixof/suffixof

Browse source
This commit is contained in:
Murphy Berzish 2017-03-13 17:03:36 -04:00
parent 94d5f242b8
commit 24df976f95
2 changed files with 52 additions and 55 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

103
src/smt/theory_str.cpp
View file

@ -817,12 +817,10 @@ void theory_str::propagate() {
instantiate_axiom_int_to_str(e); instantiate_axiom_int_to_str(e);
} else if (u.str.is_at(a)) { } else if (u.str.is_at(a)) {
instantiate_axiom_CharAt(e); instantiate_axiom_CharAt(e);
/* TODO NEXT: StartsWith/EndsWith -> prefixof/suffixof } else if (u.str.is_prefix(a)) {
} else if (is_StartsWith(e)) { instantiate_axiom_prefixof(e);
instantiate_axiom_StartsWith(e); } else if (u.str.is_suffix(a)) {
} else if (is_EndsWith(e)) { instantiate_axiom_suffixof(e);
instantiate_axiom_EndsWith(e);
*/
} else if (u.str.is_contains(a)) { } else if (u.str.is_contains(a)) {
instantiate_axiom_Contains(e); instantiate_axiom_Contains(e);
} else if (u.str.is_index(a)) { } else if (u.str.is_index(a)) {
@ -1101,64 +1099,26 @@ void theory_str::instantiate_axiom_CharAt(enode * e) {
assert_axiom(finalAxiom); assert_axiom(finalAxiom);
} }
void theory_str::instantiate_axiom_StartsWith(enode * e) { void theory_str::instantiate_axiom_prefixof(enode * e) {
context & ctx = get_context(); context & ctx = get_context();
ast_manager & m = get_manager(); ast_manager & m = get_manager();
app * expr = e->get_owner(); app * expr = e->get_owner();
if (axiomatized_terms.contains(expr)) { if (axiomatized_terms.contains(expr)) {
TRACE("t_str_detail", tout << "already set up StartsWith axiom for " << mk_pp(expr, m) << std::endl;); TRACE("t_str_detail", tout << "already set up prefixof axiom for " << mk_pp(expr, m) << std::endl;);
return; return;
} }
axiomatized_terms.insert(expr); axiomatized_terms.insert(expr);
TRACE("t_str_detail", tout << "instantiate StartsWith axiom for " << mk_pp(expr, m) << std::endl;); TRACE("t_str_detail", tout << "instantiate prefixof axiom for " << mk_pp(expr, m) << std::endl;);
expr_ref ts0(mk_str_var("ts0"), m); expr_ref ts0(mk_str_var("ts0"), m);
expr_ref ts1(mk_str_var("ts1"), m); expr_ref ts1(mk_str_var("ts1"), m);
expr_ref_vector innerItems(m); expr_ref_vector innerItems(m);
innerItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(ts0, ts1))); innerItems.push_back(ctx.mk_eq_atom(expr->get_arg(1), mk_concat(ts0, ts1)));
innerItems.push_back(ctx.mk_eq_atom(mk_strlen(ts0), mk_strlen(expr->get_arg(1)))); innerItems.push_back(ctx.mk_eq_atom(mk_strlen(ts0), mk_strlen(expr->get_arg(0))));
innerItems.push_back(m.mk_ite(ctx.mk_eq_atom(ts0, expr->get_arg(1)), expr, m.mk_not(expr))); innerItems.push_back(m.mk_ite(ctx.mk_eq_atom(ts0, expr->get_arg(0)), expr, m.mk_not(expr)));
expr_ref then1(m.mk_and(innerItems.size(), innerItems.c_ptr()), m);
SASSERT(then1);
// the top-level condition is Length(arg0) >= Length(arg1).
// of course, the integer theory is not so accommodating
expr_ref topLevelCond(
m_autil.mk_ge(
m_autil.mk_add(
mk_strlen(expr->get_arg(0)), m_autil.mk_mul(mk_int(-1), mk_strlen(expr->get_arg(1)))),
mk_int(0))
, m);
SASSERT(topLevelCond);
expr_ref finalAxiom(m.mk_ite(topLevelCond, then1, m.mk_not(expr)), m);
SASSERT(finalAxiom);
assert_axiom(finalAxiom);
}
void theory_str::instantiate_axiom_EndsWith(enode * e) {
context & ctx = get_context();
ast_manager & m = get_manager();
app * expr = e->get_owner();
if (axiomatized_terms.contains(expr)) {
TRACE("t_str_detail", tout << "already set up EndsWith axiom for " << mk_pp(expr, m) << std::endl;);
return;
}
axiomatized_terms.insert(expr);
TRACE("t_str_detail", tout << "instantiate EndsWith axiom for " << mk_pp(expr, m) << std::endl;);
expr_ref ts0(mk_str_var("ts0"), m);
expr_ref ts1(mk_str_var("ts1"), m);
expr_ref_vector innerItems(m);
innerItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(ts0, ts1)));
innerItems.push_back(ctx.mk_eq_atom(mk_strlen(ts1), mk_strlen(expr->get_arg(1))));
innerItems.push_back(m.mk_ite(ctx.mk_eq_atom(ts1, expr->get_arg(1)), expr, m.mk_not(expr)));
expr_ref then1(m.mk_and(innerItems.size(), innerItems.c_ptr()), m); expr_ref then1(m.mk_and(innerItems.size(), innerItems.c_ptr()), m);
SASSERT(then1); SASSERT(then1);
@ -1166,9 +1126,46 @@ void theory_str::instantiate_axiom_EndsWith(enode * e) {
expr_ref topLevelCond( expr_ref topLevelCond(
m_autil.mk_ge( m_autil.mk_ge(
m_autil.mk_add( m_autil.mk_add(
mk_strlen(expr->get_arg(0)), m_autil.mk_mul(mk_int(-1), mk_strlen(expr->get_arg(1)))), mk_strlen(expr->get_arg(1)), m_autil.mk_mul(mk_int(-1), mk_strlen(expr->get_arg(0)))),
mk_int(0)) mk_int(0))
, m); , m);
SASSERT(topLevelCond);
expr_ref finalAxiom(m.mk_ite(topLevelCond, then1, m.mk_not(expr)), m);
SASSERT(finalAxiom);
assert_axiom(finalAxiom);
}
void theory_str::instantiate_axiom_suffixof(enode * e) {
context & ctx = get_context();
ast_manager & m = get_manager();
app * expr = e->get_owner();
if (axiomatized_terms.contains(expr)) {
TRACE("t_str_detail", tout << "already set up suffixof axiom for " << mk_pp(expr, m) << std::endl;);
return;
}
axiomatized_terms.insert(expr);
TRACE("t_str_detail", tout << "instantiate suffixof axiom for " << mk_pp(expr, m) << std::endl;);
expr_ref ts0(mk_str_var("ts0"), m);
expr_ref ts1(mk_str_var("ts1"), m);
expr_ref_vector innerItems(m);
innerItems.push_back(ctx.mk_eq_atom(expr->get_arg(1), mk_concat(ts0, ts1)));
innerItems.push_back(ctx.mk_eq_atom(mk_strlen(ts1), mk_strlen(expr->get_arg(0))));
innerItems.push_back(m.mk_ite(ctx.mk_eq_atom(ts1, expr->get_arg(0)), expr, m.mk_not(expr)));
expr_ref then1(m.mk_and(innerItems.size(), innerItems.c_ptr()), m);
SASSERT(then1);
// the top-level condition is Length(arg0) >= Length(arg1)
expr_ref topLevelCond(
m_autil.mk_ge(
m_autil.mk_add(
mk_strlen(expr->get_arg(1)), m_autil.mk_mul(mk_int(-1), mk_strlen(expr->get_arg(0)))),
mk_int(0))
, m);
SASSERT(topLevelCond); SASSERT(topLevelCond);
expr_ref finalAxiom(m.mk_ite(topLevelCond, then1, m.mk_not(expr)), m); expr_ref finalAxiom(m.mk_ite(topLevelCond, then1, m.mk_not(expr)), m);

4
src/smt/theory_str.h
View file

@ -433,8 +433,8 @@ namespace smt {
void instantiate_str_eq_length_axiom(enode * lhs, enode * rhs); void instantiate_str_eq_length_axiom(enode * lhs, enode * rhs);
void instantiate_axiom_CharAt(enode * e); void instantiate_axiom_CharAt(enode * e);
void instantiate_axiom_StartsWith(enode * e); void instantiate_axiom_prefixof(enode * e);
void instantiate_axiom_EndsWith(enode * e); void instantiate_axiom_suffixof(enode * e);
void instantiate_axiom_Contains(enode * e); void instantiate_axiom_Contains(enode * e);
void instantiate_axiom_Indexof(enode * e); void instantiate_axiom_Indexof(enode * e);
void instantiate_axiom_Indexof2(enode * e); void instantiate_axiom_Indexof2(enode * e);