mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-18 14:46:25 +00:00
Code Activity

add membership elimination to legacy elim_uncnstr pre-processor. Detect xor encodings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-14 15:05:25 -07:00
parent e05ebe8bef
commit 3a390dda18
2 changed files with 40 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/ast/rewriter/seq_rewriter.cpp
View file

@ -3314,11 +3314,20 @@ expr_ref seq_rewriter::mk_antimirov_deriv_restrict(expr* e, expr* d, expr* cond)
expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) {
expr_ref _r1(r1, m()), _r2(r2, m());
expr *a1, *b1, *a2, *b2;
SASSERT(m_util.is_re(r1));
SASSERT(m_util.is_re(r2));
expr_ref result(m());
std::function<bool(expr*, expr*&, expr*&)> test = [&](expr* t, expr*& a, expr*& b) { return re().is_union(t, a, b); };
std::function<expr* (expr*, expr*)> compose = [&](expr* r1, expr* r2) { return (is_subset(r1, r2) ? r2 : (is_subset(r2, r1) ? r1 : re().mk_union(r1, r2))); };
std::function<bool(expr *, expr *)> is_complement = [&](expr *a, expr *b) {
expr *s;
if (re().is_complement(a, s) && s == b)
return true;
if (re().is_complement(b, s) && s == a)
return true;
return false;
};
if (r1 == r2 || re().is_empty(r2) || re().is_full_seq(r1))
result = r1;
else if (re().is_empty(r1) || re().is_full_seq(r2))
@ -3327,6 +3336,15 @@ expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) {
result = r1;
else if (re().is_dot_plus(r2) && re().get_info(r1).min_length > 0)
result = r2;
// (R1 \ R2) U (R2 \ R1) = R1 xor R2
else if (re().is_intersection(r1, a1, a2) && re().is_intersection(r2, b1, b2) &&
is_complement(a1, b2) && is_complement(a2, b1)) {
result = re().mk_xor(a1, re().mk_complement(a2));
}
else if (re().is_intersection(r1, a1, a2) && re().is_intersection(r2, b1, b2) &&
is_complement(a1, b1) && is_complement(a2, b2)) {
result = re().mk_xor(a1, re().mk_complement(a2));
}
else
result = merge_regex_sets(r1, r2, re().mk_full_seq(r1->get_sort()), test, compose);
return result;

23
src/tactic/core/elim_uncnstr_tactic.cpp
View file

@ -19,6 +19,7 @@ Notes:
#include "tactic/tactical.h"
#include "ast/converters/generic_model_converter.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/rewriter/seq_rewriter.h"
#include "ast/arith_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
#include "ast/recfun_decl_plugin.h"
@ -803,10 +804,10 @@ class elim_uncnstr_tactic : public tactic {
// x ++ y -> z, x -> z, y -> eps
app * process_seq_app(func_decl * f, unsigned num, expr * const * args) {
app *r = nullptr;
switch (f->get_decl_kind()) {
case _OP_STRING_CONCAT:
case OP_SEQ_CONCAT: {
app * r = nullptr;
expr* x, *y;
if (uncnstr(args[0]) && num == 2 &&
args[1]->get_ref_count() == 1 &&
@ -833,6 +834,26 @@ class elim_uncnstr_tactic : public tactic {
return r;
}
case OP_SEQ_IN_RE:
if (uncnstr(args[0]) && m_seq_util.re.is_ground(args[1]) && m_seq_util.is_string(args[0]->get_sort())) {
zstring s1;
expr *re = args[1];
seq_rewriter rw(m());
if (l_true != rw.some_string_in_re(re, s1))
return nullptr;
zstring s2;
expr_ref not_re(m_seq_util.re.mk_complement(re), m());
if (l_true != rw.some_string_in_re(not_re, s2))
return nullptr;
mk_fresh_uncnstr_var_for(f, num, args, r);
expr_ref witness1 = expr_ref(m_seq_util.str.mk_string(s1), m());
expr_ref witness2 = expr_ref(m_seq_util.str.mk_string(s2), m());
if (m_mc)
add_def(args[0], m().mk_ite(r, witness1, witness2));
return r;
}
return nullptr;
default:
return nullptr;
}