solversmtcvc4cvc5

SMT-LIB Error ((error "Parse Error: output.smt:37.36: Symbol '->' not declared as a type"))

I am coding in SMT-LIB langage and I am using -> but I got an error that is not defined :

(define-sort |? Z| () (-> |Z| Bool)) 
(declare-const |set.intent Z| (-> |? Z| |POW Z|)) 
(assert (! (forall ((p |? Z|)) (forall ((x |Z|)) (= (|set.in Z| x (|set.intent Z| p)) (p x) ) ) ) :named |set.in.intent Z|))

I got the error

Parse Error: output.smt:37.36: Symbol '->' not declared as a type

Solution

  • -> as a type is a fairly new feature in SMTLib. To make it work with CVC5, you need to explicitly tell it to use higher-order logic. (Z3 doesn't require this.) So, add the following to the top of your file:

    (set-logic HO_ALL)

    Since you didn't include enough of your program for us to effectively test this, I had to add a few extra declarations:

    (set-logic HO_ALL)
(declare-sort |Z| 0)
(declare-sort |POW Z| 0)
(define-sort |? Z| () (-> |Z| Bool))
(declare-const |set.intent Z| (-> |? Z| |POW Z|))
(declare-const |set.in Z| (-> |Z| |POW Z| Bool))
(assert (! (forall ((p |? Z|)) (forall ((x |Z|)) (= (|set.in Z| x (|set.intent Z| p)) (p x) ) ) ) :named |set.in.intent Z|))

    This loads cleanly with CVC5.