Skip to content

Commit

Permalink
z3str3: fix incorrect automaton polarity in intersection check, and c…
Browse files Browse the repository at this point in the history 
…lean up code (#4595)
  • Loading branch information
@mtrberzi
mtrberzi committed Jul 28, 2020
1 parent 6910c0d commit afdfc5e
Showing 1 changed file with 30 additions and 45 deletions.
75 changes: 30 additions & 45 deletions src/smt/theory_str_regex.cpp
View file
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

0 comments on commit afdfc5e

Please sign in to comment.