kdrag.theories.set

First class sets ArraySort(T, Bool)

Functions

`BigUnion`(A)	Big union of a set of sets.
`Choose`(A[, auto])	Choose an arbitrary element from set A.
`CountInter`(seq)	Countable intersection of a sequence of sets Int -> A -> Bool.
`EClass`(x, eqrel)	Equivalence class [x] under equivalence relation eqrel.
`FamilyUnion`(family)	Countable union of a sequence of sets Int -> A -> Bool.
`Finite`(A)	A set is finite if it has a finite number of elements.
`Injective`(f)	An injective function maps distinct inputs to distinct outputs.
`PowerSet`(A)	Power set of A : Set( Set(T) ) >>> IntSet = Set(smt.IntSort()) >>> A = Singleton(smt.IntVal(3)) >>> P = PowerSet(A) >>> kd.prove(member(IntSet.empty, P)) \|= Lambda(c!..., subset(c!..., Store(K(Int, False), 3, True)))[K(Int, False)]
`Quot`(dom, eqrel)	Quotient space under equivalence relation eqrel.
`Range`(f)	Range of a function.
`Set`(T)	Sets of elements of sort T.
`Singleton`(x)
`Surjective`(f)	A surjective function maps to every possible value in the range.
`bigunion`(T)	Abstracted bigunion
`complement`(A)	Complement of a set. >>> IntSet = Set(smt.IntSort()) >>> A = smt.Const("A", IntSet) >>> kd.prove(complement(complement(A)) == A) \|= complement(complement(A)) == A.
`diff`(A, B)	Set difference. >>> IntSet = Set(smt.IntSort()) >>> A = smt.Const("A", IntSet) >>> kd.prove(diff(A, A) == IntSet.empty) \|= setminus(A, A) == K(Int, False).
`inter`(A, B)
`is_set`(A)
`member`(x, A)
`subset`(A, B)
`union`(A, B)

kdrag.theories.set.BigUnion(A: ArrayRef) → ArrayRef

Big union of a set of sets. >>> IntSet = Set(smt.IntSort()) >>> A = smt.Const(“A”, Set(IntSet)) >>> BigUnion(A) Lambda(x, Exists(B, And(B[x], A[B])))

Parameters:: A (ArrayRef)
Return type:: ArrayRef

kdrag.theories.set.Choose(A: FuncRef, auto=False) → tuple[list[ExprRef], Proof]

Choose an arbitrary element from set A.

>>> x = smt.Int("x")
>>> Choose(smt.Lambda([x], x > 0))
([c!...], |= Implies(Exists(c!..., c!... > 0), c!... > 0))

Parameters:: A (FuncRef)
Return type:: tuple[list[ExprRef], Proof]

kdrag.theories.set.CountInter(seq: ArrayRef) → ArrayRef

Countable intersection of a sequence of sets Int -> A -> Bool.

>>> ISet = Set(smt.IntSort())
>>> i,j,k = smt.Ints("i j k")
>>> kd.prove(smt.ForAll([k], smt.Not(CountInter(smt.Lambda([i], smt.Lambda([j], i == j)))[k])))
|= ForAll(k,
       Not(Lambda(x!...,
                  ForAll(i!...,
                         Lambda(i, Lambda(j, i == j))[i!...][x!...]))[k]))

Parameters:: seq (ArrayRef)
Return type:: ArrayRef

kdrag.theories.set.EClass(x: ExprRef, eqrel) → QuantifierRef

Equivalence class [x] under equivalence relation eqrel. The set of all v such that eqrel(x, v) holds. https://en.wikipedia.org/wiki/Equivalence_class

>>> x,y = smt.Ints("x y")
>>> (A := EClass(x, lambda a,b: a % 3 == b % 3))
Lambda(v!..., x%3 == v!...%3)
>>> kd.prove(EClass(3, lambda a,b: a % 3 == b % 3)[3])
|= Lambda(v!..., 3%3 == v!...%3)[3]

Parameters:: x (ExprRef)
Return type:: QuantifierRef

kdrag.theories.set.FamilyUnion(family: ArrayRef) → ArrayRef

Countable union of a sequence of sets Int -> A -> Bool.

>>> ISet = Set(smt.IntSort())
>>> i,j,k = smt.Ints("i j k")
>>> kd.prove(smt.ForAll([k], FamilyUnion(smt.Lambda([i], smt.Lambda([j], i == j)))[k]))
    |= ForAll(k,
       Lambda(x!...,
              Exists(i!...,
                     Lambda(i, Lambda(j, i == j))[i!...][x!...]))[k])

Parameters:: family (ArrayRef)
Return type:: ArrayRef

kdrag.theories.set.Finite(A: ArrayRef) → BoolRef

A set is finite if it has a finite number of elements.

See https://cvc5.github.io/docs/cvc5-1.1.2/theories/sets-and-relations.html#finite-sets

>>> IntSet = Set(smt.IntSort())
>>> kd.prove(Finite(IntSet.empty))
|= Exists(finwit!...,
       ForAll(x!...,
              K(Int, False)[x!...] ==
              Contains(finwit!..., Unit(x!...))))

Parameters:: A (ArrayRef)
Return type:: BoolRef

kdrag.theories.set.Injective(f: FuncDeclRef) → BoolRef

An injective function maps distinct inputs to distinct outputs.

>>> x, y = smt.Ints("x y")
>>> neg = (-x).decl()
>>> kd.prove(Injective(neg))
|= ForAll([x!..., y!...],
       Implies(-x!... == -y!..., x!... == y!...))

Parameters:: f (FuncDeclRef)
Return type:: BoolRef

kdrag.theories.set.PowerSet(A: ArrayRef) → ArrayRef

Power set of A : Set( Set(T) ) >>> IntSet = Set(smt.IntSort()) >>> A = Singleton(smt.IntVal(3)) >>> P = PowerSet(A) >>> kd.prove(member(IntSet.empty, P)) |= Lambda(c!…, subset(c!…, Store(K(Int, False), 3, True)))[K(Int,

False)]

Parameters:: A (ArrayRef)
Return type:: ArrayRef

kdrag.theories.set.Quot(dom: SortRef, eqrel) → QuantifierRef

Quotient space under equivalence relation eqrel. A set of sets of A. The set of equivalence classes https://en.wikipedia.org/wiki/Equivalence_class

>>> x = smt.Int("x")
>>> l = kd.Lemma((smt.IntSort() // (lambda a,b: a % 3 == b % 3))[EClass(x, lambda a,b: a % 3 == b % 3)])
>>> l.simp().exists(x).auto()
Nothing to do. Hooray!
>>> _ = l.qed()

Parameters:: dom (SortRef)
Return type:: QuantifierRef

kdrag.theories.set.Range(f: FuncDeclRef) → ArrayRef

Range of a function. Also known as the Image of the function.

>>> f = smt.Function("f", smt.IntSort(), smt.IntSort())
>>> Range(f)
Lambda(y, Exists(x0, f(x0) == y))

Parameters:: f (FuncDeclRef)
Return type:: ArrayRef

kdrag.theories.set.Set(T)

Sets of elements of sort T. This registers a number of helper notations and useful lemmas.

>>> IntSet = Set(smt.IntSort())
>>> IntSet.empty
K(Int, False)
>>> IntSet.full
K(Int, True)
>>> A,B = smt.Consts("A B", IntSet)
>>> A & B
intersection(A, B)
>>> A | B
union(A, B)
>>> A - B
setminus(A, B)
>>> A <= B
subset(A, B)
>>> A < B
And(subset(A, B), A != B)
>>> A >= B
subset(B, A)
>>> IntSet.union_comm
|= ForAll([A, B], union(A, B) == union(B, A))

kdrag.theories.set.Singleton(x: ExprRef) → ArrayRef

>>> x = smt.Int("x")
>>> kd.prove(Singleton(smt.IntVal(3))[3])
|= Store(K(Int, False), 3, True)[3]
>>> kd.prove(smt.Not(Singleton(smt.IntVal(3))[4]))
|= Not(Store(K(Int, False), 3, True)[4])

Parameters:: x (ExprRef)
Return type:: ArrayRef

kdrag.theories.set.Surjective(f: FuncDeclRef) → BoolRef

A surjective function maps to every possible value in the range.

>>> x = smt.Int("x")
>>> neg = (-x).decl()
>>> kd.prove(Surjective(neg))
|= ForAll(y!..., Lambda(y, Exists(x0, -x0 == y))[y!...])

Parameters:: f (FuncDeclRef)
Return type:: BoolRef

kdrag.theories.set.bigunion(T: SortRef) → FuncDeclRef

Abstracted bigunion

Parameters:: T (SortRef)
Return type:: FuncDeclRef

kdrag.theories.set.complement(A: ArrayRef) → ArrayRef

Complement of a set. >>> IntSet = Set(smt.IntSort()) >>> A = smt.Const(“A”, IntSet) >>> kd.prove(complement(complement(A)) == A) |= complement(complement(A)) == A

Parameters:: A (ArrayRef)
Return type:: ArrayRef

kdrag.theories.set.diff(A: ArrayRef, B: ArrayRef) → ArrayRef

Set difference. >>> IntSet = Set(smt.IntSort()) >>> A = smt.Const(“A”, IntSet) >>> kd.prove(diff(A, A) == IntSet.empty) |= setminus(A, A) == K(Int, False)

Parameters:

A (ArrayRef)
B (ArrayRef)

Return type:

ArrayRef

kdrag.theories.set.inter(A: ArrayRef, B: ArrayRef) → ArrayRef

Parameters:

A (ArrayRef)
B (ArrayRef)

Return type:

ArrayRef

kdrag.theories.set.is_set(A: ArrayRef) → bool

Parameters:: A (ArrayRef)
Return type:: bool

kdrag.theories.set.member(x: ExprRef, A: ArrayRef) → BoolRef

>>> x = smt.Int("x")
>>> A = smt.Const("A", Set(smt.IntSort()))
>>> member(x, A)
A[x]

Parameters:

x (ExprRef)
A (ArrayRef)

Return type:

BoolRef

kdrag.theories.set.subset(A: ArrayRef, B: ArrayRef) → BoolRef

>>> IntSet = Set(smt.IntSort())
>>> A = smt.Const("A", IntSet)
>>> kd.prove(subset(IntSet.empty, A))
|= subset(K(Int, False), A)
>>> kd.prove(subset(A, A))
|= subset(A, A)
>>> kd.prove(subset(A, IntSet.full))
|= subset(A, K(Int, True))

Parameters:

A (ArrayRef)
B (ArrayRef)

Return type:

BoolRef

kdrag.theories.set.union(A: ArrayRef, B: ArrayRef) → ArrayRef

Parameters:

A (ArrayRef)
B (ArrayRef)

Return type:

ArrayRef