mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

EndsWith decl and rewriter, WIP

Browse source
This commit is contained in:
Murphy Berzish 2016-06-14 17:55:46 -04:00
parent 4f131ebba7
commit fd38b4c729
6 changed files with 79 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -69,6 +69,28 @@ br_status str_rewriter::mk_str_StartsWith(expr * haystack, expr * needle, expr_r
}
}
br_status str_rewriter::mk_str_EndsWith(expr * haystack, expr * needle, expr_ref & result) {
TRACE("t_str_rw", tout << "rewrite (EndsWith " << mk_pp(haystack, m()) << " " << mk_pp(needle, m()) << ")" << std::endl;);
if (m_strutil.is_string(haystack) && m_strutil.is_string(needle)) {
TRACE("t_str_rw", tout << "evaluating constant EndsWith predicate" << std::endl;);
std::string haystackStr = m_strutil.get_string_constant_value(haystack);
std::string needleStr = m_strutil.get_string_constant_value(needle);
if (haystackStr.length() < needleStr.length()) {
result = m().mk_false();
return BR_DONE;
} else {
if (haystackStr.substr(haystackStr.length() - needleStr.length(), needleStr.length()) == needleStr) {
result = m().mk_true();
} else {
result = m().mk_false();
}
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());
@ -82,6 +104,9 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_STR_STARTSWITH:
SASSERT(num_args == 2);
return mk_str_StartsWith(args[0], args[1], result);
case OP_STR_ENDSWITH:
SASSERT(num_args == 2);
return mk_str_EndsWith(args[0], args[1], result);
default:
return BR_FAILED;
}

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

@ -42,6 +42,7 @@ public:
br_status mk_str_CharAt(expr * arg0, expr * arg1, expr_ref & result);
br_status mk_str_StartsWith(expr * haystack, expr * needle, expr_ref & result);
br_status mk_str_EndsWith(expr * haystack, expr * needle, 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);

7
src/ast/str_decl_plugin.cpp
View file

@ -28,6 +28,7 @@ str_decl_plugin::str_decl_plugin():
m_length_decl(0),
m_charat_decl(0),
m_startswith_decl(0),
m_endswith_decl(0),
m_arith_plugin(0),
m_arith_fid(0),
m_int_sort(0){
@ -43,6 +44,7 @@ void str_decl_plugin::finalize(void) {
DEC_REF(m_length_decl);
DEC_REF(m_charat_decl);
DEC_REF(m_startswith_decl);
DEC_REF(m_endswith_decl);
DEC_REF(m_int_sort);
}
@ -78,6 +80,9 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) {
m_startswith_decl = m->mk_func_decl(symbol("StartsWith"), s, s, boolT, func_decl_info(id, OP_STR_STARTSWITH));
m_manager->inc_ref(m_startswith_decl);
m_endswith_decl = m->mk_func_decl(symbol("EndsWith"), s, s, boolT, func_decl_info(id, OP_STR_ENDSWITH));
m_manager->inc_ref(m_endswith_decl);
}
decl_plugin * str_decl_plugin::mk_fresh() {
@ -97,6 +102,7 @@ func_decl * str_decl_plugin::mk_func_decl(decl_kind k) {
case OP_STRLEN: return m_length_decl;
case OP_STR_CHARAT: return m_charat_decl;
case OP_STR_STARTSWITH: return m_startswith_decl;
case OP_STR_ENDSWITH: return m_endswith_decl;
default: return 0;
}
}
@ -155,6 +161,7 @@ void str_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
op_names.push_back(builtin_name("Length", OP_STRLEN));
op_names.push_back(builtin_name("CharAt", OP_STR_CHARAT));
op_names.push_back(builtin_name("StartsWith", OP_STR_STARTSWITH));
op_names.push_back(builtin_name("EndsWith", OP_STR_ENDSWITH));
}
void str_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {

2
src/ast/str_decl_plugin.h
View file

@ -33,6 +33,7 @@ enum str_op_kind {
// higher-level string functions -- these are reduced to basic operations
OP_STR_CHARAT,
OP_STR_STARTSWITH,
OP_STR_ENDSWITH,
// end
LAST_STR_OP
};
@ -47,6 +48,7 @@ protected:
func_decl * m_charat_decl;
func_decl * m_startswith_decl;
func_decl * m_endswith_decl;
arith_decl_plugin * m_arith_plugin;
family_id m_arith_fid;

40
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_StartsWith_todo.empty()
|| !m_axiom_CharAt_todo.empty() || !m_axiom_StartsWith_todo.empty() || !m_axiom_EndsWith_todo.empty()
;
}
@ -602,6 +602,11 @@ void theory_str::propagate() {
instantiate_axiom_StartsWith(m_axiom_StartsWith_todo[i]);
}
m_axiom_StartsWith_todo.reset();
for (unsigned i = 0; i < m_axiom_EndsWith_todo.size(); ++i) {
instantiate_axiom_EndsWith(m_axiom_EndsWith_todo[i]);
}
m_axiom_EndsWith_todo.reset();
}
}
@ -832,6 +837,37 @@ void theory_str::instantiate_axiom_StartsWith(enode * e) {
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;);
// TODO NEXT
NOT_IMPLEMENTED_YET();
/*
Z3_ast resBoolVar = my_mk_internal_bool_var(t);
Z3_ast ts0 = my_mk_internal_string_var(t);
Z3_ast ts1 = my_mk_internal_string_var(t);
// boolVar = endswith(arg[0], arg[1])
// --------------------------------------------
std::vector<Z3_ast> innerItems;
innerItems.push_back( Z3_mk_eq(ctx, args[0], mk_concat(t, ts0, ts1)) );
innerItems.push_back( Z3_mk_eq(ctx, mk_length(t, ts1), mk_length(t, args[1])) );
innerItems.push_back( Z3_mk_ite(ctx, Z3_mk_eq(ctx, ts1, args[1]), Z3_mk_eq(ctx, resBoolVar, Z3_mk_true(ctx)), Z3_mk_eq(ctx, resBoolVar, Z3_mk_false(ctx) ) ) );
Z3_ast then1 = mk_and_fromVector(t, innerItems);
breakdownAssert = Z3_mk_ite(ctx, Z3_mk_ge(ctx, mk_length(t, args[0]), mk_length(t, args[1])), then1, Z3_mk_eq(ctx, resBoolVar, Z3_mk_false(ctx) ) );
reduceAst = resBoolVar;
*/
}
void theory_str::attach_new_th_var(enode * n) {
context & ctx = get_context();
theory_var v = mk_var(n);
@ -3587,6 +3623,8 @@ void theory_str::set_up_axioms(expr * ex) {
app * ap = to_app(ex);
if (is_StartsWith(ap)) {
m_axiom_StartsWith_todo.push_back(n);
} else if (is_EndsWith(ap)) {
m_axiom_EndsWith_todo.push_back(n);
}
}
} else {

5
src/smt/theory_str.h
View file

@ -109,6 +109,7 @@ namespace smt {
// enode lists for term-specific axioms
ptr_vector<enode> m_axiom_CharAt_todo;
ptr_vector<enode> m_axiom_StartsWith_todo;
ptr_vector<enode> m_axiom_EndsWith_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
@ -180,12 +181,16 @@ namespace smt {
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()); }
bool is_EndsWith(app const * a) const { return a->is_app_of(get_id(), OP_STR_ENDSWITH); }
bool is_EndsWith(enode const * n) const { return is_EndsWith(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 instantiate_axiom_EndsWith(enode * e);
void set_up_axioms(expr * ex);
void handle_equality(expr * lhs, expr * rhs);