Documentation

Cvc.Spec.Set

Set specification #

Note the operand order of setMember and setInsert: cvc5 takes the element first and the set last. cvc5 marks setIsEmpty, setIsSingleton, setChoose and the higher-order operators experimental.

Higher-order operators #

Constants #

Built by a TermManager method rather than by applying a kind, so the sort-erased constructor takes the element sort, and the typed one reads it off its index.