kdrag.theories.set.subset

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