mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-26 10:28:48 +00:00
Code Activity

enable distribution of union over intersection

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-23 12:56:23 -07:00
parent f2e6d05c56
commit d77fe0b0cd
1 changed files with 16 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/ast/rewriter/seq_derive.cpp
View file

@ -753,13 +753,22 @@ namespace seq {
// TODO: Distribution of intersection over union
// Disabled pending performance analysis
// expr *u1, *u2;
// if (re().is_union(a, u1, u2))
// return mk_union(mk_inter(u1, b), mk_inter(u2, b));
// if (re().is_union(b, u1, u2))
// return mk_union(mk_inter(a, u1), mk_inter(a, u2));
// Distribution of intersection over union: (x ∪ y) ∩ b → (x ∩ b) ∪ (y ∩ b).
// This is essential for keeping the symbolic derivative a proper
// *transition regex*: with antimirov derivatives the operands of an
// intersection are unions of ITE-branches. If the intersection is left
// *above* the union/ITE structure, the solver's get_derivative_targets
// (which only descends through top-level ITE and union, not
// intersection) cannot decompose the transition regex into ground
// target states. The result is a handful of gigantic states still
// carrying the (:var 0) character conditions, on which the solver's
// cofactor/accept enumeration explodes. Distributing here pushes the
// intersection into the ITE leaves so states stay small and ground.
expr *u1 = nullptr, *u2 = nullptr;
if (re().is_union(a, u1, u2))
return mk_union(mk_inter(u1, b), mk_inter(u2, b));
if (re().is_union(b, u1, u2))
return mk_union(mk_inter(a, u1), mk_inter(a, u2));
// Base case: build raw intersection
return m_re.mk_inter(a, b);