Finite Sets

from z3 import *

# Note: FiniteSet support may vary by Z3 version/binding
# This documents the C API

# Finite set of integers
IntFiniteSet = FiniteSetSort(IntSort())
S = Const('S', IntFiniteSet)

# Finite set of bit-vectors
BVFiniteSet = FiniteSetSort(BitVecSort(8))
T = Const('T', BVFiniteSet)

IntFiniteSet = FiniteSetSort(IntSort())
empty = EmptyFiniteSet(IntFiniteSet)

solve(Size(empty) == 0)
# sat

x = Int('x')
singleton = SingletonFiniteSet(x)

solve(x == 42, Size(singleton) == 1)
# sat

low = Int('low')
high = Int('high')
range_set = FiniteSetRange(low, high)

solve(
    low == 1,
    high == 10,
    Size(range_set) == 10
)
# [low = 1, high = 10, |range_set| = 10]

S = Const('S', FiniteSetSort(IntSort()))
T = Const('T', FiniteSetSort(IntSort()))

union_set = FiniteSetUnion(S, T)

x = Int('x')
solve(
    IsMemberFiniteSet(x, S),
    Not(IsMemberFiniteSet(x, T)),
    IsMemberFiniteSet(x, union_set)
)
# sat - x is in S, so it's in the union

intersect_set = FiniteSetIntersect(S, T)

solve(
    Size(intersect_set) > 0,
    Size(S) == 5,
    Size(T) == 5
)
# Sets have at least one element in common

diff_set = FiniteSetDifference(S, T)

solve(
    Size(S) == 10,
    Size(T) == 3,
    Size(diff_set) == 7
)
# All elements of T are in S

S = Const('S', FiniteSetSort(IntSort()))
x = Int('x')

solve(
    IsMemberFiniteSet(x, S),
    x == 42,
    Size(S) == 1
)
# [S = {42}, x = 42]

S = Const('S', FiniteSetSort(IntSort()))
T = Const('T', FiniteSetSort(IntSort()))

solve(
    IsSubsetFiniteSet(S, T),
    Size(S) == 3,
    Size(T) == 5,
    Not(S == T)
)
# S ⊆ T and S ≠ T

S = Const('S', FiniteSetSort(IntSort()))
size = Int('size')

solve(
    size == FiniteSetSize(S),
    size >= 1,
    size <= 10
)
# S has between 1 and 10 elements

S = Const('S', FiniteSetSort(IntSort()))
T = Const('T', FiniteSetSort(IntSort()))
U = FiniteSetUnion(S, T)

solve(
    Size(S) == 5,
    Size(T) == 3,
    Size(FiniteSetIntersect(S, T)) == 2,
    Size(U) == 6  # |S ∪ T| = |S| + |T| - |S ∩ T|
)
# sat

S = Const('S', FiniteSetSort(IntSort()))
f = Function('f', IntSort(), IntSort())

# Map f over S: {f(x) | x ∈ S}
mapped_set = FiniteSetMap(f, S)

solve(
    Size(S) == 3,
    Size(mapped_set) <= 3  # May be smaller if f is not injective
)

S = Const('S', FiniteSetSort(IntSort()))
p = Function('p', IntSort(), BoolSort())

# Filter S by predicate: {x ∈ S | p(x)}
filtered_set = FiniteSetFilter(p, S)

solve(
    Size(S) == 10,
    Size(filtered_set) == 5
)
# Half the elements satisfy the predicate

from z3 import *

# Simplified set cover using finite sets
# Universe of elements: {1, 2, 3, 4, 5}
# Available sets: S1={1,2}, S2={2,3}, S3={3,4}, S4={4,5}
# Find minimum number of sets to cover all elements

universe = FiniteSetRange(IntVal(1), IntVal(5))

# Decision variables: include each set or not
use_s1 = Bool('use_s1')
use_s2 = Bool('use_s2')
use_s3 = Bool('use_s3')
use_s4 = Bool('use_s4')

# Build the covering based on selections
covering = EmptyFiniteSet(FiniteSetSort(IntSort()))
# Add sets conditionally (pseudocode - actual encoding more complex)

# Minimize number of sets used
cost = If(use_s1, 1, 0) + If(use_s2, 1, 0) + If(use_s3, 1, 0) + If(use_s4, 1, 0)

solve(
    IsSubsetFiniteSet(universe, covering),  # All elements covered
    cost <= 3  # Use at most 3 sets
)

from z3 import *

# Partition a set into two subsets with equal sum
original = FiniteSetRange(IntVal(1), IntVal(10))
S1 = Const('S1', FiniteSetSort(IntSort()))
S2 = Const('S2', FiniteSetSort(IntSort()))

solve(
    # S1 and S2 partition the original set
    FiniteSetUnion(S1, S2) == original,
    Size(FiniteSetIntersect(S1, S2)) == 0,  # Disjoint
    
    # Equal sums (would need sum function)
    Size(S1) == Size(S2)  # At least equal sizes
)

from z3 import *

# Color nodes such that no edge connects same-colored nodes
# Graph represented as adjacency

Color = DeclareSort('Color')
Node = DeclareSort('Node')

red = Const('red', Color)
blue = Const('blue', Color)
green = Const('green', Color)

# Sets of nodes for each color
red_nodes = Const('red_nodes', FiniteSetSort(Node))
blue_nodes = Const('blue_nodes', FiniteSetSort(Node))
green_nodes = Const('green_nodes', FiniteSetSort(Node))

# All nodes colored
all_nodes = Const('all_nodes', FiniteSetSort(Node))

solve(
    # Partition nodes by color
    FiniteSetUnion(red_nodes, FiniteSetUnion(blue_nodes, green_nodes)) == all_nodes,
    
    # Colors are disjoint
    Size(FiniteSetIntersect(red_nodes, blue_nodes)) == 0,
    Size(FiniteSetIntersect(red_nodes, green_nodes)) == 0,
    Size(FiniteSetIntersect(blue_nodes, green_nodes)) == 0
    
    # Add edge constraints here
)

from z3 import *

# Select exactly k elements from a set
elements = FiniteSetRange(IntVal(1), IntVal(10))
selection = Const('selection', FiniteSetSort(IntSort()))
k = Int('k')

solve(
    IsSubsetFiniteSet(selection, elements),
    Size(selection) == k,
    k == 5,
    # Additional constraints on selected elements
    ForAll([x], 
        Implies(
            IsMemberFiniteSet(x, selection),
            x > 3  # Only select elements > 3
        )
    )
)

from z3 import *

# Prove: |A ∪ B| = |A| + |B| - |A ∩ B|
A = Const('A', FiniteSetSort(IntSort()))
B = Const('B', FiniteSetSort(IntSort()))

solve(
    Size(FiniteSetUnion(A, B)) != 
    Size(A) + Size(B) - Size(FiniteSetIntersect(A, B))
)
# unsat - the formula is a tautology

from z3 import *

# All elements in a set satisfy a property
S = Const('S', FiniteSetSort(IntSort()))

# Every element in S is even
solve(
    Size(S) > 0,
    ForAll([x], 
        Implies(
            IsMemberFiniteSet(x, S),
            x % 2 == 0
        )
    ),
    IsMemberFiniteSet(IntVal(3), S)  # Contradiction
)
# unsat - cannot have odd number in set of evens