mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-02 09:20:22 +00:00
Code Activity

z3str3: heuristics for predicates over int-to-string terms

Browse source
This commit is contained in:
Murphy Berzish 2020-05-12 21:35:24 -04:00
parent 22d0dd863b
commit 51beeec92f
2 changed files with 107 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

102
src/smt/theory_str.cpp
View file

@ -4512,6 +4512,15 @@ namespace smt {
generate_mutual_exclusion(arrangement_disjunction);
}
bool theory_str::get_string_constant_eqc(expr * e, zstring & stringVal) {
bool exists;
expr * strExpr = get_eqc_value(e, exists);
if (!exists) {
return false;}
u.str.is_string(strExpr, stringVal);
return true;
}
/*
* Look through the equivalence class of n to find a string constant.
* Return that constant if it is found, and set hasEqcValue to true.
@ -7019,6 +7028,99 @@ namespace smt {
set_up_axioms(e);
propagate();
}
// heuristics
if (u.str.is_prefix(e)) {
check_consistency_prefix(e, is_true);
} else if (u.str.is_suffix(e)) {
check_consistency_suffix(e, is_true);
} else if (u.str.is_contains(e)) {
check_consistency_contains(e, is_true);
}
}
// terms like int.to.str cannot start with / end with / contain non-digit characters
// in the future this could be expanded to regex checks as well
void theory_str::check_consistency_prefix(expr * e, bool is_true) {
context & ctx = get_context();
ast_manager & m = get_manager();
expr * needle;
expr * haystack;
u.str.is_prefix(e, needle, haystack);
TRACE("str", tout << "check consistency of prefix predicate: " << mk_pp(needle, m) << " prefixof " << mk_pp(haystack, m) << std::endl;);
zstring needleStringConstant;
if (get_string_constant_eqc(needle, needleStringConstant)) {
if (u.str.is_itos(haystack) && is_true) {
// needle cannot contain non-digit characters
for (unsigned i = 0; i < needleStringConstant.length(); ++i) {
if (! ('0' <= needleStringConstant[i] && needleStringConstant[i] <= '9')) {
TRACE("str", tout << "conflict: needle = \"" << needleStringConstant << "\" contains non-digit character, but is a prefix of int-to-string term" << std::endl;);
expr_ref premise(ctx.mk_eq_atom(needle, mk_string(needleStringConstant)), m);
expr_ref conclusion(m.mk_not(e), m);
expr_ref conflict(rewrite_implication(premise, conclusion), m);
assert_axiom_rw(conflict);
return;
}
}
}
}
}
void theory_str::check_consistency_suffix(expr * e, bool is_true) {
context & ctx = get_context();
ast_manager & m = get_manager();
expr * needle;
expr * haystack;
u.str.is_suffix(e, needle, haystack);
TRACE("str", tout << "check consistency of suffix predicate: " << mk_pp(needle, m) << " suffixof " << mk_pp(haystack, m) << std::endl;);
zstring needleStringConstant;
if (get_string_constant_eqc(needle, needleStringConstant)) {
if (u.str.is_itos(haystack) && is_true) {
// needle cannot contain non-digit characters
for (unsigned i = 0; i < needleStringConstant.length(); ++i) {
if (! ('0' <= needleStringConstant[i] && needleStringConstant[i] <= '9')) {
TRACE("str", tout << "conflict: needle = \"" << needleStringConstant << "\" contains non-digit character, but is a suffix of int-to-string term" << std::endl;);
expr_ref premise(ctx.mk_eq_atom(needle, mk_string(needleStringConstant)), m);
expr_ref conclusion(m.mk_not(e), m);
expr_ref conflict(rewrite_implication(premise, conclusion), m);
assert_axiom_rw(conflict);
return;
}
}
}
}
}
void theory_str::check_consistency_contains(expr * e, bool is_true) {
context & ctx = get_context();
ast_manager & m = get_manager();
expr * needle;
expr * haystack;
u.str.is_contains(e, haystack, needle); // first string contains second one
TRACE("str", tout << "check consistency of contains predicate: " << mk_pp(haystack, m) << " contains " << mk_pp(needle, m) << std::endl;);
zstring needleStringConstant;
if (get_string_constant_eqc(needle, needleStringConstant)) {
if (u.str.is_itos(haystack) && is_true) {
// needle cannot contain non-digit characters
for (unsigned i = 0; i < needleStringConstant.length(); ++i) {
if (! ('0' <= needleStringConstant[i] && needleStringConstant[i] <= '9')) {
TRACE("str", tout << "conflict: needle = \"" << needleStringConstant << "\" contains non-digit character, but int-to-string term contains it" << std::endl;);
expr_ref premise(ctx.mk_eq_atom(needle, mk_string(needleStringConstant)), m);
expr_ref conclusion(m.mk_not(e), m);
expr_ref conflict(rewrite_implication(premise, conclusion), m);
assert_axiom_rw(conflict);
return;
}
}
}
}
}
void theory_str::push_scope_eh() {