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

regex length term assertion WIP

Browse source
This commit is contained in:
Murphy Berzish 2018-01-16 13:56:01 -05:00
parent 6c4c9a10e4
commit 153701eabe
2 changed files with 50 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

49
src/smt/theory_str.cpp
View file

@ -6735,8 +6735,6 @@ namespace smt {
bool theory_str::refine_automaton_lower_bound(eautomaton * aut, rational current_lower_bound, rational & refined_lower_bound) {
ENSURE(aut != NULL);
ast_manager & m = get_manager();
if (aut->final_states().size() < 1) {
// no solutions at all
refined_lower_bound = rational::minus_one();
@ -9610,6 +9608,53 @@ namespace smt {
if (current_assignment == l_undef) {
continue;
}
if (!regex_terms_with_length_constraints.contains(str_in_re)) {
if (current_assignment == l_true && check_regex_length_linearity(re)) {
TRACE("str", tout << "regex length constraints expected to be linear -- generating and asserting them" << std::endl;);
if (regex_term_to_length_constraint.contains(str_in_re)) {
// use existing length constraint
expr * top_level_length_constraint;
regex_term_to_length_constraint.find(str_in_re, top_level_length_constraint);
ptr_vector<expr> extra_length_vars;
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;
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);
}
} else {
// generate new length constraint
expr_ref_vector extra_length_vars(m);
expr_ref top_level_length_constraint = infer_all_regex_lengths(mk_strlen(str), re, extra_length_vars);
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;
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);
}
regex_term_to_extra_length_vars.insert(str_in_re, vtmp);
}
regex_terms_with_length_constraints.insert(str_in_re);
m_trail_stack.push(insert_obj_trail<theory_str, expr>(regex_terms_with_length_constraints, str_in_re));
regex_axiom_add = true;
}
} // re not in regex_terms_with_length_constraints
rational exact_length_value;
if (get_len_value(str, exact_length_value)) {
TRACE("str", tout << "exact length of " << mk_pp(str, m) << " is " << exact_length_value << std::endl;);

3
src/smt/theory_str.h
View file

@ -409,6 +409,9 @@ protected:
obj_map<expr, svector<regex_automaton_under_assumptions> > regex_automaton_assumptions; // RegEx --> [ aut+assumptions ]
std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
obj_hashtable<expr> regex_terms_with_path_constraints; // set of string terms which have had path constraints asserted in the current scope
obj_hashtable<expr> regex_terms_with_length_constraints; // set of regex terms which had had length constraints asserted in the current scope
obj_map<expr, expr*> regex_term_to_length_constraint; // (str.in.re S R) -> (length constraint over S wrt. R)
obj_map<expr, ptr_vector<expr> > regex_term_to_extra_length_vars; // extra length vars used in regex_term_to_length_constraint entries
// each counter maps a (str.in.re) expression to an integer.
// use helper functions regex_inc_counter() and regex_get_counter() to access