mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

axioms for StartsWith; WIP as I need to fix an infinite recursion bug

Browse source
This commit is contained in:
Murphy Berzish 2016-06-14 16:16:39 -04:00
parent 7d8e54c50f
commit c5ffb012dd
2 changed files with 56 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

53
src/smt/theory_str.cpp
View file

@ -568,7 +568,7 @@ expr * theory_str::mk_concat(expr * n1, expr * n2) {
bool theory_str::can_propagate() {
return !m_basicstr_axiom_todo.empty() || !m_str_eq_todo.empty() || !m_concat_axiom_todo.empty()
|| !m_axiom_CharAt_todo.empty()
|| !m_axiom_CharAt_todo.empty() || !m_axiom_StartsWith_todo.empty()
;
}
@ -597,6 +597,10 @@ void theory_str::propagate() {
instantiate_axiom_CharAt(m_axiom_CharAt_todo[i]);
}
m_axiom_CharAt_todo.reset();
for (unsigned i = 0; i < m_axiom_StartsWith_todo.size(); ++i) {
instantiate_axiom_StartsWith(m_axiom_StartsWith_todo[i]);
}
}
}
@ -783,6 +787,39 @@ void theory_str::instantiate_axiom_CharAt(enode * e) {
assert_axiom(finalAxiom);
}
void theory_str::instantiate_axiom_StartsWith(enode * e) {
context & ctx = get_context();
ast_manager & m = get_manager();
app * expr = e->get_owner();
TRACE("t_str_detail", tout << "instantiate StartsWith 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(ts0), mk_strlen(expr->get_arg(1))));
innerItems.push_back(m.mk_ite(ctx.mk_eq_atom(ts0, expr->get_arg(1)), 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::attach_new_th_var(enode * n) {
context & ctx = get_context();
theory_var v = mk_var(n);
@ -3491,6 +3528,7 @@ void theory_str::set_up_axioms(expr * ex) {
sort * ex_sort = m.get_sort(ex);
sort * str_sort = m.mk_sort(get_family_id(), STRING_SORT);
sort * bool_sort = m.mk_bool_sort();
if (ex_sort == str_sort) {
TRACE("t_str_detail", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) <<
@ -3526,6 +3564,19 @@ void theory_str::set_up_axioms(expr * ex) {
TRACE("t_str_detail", tout << "variable " << mk_ismt2_pp(ap, get_manager()) << " is #" << v << std::endl;);
}
}
} else if (ex_sort == bool_sort) {
TRACE("t_str_detail", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) <<
": expr is of sort Bool" << std::endl;);
// set up axioms for boolean terms
enode * n = ctx.get_enode(ex);
SASSERT(n);
if (is_app(ex)) {
app * ap = to_app(ex);
if (is_StartsWith(ap)) {
m_axiom_StartsWith_todo.push_back(n);
}
}
} else {
TRACE("t_str_detail", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) <<
": expr is of wrong sort, ignoring" << std::endl;);

4
src/smt/theory_str.h
View file

@ -108,6 +108,7 @@ namespace smt {
// enode lists for term-specific axioms
ptr_vector<enode> m_axiom_CharAt_todo;
ptr_vector<enode> m_axiom_StartsWith_todo;
int tmpStringVarCount;
int tmpXorVarCount;
@ -172,11 +173,14 @@ namespace smt {
bool is_strlen(enode const * n) const { return is_strlen(n->get_owner()); }
bool is_CharAt(app const * a) const { return a->is_app_of(get_id(), OP_STR_CHARAT); }
bool is_CharAt(enode const * n) const { return is_CharAt(n->get_owner()); }
bool is_StartsWith(app const * a) const { return a->is_app_of(get_id(), OP_STR_STARTSWITH); }
bool is_StartsWith(enode const * n) const { return is_StartsWith(n->get_owner()); }
void instantiate_concat_axiom(enode * cat);
void instantiate_basic_string_axioms(enode * str);
void instantiate_str_eq_length_axiom(enode * lhs, enode * rhs);
void instantiate_axiom_CharAt(enode * e);
void instantiate_axiom_StartsWith(enode * e);
void set_up_axioms(expr * ex);
void handle_equality(expr * lhs, expr * rhs);