Ошибка «неизвестного вида» в запросах с фиксированной точкой

Question

Я получаю сообщение об ошибке «неизвестного типа» при попытке задать запрос с фиксированной точкой, используя ключевое слово query. Например, следующий пример из точки учебник фиксированной, который прекрасно работает в онлайн-версии Z3,

(declare-rel mc (Int Int)) 
(declare-var n Int) 
(declare-var m Int) 
(declare-var p Int) 

(rule (=> (> m 100) (mc m (- m 10)))) 
(rule (=> (and (<= m 100) (mc (+ m 11) p) (mc p n)) (mc m n))) 

(query (and (mc m n) (< n 91)) 
:print-certificate true) 

возвращается:

(error "line 9 column 13: unknown sort 'mc'") 

, когда я запустить его из командной строки. Я использую Z3 версию 4.4.2, скомпилированную из репозитория github в Linux. Моя командная строка: z3 -smt2 example.smt

Есть ли какие-то флаговые компиляции, которые нужно настроить для включения этой функции?

Answer 1

Недавно я изменил формат «запроса», чтобы использовать только предикат. Урок должен быть обновлен.

(declare-rel q (Int Int)) 
(rule (=> (and (mc m n) (< n 91)) (q m n))) 
(query q :print-certificate true)