mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-17 20:45:45 +00:00
Code Activity

cleanup and add comments

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-07-02 19:32:09 -07:00
parent 2b4a473334
commit d43d61a4bf
2 changed files with 89 additions and 56 deletions
Download patch file Download diff file Expand all files Collapse all files

120
src/smt/seq_regex.cpp
View file

@ -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 <lit, split_set, in_re2 literals>
// 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 <lit, split_set, in_re2 literals>
// 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());

25
src/smt/seq_regex.h
View file

@ -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);