diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index be7564126..497000d46 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -127,7 +127,6 @@ namespace smt { return; } - if (is_string_equality(lit)) { TRACE(seq_regex, tout << "simplified regex using string equality" << std::endl;); @@ -135,60 +134,10 @@ namespace smt { return; } - // TODO - replace this with a propagator closure that gets invoked and removed on backtracking. - // it tracks - // an in_re2 literal is of the form in_re2(u, R1, v, R2) - // Assert in_re2(u, R1, v, R2) => u in R1 and v in R2 - // forward on split_set until there is a new in_re2 literal that is not already false. - // If there was an already created in_re2 literal that is true, - // then check that the propagation axiom is true - // if it isn't true, then assert it. - // if it is true, we are done - // If split_set is done and all in_re2 literals are false, there is a conflict. - // Assert the conflict clause lit => (or in_re2 literals) - // Final check also unfolds this axiomatization - // (we have to add a final check to seq_regex for this). - - if (th.get_fparams().m_seq_regex_factorization_enabled) { - unsigned threshold = th.get_fparams().m_seq_regex_factorization_threshold; - expr_ref_vector prefix(m); - expr *hd, *tl, *v; - auto filter = [&](expr* p, expr* _q) -> bool { - expr_ref q(_q, m); - for (expr* v : prefix) { - q = seq_rw().mk_derivative(v, q); - if (re().is_empty(q)) - return false; - } - return re().is_empty(q); - }; - - split_set result(seq_rw(), r, threshold, filter); - - auto [head, tail] = result.try_split_sequence(s); - if (head && tail) { - tl = tail; - while (str().is_concat(tl, hd, tl) && str().is_unit(hd, v) && m.is_value(v)) { - prefix.push_back(v); - } - - // propagate all cases - expr_ref_vector cases(m); - expr_ref_vector branches(m); - for (auto [pre, post] : result) { - expr_ref mem_head(re().mk_in_re(head, pre), m); - expr_ref mem_tail(re().mk_in_re(tail, post), m); - cases.push_back(m.mk_and(mem_head, mem_tail)); - } - if (!result.failed()) { - const expr_ref cases_expr(m.mk_or(cases), m); - ctx.internalize(cases_expr, false); - th.propagate_lit(nullptr, 1, &lit, ctx.get_literal(cases_expr)); - return; - } - } - // fallthrough; decomposition failed - } + if (factor_membership(lit)) { + TRACE(seq_regex, tout << "factor membership\n"); + return; + } // Convert a non-ground sequence into an additional regex and // strengthen the original regex constraint into an intersection @@ -216,7 +165,6 @@ namespace smt { TRACE(seq, tout << "propagate " << acc << "\n";); - //th.propagate_lit(nullptr, 1, &lit, acc_lit); th.add_axiom(~lit, acc_lit); } @@ -419,6 +367,66 @@ namespace smt { true); } + bool seq_regex::factor_membership(literal lit) { + expr *s = nullptr, *r = nullptr; + expr *e = ctx.bool_var2expr(lit.var()); + VERIFY(str().is_in_re(e, s, r)); + // TODO - replace this with a propagator closure that gets invoked and removed on backtracking. + // it tracks + // an in_re2 literal is of the form in_re2(u, R1, v, R2) + // Assert in_re2(u, R1, v, R2) => u in R1 and v in R2 + // forward on split_set until there is a new in_re2 literal that is not already false. + // If there was an already created in_re2 literal that is true, + // then check that the propagation axiom is true + // if it isn't true, then assert it. + // if it is true, we are done + // If split_set is done and all in_re2 literals are false, there is a conflict. + // Assert the conflict clause lit => (or in_re2 literals) + // Final check also unfolds this axiomatization + // (we have to add a final check to seq_regex for this). + + if (!th.get_fparams().m_seq_regex_factorization_enabled) + return false; + + unsigned threshold = th.get_fparams().m_seq_regex_factorization_threshold; + expr_ref_vector prefix(m); + expr *hd, *tl, *v; + auto filter = [&](expr *p, expr *_q) -> bool { + expr_ref q(_q, m); + for (expr *v : prefix) { + q = seq_rw().mk_derivative(v, q); + if (re().is_empty(q)) + return false; + } + return re().is_empty(q); + }; + + split_set result(seq_rw(), r, threshold, filter); + + auto [head, tail] = result.try_split_sequence(s); + if (head && tail) { + tl = tail; + while (str().is_concat(tl, hd, tl) && str().is_unit(hd, v) && m.is_value(v)) + prefix.push_back(v); + + // propagate all cases + expr_ref_vector cases(m); + expr_ref_vector branches(m); + for (auto [pre, post] : result) { + expr_ref mem_head(re().mk_in_re(head, pre), m); + expr_ref mem_tail(re().mk_in_re(tail, post), m); + cases.push_back(m.mk_and(mem_head, mem_tail)); + } + if (!result.failed()) { + const expr_ref cases_expr(m.mk_or(cases), m); + ctx.internalize(cases_expr, false); + th.propagate_lit(nullptr, 1, &lit, ctx.get_literal(cases_expr)); + return true; + } + } + return false; + } + bool seq_regex::unfold_prefix(literal lit) { expr *s = nullptr, *r = nullptr; expr *e = ctx.bool_var2expr(lit.var()); diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index ff7b601b4..376c19a50 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -21,6 +21,7 @@ Author: #include "ast/seq_decl_plugin.h" #include "ast/rewriter/seq_rewriter.h" #include "ast/rewriter/seq_skolem.h" +#include "ast/rewriter/seq_split.h" #include "smt/smt_context.h" /* @@ -91,6 +92,28 @@ Author: namespace smt { class theory_seq; + class seq_regex; + + // a split continuation is a closure that contains a split set + // and in_re2 literals that were extracted from a partial split. + // there are the following outcomes: + // 1. it was not possible to split:failed() + // 2. one of the in_re2 literals is true: in_re2(u, r1, v, r2) and in_re(u, r1), in_re(v, r2) are true + // 3. one of in_re2(u, r1, v, r2) is true: but in_re(u, r1) or in_re(v, r2) is undef or false. + // 4. all in_re2(u, r1, v, r2) are false: there is a next split from m_split -> add propagation axioms and set phase of in_re2. + // 5. all in_re2(u, r1, v, r2) are false: there is no next split from m_split -> conflict + // split continuations are assigned at scope level and map propagation literal lit to a split continuation. + // they are checked during propagation and during final check. + class split_cont { + split_set m_split; + expr_ref_vector m_in_re2; + public: + split_cont(seq_regex &r, literal lit); + bool failed() const; + bool is_sat(); + bool is_unsat(); + literal next_split(); + }; class seq_regex { // Data about a constraint of the form (str.in_re s R) @@ -153,6 +176,8 @@ namespace smt { bool unfold_prefix(literal lit); + bool factor_membership(literal lit); + expr_ref mk_first(expr* r, expr* n); bool is_member(expr* r, expr* u);