kdrag.theories.set.Finite

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