Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

z3str3: fix incorrect automaton polarity in intersection check #4595

Merged
merged 1 commit into from
Jul 28, 2020
Merged

z3str3: fix incorrect automaton polarity in intersection check #4595

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
75 changes: 30 additions & 45 deletions src/smt/theory_str_regex.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,8 +48,7 @@ namespace smt {

// TODO since heuristics might fail, the "no progress" flag might need to be handled specially here
bool regex_axiom_add = false;
for (obj_hashtable<expr>::iterator it = regex_terms.begin(); it != regex_terms.end(); ++it) {
expr * str_in_re = *it;
for (auto str_in_re : regex_terms) {
expr * str = nullptr;
expr * re = nullptr;
u.str.is_in_re(str_in_re, str, re);
Expand Down Expand Up @@ -78,8 +77,7 @@ namespace smt {
regex_term_to_extra_length_vars.find(str_in_re, extra_length_vars);

assert_axiom(top_level_length_constraint);
for(ptr_vector<expr>::iterator it = extra_length_vars.begin(); it != extra_length_vars.end(); ++it) {
expr * v = *it;
for(auto v : extra_length_vars) {
refresh_theory_var(v);
expr_ref len_constraint(m_autil.mk_ge(v, m_autil.mk_numeral(rational::zero(), true)), m);
assert_axiom(len_constraint);
Expand All @@ -95,16 +93,15 @@ namespace smt {
TRACE("str", tout << "top-level length constraint: " << mk_pp(top_level_length_constraint, m) << std::endl;);
// assert and track length constraint
assert_axiom(top_level_length_constraint);
for(expr_ref_vector::iterator it = extra_length_vars.begin(); it != extra_length_vars.end(); ++it) {
expr * v = *it;
for(auto v : extra_length_vars) {
expr_ref len_constraint(m_autil.mk_ge(v, m_autil.mk_numeral(rational::zero(), true)), m);
assert_axiom(len_constraint);
}

regex_term_to_length_constraint.insert(str_in_re, top_level_length_constraint);
ptr_vector<expr> vtmp;
for(expr_ref_vector::iterator it = extra_length_vars.begin(); it != extra_length_vars.end(); ++it) {
vtmp.push_back(*it);
for(auto v : extra_length_vars) {
vtmp.push_back(v);
}
regex_term_to_extra_length_vars.insert(str_in_re, vtmp);
}
Expand All @@ -129,9 +126,7 @@ namespace smt {
regex_automaton_under_assumptions assumption;
if (regex_automaton_assumptions.contains(re) &&
!regex_automaton_assumptions[re].empty()){
for (svector<regex_automaton_under_assumptions>::iterator it = regex_automaton_assumptions[re].begin();
it != regex_automaton_assumptions[re].end(); ++it) {
regex_automaton_under_assumptions autA = *it;
for (auto autA : regex_automaton_assumptions[re]) {
rational assumed_upper_bound, assumed_lower_bound;
bool assumes_upper_bound = autA.get_upper_bound(assumed_upper_bound);
bool assumes_lower_bound = autA.get_lower_bound(assumed_lower_bound);
Expand Down Expand Up @@ -276,9 +271,7 @@ namespace smt {
bool need_assumption = true;
regex_automaton_under_assumptions last_assumption;
rational last_ub = rational::minus_one();
for (svector<regex_automaton_under_assumptions>::iterator it = regex_automaton_assumptions[re].begin();
it != regex_automaton_assumptions[re].end(); ++it) {
regex_automaton_under_assumptions autA = *it;
for (auto autA : regex_automaton_assumptions[re]) {
if ((current_assignment == l_true && autA.get_polarity() == false)
|| (current_assignment == l_false && autA.get_polarity() == true)) {
// automaton uses incorrect polarity
Expand Down Expand Up @@ -399,9 +392,7 @@ namespace smt {
bool need_assumption = true;
regex_automaton_under_assumptions last_assumption;
rational last_lb = rational::zero(); // the default
for (svector<regex_automaton_under_assumptions>::iterator it = regex_automaton_assumptions[re].begin();
it != regex_automaton_assumptions[re].end(); ++it) {
regex_automaton_under_assumptions autA = *it;
for (auto autA : regex_automaton_assumptions[re]) {
if ((current_assignment == l_true && autA.get_polarity() == false)
|| (current_assignment == l_false && autA.get_polarity() == true)) {
// automaton uses incorrect polarity
Expand Down Expand Up @@ -540,12 +531,11 @@ namespace smt {
}
} // foreach (entry in regex_terms)

for (obj_map<expr, ptr_vector<expr> >::iterator it = regex_terms_by_string.begin();
it != regex_terms_by_string.end(); ++it) {
for (auto entry : regex_terms_by_string) {
// TODO do we need to check equivalence classes of strings here?

expr * str = it->m_key;
ptr_vector<expr> str_in_re_terms = it->m_value;
expr* str = entry.m_key;
ptr_vector<expr> str_in_re_terms = entry.m_value;

svector<regex_automaton_under_assumptions> intersect_constraints;
// we may find empty intersection before checking every constraint;
Expand All @@ -554,12 +544,11 @@ namespace smt {

// choose an automaton/assumption for each assigned (str.in.re)
// that's consistent with the current length information
for (ptr_vector<expr>::iterator term_it = str_in_re_terms.begin();
term_it != str_in_re_terms.end(); ++term_it) {
for (auto str_in_re_term : str_in_re_terms) {
expr * _unused = nullptr;
expr * re = nullptr;
SASSERT(u.str.is_in_re(*term_it));
u.str.is_in_re(*term_it, _unused, re);
SASSERT(u.str.is_in_re(str_in_re_term));
u.str.is_in_re(str_in_re_term, _unused, re);

rational exact_len;
bool has_exact_len = get_len_value(str, exact_len);
Expand All @@ -570,9 +559,7 @@ namespace smt {

if (regex_automaton_assumptions.contains(re) &&
!regex_automaton_assumptions[re].empty()){
for (svector<regex_automaton_under_assumptions>::iterator aut_it = regex_automaton_assumptions[re].begin();
aut_it != regex_automaton_assumptions[re].end(); ++aut_it) {
regex_automaton_under_assumptions aut = *aut_it;
for (auto aut : regex_automaton_assumptions[re]) {
rational aut_ub;
bool assume_ub = aut.get_upper_bound(aut_ub);
rational aut_lb;
Expand Down Expand Up @@ -615,16 +602,7 @@ namespace smt {

eautomaton * aut_inter = nullptr;
CTRACE("str", !intersect_constraints.empty(), tout << "check intersection of automata constraints for " << mk_pp(str, m) << std::endl;);
for (svector<regex_automaton_under_assumptions>::iterator aut_it = intersect_constraints.begin();
aut_it != intersect_constraints.end(); ++aut_it) {
regex_automaton_under_assumptions aut = *aut_it;
if (aut_inter == nullptr) {
// start somewhere
aut_inter = aut.get_automaton();
used_intersect_constraints.push_back(aut);
continue;
}

for (auto aut : intersect_constraints) {
TRACE("str",
{
unsigned v = regex_get_counter(regex_length_attempt_count, aut.get_regex_term());
Expand All @@ -646,8 +624,12 @@ namespace smt {
// TODO do we need to push the intermediates into a vector for deletion anyway?
if ( (current_assignment == l_true && aut.get_polarity())
|| (current_assignment == l_false && !aut.get_polarity())) {
aut_inter = m_mk_aut.mk_product(aut_inter, aut.get_automaton());
m_automata.push_back(aut_inter);
if (aut_inter == nullptr) {
aut_inter = aut.get_automaton();
} else {
aut_inter = m_mk_aut.mk_product(aut_inter, aut.get_automaton());
m_automata.push_back(aut_inter);
}
} else {
// need to complement first
expr_ref rc(u.re.mk_complement(aut.get_regex_term()), m);
Expand All @@ -659,8 +641,12 @@ namespace smt {
regex_automata.push_back(aut_c);
// TODO is there any way to build a complement automaton from an existing one?
// this discards length information
aut_inter = m_mk_aut.mk_product(aut_inter, aut_c);
m_automata.push_back(aut_inter);
if (aut_inter == nullptr) {
aut_inter = aut_c;
} else {
aut_inter = m_mk_aut.mk_product(aut_inter, aut_c);
m_automata.push_back(aut_inter);
}
}
used_intersect_constraints.push_back(aut);
if (aut_inter->is_empty()) {
Expand All @@ -679,9 +665,7 @@ namespace smt {

expr_ref_vector conflict_terms(m);
expr_ref conflict_lhs(m);
for (svector<regex_automaton_under_assumptions>::iterator aut_it = used_intersect_constraints.begin();
aut_it != used_intersect_constraints.end(); ++aut_it) {
regex_automaton_under_assumptions aut = *aut_it;
for (auto aut : used_intersect_constraints) {
expr * str_in_re_term(u.re.mk_in_re(str, aut.get_regex_term()));
lbool current_assignment = ctx.get_assignment(str_in_re_term);
if (current_assignment == l_true) {
Expand All @@ -702,6 +686,7 @@ namespace smt {
}
}
conflict_lhs = mk_and(conflict_terms);
TRACE("str", tout << "conflict lhs: " << mk_pp(conflict_lhs, m) << std::endl;);

if (used_intersect_constraints.size() > 1 && aut_inter != nullptr) {
// check whether the intersection is only the empty string
Expand Down