Unexpected `Unknown' result in theory with finite set

I want to show satisfiability of a simple vehicle configuration problem, in which any vehicle must have one wheel.

Here is the encoding:

(set-logic ALL)
(set-option :produce-models true)
(declare-sort Vehicle 0) ; type Vehicle


(declare-sort Wheel 0) ; type Wheel
(declare-fun wheels (Vehicle) (Set Wheel)); wheels: Vehicle -> Set(Wheels)

; number of wheels per vehicle
(assert (forall ((v Vehicle)) (= (card (wheels v)) 1)))

(check-sat)
(get-model)

I ran it with CVC4 online, and got this:

unknown
(
; cardinality of Vehicle is 1
; cardinality of Wheel is 1
(define-fun wheels ((BOUND_VARIABLE_349 Vehicle)) (Set Wheel) (as emptyset (Set Wheel)))
)

I would expect it to be satisfiable, with 1 vehicle having a set of 1 wheel. Does it fail because the types are open ? I tried with enumerated types without success.

Trying with CVC5 online results in this:

(error "Parse Error: /code.txt:10.50: Symbol 'card' not declared as a variable")

Solution

For CVC5; use set.card instead of card.

In either case, CVC will not be able to answer your query, because mixing quantifiers makes the logic semi-decidable. Note that when quantifiers are present, you can describe infinite sets; which takes the logic to the semi-decidable fragment. So, don't expect CVC to be able to answer your queries about sets when you use quantifiers.

(See https://cvc5.github.io/docs/cvc5-1.0.2/theories/sets-and-relations.html for an example how quantifiers allow you to specify infinite sets.)