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")
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.)