Extractor to identify predicates that are domain predicates of some sort.
Create a new uninterpreted sort of infinite cardinality.
Create a new uninterpreted sort of finite or infinite cardinality.
(Since version ) see corresponding Javadoc for more information.