Заявить-весело и определить-весело в Z3 не может работать вместе?

Question

Мне нужно смоделировать длину массива. Поэтому я объявляю функцию

(declare-fun LEN ((Array Int Int)) Int)

В то же время я хочу определить некоторые макросы, используя define-fun,

Однако, как я немного протестировал на Z3, кажется, что define-fun а также declare-fun не может существовать в том же исходном файле?

Этот код вроде следующего работает нормально:

(define-fun mymax ((a Int) (b Int)) Int
  (ite (> a b) a b))

(assert (= (mymax 100 7) 100))
(check-sat)

(источник: http://rise4fun.com/Z3/jRzs)

Но следующее, независимо от того, где LEN вставлен, будут ошибки:

;(declare-fun LEN ((Array Int Int) Int) 
;unknown sort 'assert'  
(define-fun mymax ((a Int) (b Int)) Int
  (ite (> a b) a b))
; (declare-fun LEN ((Array Int Int) Int) 
;unknown sort 'assert'
(assert (= (mymax 4 7) 7))
; (declare-fun LEN ((Array Int Int) Int) 
;;unknown sort 'check-assert'
(check-sat)
;(declare-fun LEN ((Array Int Int) Int) 
 ;invalid sort, symbol, '_' or '(' expected

(источник: http://rise4fun.com/Z3/HdEy)

Кто-нибудь знает, как обойти это?

Answer 1

declare-fun а также define-fun можно использовать вместе. Проблема в том, что у вас пропущена скобка. Так должно быть

(declare-fun LEN ((Array Int Int)) Int) 

вместо

(declare-fun LEN ((Array Int Int) Int) 

Из-за отсутствия круглых скобок второй фактически объявляет функцию LEN с двумя аргументами (массив и целое число), тогда Z3 генерирует ошибку, когда он может найти результирующую сортировку для этого объявления.

Вот ссылка на полный пример: http://rise4fun.com/Z3/TjNS