From 191cc30e2a6116b1f3c03c05495bb52da762275a Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 15 Jan 2018 15:30:12 -0500 Subject: [PATCH] intersection of regex constraints produces a conflict clause --- src/smt/theory_str.cpp | 56 +++++++++++++++++++++++++++++++++++++----- src/smt/theory_str.h | 10 ++++---- 2 files changed, 55 insertions(+), 11 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 1fc04c77f..4c36b0f45 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -9637,7 +9637,13 @@ namespace smt { regex_axiom_add = true; // increment LengthAttemptCount - regex_inc_counter(regex_length_attempt_count, str_in_re); + regex_inc_counter(regex_length_attempt_count, re); + + { + unsigned v = regex_get_counter(regex_length_attempt_count, re); + TRACE("str", tout << "length attempt count for " << mk_pp(re, m) << " is " << v << std::endl;); + } + continue; } else { // no automata available, or else all bounds assumptions are invalid @@ -9910,8 +9916,6 @@ namespace smt { } } } - - // NOT_IMPLEMENTED_YET(); } // foreach (entry in regex_terms) for (obj_map >::iterator it = regex_terms_by_string.begin(); @@ -9999,11 +10003,19 @@ namespace smt { continue; } + { + unsigned v = regex_get_counter(regex_length_attempt_count, aut.get_regex_term()); + TRACE("str", tout << "length attempt count of " << mk_pp(aut.get_regex_term(), m) << " is " << v + << ", threshold is " << m_params.m_RegexAutomata_LengthAttemptThreshold << std::endl;); + } + if (regex_get_counter(regex_length_attempt_count, aut.get_regex_term()) >= m_params.m_RegexAutomata_LengthAttemptThreshold) { unsigned intersectionDifficulty = 0; // TODO EstimateIntersectionDifficulty if (intersectionDifficulty <= m_params.m_RegexAutomata_IntersectionDifficultyThreshold || regex_get_counter(regex_intersection_fail_count, aut.get_regex_term()) >= m_params.m_RegexAutomata_FailedIntersectionThreshold) { - lbool current_assignment = ctx.get_assignment(aut.get_regex_term()); + + 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 the assignment is consistent with our assumption, use the automaton directly; // otherwise, complement it (and save that automaton for next time) // TODO we should cache these intermediate results @@ -10013,7 +10025,12 @@ namespace smt { aut_inter = m_mk_aut.mk_product(aut_inter, aut.get_automaton()); } else { // need to complement first - NOT_IMPLEMENTED_YET(); + expr_ref rc(u.re.mk_complement(aut.get_regex_term()), m); + eautomaton * aut_c = m_mk_aut(rc); + 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); } used_intersect_constraints.push_back(aut); if (aut_inter->is_empty()) { @@ -10028,7 +10045,34 @@ namespace smt { TRACE("str", tout << "intersected " << used_intersect_constraints.size() << " constraints" << std::endl;); if (aut_inter != NULL && aut_inter->is_empty()) { TRACE("str", tout << "product automaton is empty; asserting conflict clause" << std::endl;); - NOT_IMPLEMENTED_YET(); + expr_ref_vector conflict_terms(m); + + for (svector::iterator aut_it = used_intersect_constraints.begin(); + aut_it != used_intersect_constraints.end(); ++aut_it) { + regex_automaton_under_assumptions aut = *aut_it; + 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) { + conflict_terms.push_back(str_in_re_term); + } else if (current_assignment == l_false) { + conflict_terms.push_back(m.mk_not(str_in_re_term)); + } + // add length assumptions, if any + rational ub; + if (aut.get_upper_bound(ub)) { + expr_ref ub_term(m_autil.mk_le(mk_strlen(str), m_autil.mk_numeral(ub, true)), m); + conflict_terms.push_back(ub_term); + } + rational lb; + if (aut.get_lower_bound(lb)) { + expr_ref lb_term(m_autil.mk_ge(mk_strlen(str), m_autil.mk_numeral(lb, true)), m); + conflict_terms.push_back(lb_term); + } + } + + expr_ref conflict_clause(m.mk_not(mk_and(conflict_terms)), m); + assert_axiom(conflict_clause); + regex_axiom_add = true; } } // foreach (entry in regex_terms_by_string) diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 86929d4d3..acab8e019 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -168,7 +168,7 @@ public: class regex_automaton_under_assumptions { protected: - expr * str_in_re; + expr * re_term; eautomaton * aut; bool polarity; @@ -179,11 +179,11 @@ protected: rational upper_bound; public: regex_automaton_under_assumptions() : - str_in_re(NULL), aut(NULL), polarity(false), + re_term(NULL), aut(NULL), polarity(false), assume_lower_bound(false), assume_upper_bound(false) {} - regex_automaton_under_assumptions(expr * str_in_re, eautomaton * aut, bool polarity) : - str_in_re(str_in_re), aut(aut), polarity(polarity), + regex_automaton_under_assumptions(expr * re_term, eautomaton * aut, bool polarity) : + re_term(re_term), aut(aut), polarity(polarity), assume_lower_bound(false), assume_upper_bound(false) {} void set_lower_bound(rational & lb) { @@ -221,7 +221,7 @@ public: } eautomaton * get_automaton() const { return aut; } - expr * get_regex_term() const { return str_in_re; } + expr * get_regex_term() const { return re_term; } bool get_polarity() const { return polarity; } virtual ~regex_automaton_under_assumptions() {