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

support for Indexof2 in theory_str

Browse source
This commit is contained in:
Murphy Berzish 2016-06-15 17:37:17 -04:00
parent 881e3056f3
commit dc5a334d42
6 changed files with 133 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/ast/rewriter/str_rewriter.cpp
View file

@ -130,6 +130,34 @@ br_status str_rewriter::mk_str_Indexof(expr * haystack, expr * needle, expr_ref
}
}
br_status str_rewriter::mk_str_Indexof2(expr * arg0, expr * arg1, expr * arg2, expr_ref & result) {
TRACE("t_str_rw", tout << "rewrite (Indexof2 " << mk_pp(arg0, m()) << " " << mk_pp(arg1, m()) << " " << mk_pp(arg2, m()) << ")" << std::endl;);
//if (getNodeType(t, args[0]) == my_Z3_ConstStr && getNodeType(t, args[1]) == my_Z3_ConstStr && getNodeType(t, args[2]) == my_Z3_Num) {
rational arg2Int;
if (m_strutil.is_string(arg0) && m_strutil.is_string(arg1) && m_autil.is_numeral(arg2, arg2Int)) {
TRACE("t_str_rw", tout << "evaluating constant Indexof2 expression" << std::endl;);
std::string arg0str = m_strutil.get_string_constant_value(arg0);
std::string arg1str = m_strutil.get_string_constant_value(arg1);
if (arg2Int >= rational((unsigned)arg0str.length())) {
result = m_autil.mk_numeral(rational(-1), true);
} else if (arg2Int < rational(0)) {
int index = arg0str.find(arg1str);
result = m_autil.mk_numeral(rational(index), true);
} else {
std::string suffixStr = arg0str.substr(arg2Int.get_unsigned(), arg0str.length() - arg2Int.get_unsigned());
if (suffixStr.find(arg1str) != std::string::npos) {
int index = suffixStr.find(arg1str) + arg2Int.get_unsigned();
result = m_autil.mk_numeral(rational(index), true);
} else {
result = m_autil.mk_numeral(rational(-1), true);
}
}
return BR_DONE;
} else {
return BR_FAILED;
}
}
br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(f->get_family_id() == get_fid());
@ -152,6 +180,9 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_STR_INDEXOF:
SASSERT(num_args == 2);
return mk_str_Indexof(args[0], args[1], result);
case OP_STR_INDEXOF2:
SASSERT(num_args == 3);
return mk_str_Indexof2(args[0], args[1], args[2], result);
default:
return BR_FAILED;
}

1
src/ast/rewriter/str_rewriter.h
View file

@ -45,6 +45,7 @@ public:
br_status mk_str_EndsWith(expr * haystack, expr * needle, expr_ref & result);
br_status mk_str_Contains(expr * haystack, expr * needle, expr_ref & result);
br_status mk_str_Indexof(expr * haystack, expr * needle, expr_ref & result);
br_status mk_str_Indexof2(expr * arg0, expr * arg1, expr * arg2, expr_ref & result);
bool reduce_eq(expr * l, expr * r, expr_ref_vector & lhs, expr_ref_vector & rhs, bool & change);
bool reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change);

10
src/ast/str_decl_plugin.cpp
View file

@ -31,6 +31,7 @@ str_decl_plugin::str_decl_plugin():
m_endswith_decl(0),
m_contains_decl(0),
m_indexof_decl(0),
m_indexof2_decl(0),
m_arith_plugin(0),
m_arith_fid(0),
m_int_sort(0){
@ -49,6 +50,7 @@ void str_decl_plugin::finalize(void) {
DEC_REF(m_endswith_decl);
DEC_REF(m_contains_decl);
DEC_REF(m_indexof_decl);
DEC_REF(m_indexof2_decl);
DEC_REF(m_int_sort);
}
@ -93,6 +95,12 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) {
m_indexof_decl = m->mk_func_decl(symbol("Indexof"), s, s, i, func_decl_info(id, OP_STR_INDEXOF));
m_manager->inc_ref(m_indexof_decl);
{
sort * d[3] = { s, s, i };
m_indexof2_decl = m->mk_func_decl(symbol("Indexof2"), 3, d, i, func_decl_info(id, OP_STR_INDEXOF2));
m_manager->inc_ref(m_indexof2_decl);
}
}
decl_plugin * str_decl_plugin::mk_fresh() {
@ -115,6 +123,7 @@ func_decl * str_decl_plugin::mk_func_decl(decl_kind k) {
case OP_STR_ENDSWITH: return m_endswith_decl;
case OP_STR_CONTAINS: return m_contains_decl;
case OP_STR_INDEXOF: return m_indexof_decl;
case OP_STR_INDEXOF2: return m_indexof2_decl;
default: return 0;
}
}
@ -176,6 +185,7 @@ void str_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
op_names.push_back(builtin_name("EndsWith", OP_STR_ENDSWITH));
op_names.push_back(builtin_name("Contains", OP_STR_CONTAINS));
op_names.push_back(builtin_name("Indexof", OP_STR_INDEXOF));
op_names.push_back(builtin_name("Indexof2", OP_STR_INDEXOF2));
}
void str_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {

2
src/ast/str_decl_plugin.h
View file

@ -36,6 +36,7 @@ enum str_op_kind {
OP_STR_ENDSWITH,
OP_STR_CONTAINS,
OP_STR_INDEXOF,
OP_STR_INDEXOF2,
// end
LAST_STR_OP
};
@ -53,6 +54,7 @@ protected:
func_decl * m_endswith_decl;
func_decl * m_contains_decl;
func_decl * m_indexof_decl;
func_decl * m_indexof2_decl;
arith_decl_plugin * m_arith_plugin;
family_id m_arith_fid;

84
src/smt/theory_str.cpp
View file

@ -531,6 +531,15 @@ app * theory_str::mk_contains(expr * haystack, expr * needle) {
return contains;
}
app * theory_str::mk_indexof(expr * haystack, expr * needle) {
expr * args[2] = {haystack, needle};
app * indexof = get_manager().mk_app(get_id(), OP_STR_INDEXOF, 0, 0, 2, args);
// immediately force internalization so that axiom setup does not fail
get_context().internalize(indexof, false);
set_up_axioms(indexof);
return indexof;
}
app * theory_str::mk_strlen(expr * e) {
/*if (m_strutil.is_string(e)) {*/ if (false) {
const char * strval = 0;
@ -602,7 +611,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_StartsWith_todo.empty() || !m_axiom_EndsWith_todo.empty()
|| !m_axiom_Contains_todo.empty() || !m_axiom_Indexof_todo.empty()
|| !m_axiom_Contains_todo.empty() || !m_axiom_Indexof_todo.empty() || !m_axiom_Indexof2_todo.empty()
;
}
@ -651,6 +660,11 @@ void theory_str::propagate() {
instantiate_axiom_Indexof(m_axiom_Indexof_todo[i]);
}
m_axiom_Indexof_todo.reset();
for (unsigned i = 0; i < m_axiom_Indexof2_todo.size(); ++i) {
instantiate_axiom_Indexof2(m_axiom_Indexof2_todo[i]);
}
m_axiom_Indexof2_todo.reset();
}
}
@ -994,6 +1008,74 @@ void theory_str::instantiate_axiom_Indexof(enode * e) {
assert_axiom(finalAxiom);
}
void theory_str::instantiate_axiom_Indexof2(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 Indexof2 axiom for " << mk_pp(expr, m) << std::endl;);
return;
}
axiomatized_terms.insert(expr);
TRACE("t_str_detail", tout << "instantiate Indexof2 axiom for " << mk_pp(expr, m) << std::endl;);
// -------------------------------------------------------------------------------
// if (arg[2] >= length(arg[0])) // ite2
// resAst = -1
// else
// args[0] = prefix . suffix
// /\ indexAst = indexof(suffix, arg[1])
// /\ args[2] = len(prefix)
// /\ if (indexAst == -1) resAst = indexAst // ite3
// else resAst = args[2] + indexAst
// -------------------------------------------------------------------------------
expr_ref resAst(mk_int_var("res"), m);
expr_ref indexAst(mk_int_var("index"), m);
expr_ref prefix(mk_str_var("prefix"), m);
expr_ref suffix(mk_str_var("suffix"), m);
expr_ref prefixLen(mk_strlen(prefix), m);
expr_ref zeroAst(mk_int(0), m);
expr_ref negOneAst(mk_int(-1), m);
expr_ref ite3(m.mk_ite(
ctx.mk_eq_atom(indexAst, negOneAst),
ctx.mk_eq_atom(resAst, negOneAst),
ctx.mk_eq_atom(resAst, m_autil.mk_add(expr->get_arg(2), indexAst))
),m);
expr_ref_vector ite2ElseItems(m);
ite2ElseItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(prefix, suffix)));
ite2ElseItems.push_back(ctx.mk_eq_atom(indexAst, mk_indexof(suffix, expr->get_arg(1))));
ite2ElseItems.push_back(ctx.mk_eq_atom(expr->get_arg(2), prefixLen));
ite2ElseItems.push_back(ite3);
expr_ref ite2Else(m.mk_and(ite2ElseItems.size(), ite2ElseItems.c_ptr()), m);
SASSERT(ite2Else);
expr_ref ite2(m.mk_ite(
//m_autil.mk_ge(expr->get_arg(2), mk_strlen(expr->get_arg(0))),
m_autil.mk_ge(m_autil.mk_add(expr->get_arg(2), m_autil.mk_mul(mk_int(-1), mk_strlen(expr->get_arg(0)))), zeroAst),
ctx.mk_eq_atom(resAst, negOneAst),
ite2Else
), m);
SASSERT(ite2);
expr_ref ite1(m.mk_ite(
//m_autil.mk_lt(expr->get_arg(2), zeroAst),
m.mk_not(m_autil.mk_ge(expr->get_arg(2), zeroAst)),
ctx.mk_eq_atom(resAst, mk_indexof(expr->get_arg(0), expr->get_arg(1))),
ite2
), m);
SASSERT(ite1);
assert_axiom(ite1);
expr_ref reduceTerm(ctx.mk_eq_atom(expr, resAst), m);
SASSERT(reduceTerm);
assert_axiom(reduceTerm);
}
void theory_str::attach_new_th_var(enode * n) {
context & ctx = get_context();
theory_var v = mk_var(n);

6
src/smt/theory_str.h
View file

@ -107,11 +107,13 @@ namespace smt {
ptr_vector<enode> m_string_constant_length_todo;
// enode lists for term-specific axioms
// TODO maybe refactor this into a generic "library_aware_axiom_todo" list
ptr_vector<enode> m_axiom_CharAt_todo;
ptr_vector<enode> m_axiom_StartsWith_todo;
ptr_vector<enode> m_axiom_EndsWith_todo;
ptr_vector<enode> m_axiom_Contains_todo;
ptr_vector<enode> m_axiom_Indexof_todo;
ptr_vector<enode> m_axiom_Indexof2_todo;
// hashtable of all exprs for which we've already set up term-specific axioms --
// this prevents infinite recursive descent with respect to axioms that
@ -158,6 +160,7 @@ namespace smt {
expr * mk_concat(expr * n1, expr * n2);
expr * mk_concat_const_str(expr * n1, expr * n2);
app * mk_contains(expr * haystack, expr * needle);
app * mk_indexof(expr * haystack, expr * needle);
literal mk_literal(expr* _e);
app * mk_int(int n);
@ -191,6 +194,8 @@ namespace smt {
bool is_Contains(enode const * n) const { return is_Contains(n->get_owner()); }
bool is_Indexof(app const * a) const { return a->is_app_of(get_id(), OP_STR_INDEXOF); }
bool is_Indexof(enode const * n) const { return is_Indexof(n->get_owner()); }
bool is_Indexof2(app const * a) const { return a->is_app_of(get_id(), OP_STR_INDEXOF2); }
bool is_Indexof2(enode const * n) const { return is_Indexof2(n->get_owner()); }
void instantiate_concat_axiom(enode * cat);
void instantiate_basic_string_axioms(enode * str);
@ -201,6 +206,7 @@ namespace smt {
void instantiate_axiom_EndsWith(enode * e);
void instantiate_axiom_Contains(enode * e);
void instantiate_axiom_Indexof(enode * e);
void instantiate_axiom_Indexof2(enode * e);
void set_up_axioms(expr * ex);
void handle_equality(expr * lhs, expr * rhs);