Как Int сортировка (из теории Ints SMT-LIB 2.0) и динамически объявленные сортировки определены в z3? - PullRequest
Новая
       19

Как Int сортировка (из теории Ints SMT-LIB 2.0) и динамически объявленные сортировки определены в z3?

4 голосов
/ 17 ноября 2011

Вот тест SMT-LIB 2.0, который я выполнил с помощью z3: 

(set-logic AUFLIA)
(declare-sort PZ 0)
(declare-fun MS (Int PZ) Bool)

(assert (forall ((x Int)) (exists ((X PZ)) 
            (and (MS x X) 
                 (forall ((y Int)) (=> (MS y X) (= y x)))))))
(check-sat)

Я ожидал, что результат будет sat, по крайней мере с моделью, где PZ - это блок питания Z (целые числа) и MS - это предикат, который проверяет членство целого числа в подмножестве Z (элемент вида PZ).

Но z3 ответил unsat.

Не могли бы вы помочь мне понять этот результат, пожалуйста?В частности, как z3 интерпретирует сортировку Int?Это действительно считается бесконечным?А как насчет динамически объявленной сортировки (здесь сортировка PZ)?

1 Ответ

3 голосов
/ 17 ноября 2011

В Z3 Int бесконечно.Вы правы, результат должен быть sat.Результат unsat вызван ошибкой в ​​одном из модулей Z3.Я уже исправил ошибку.Один временный кеш в реализации не сбрасывался.Исправление будет доступно в следующем выпуске.Тем временем вы можете отключить модуль с ошибками, используя следующую команду в начале вашего скрипта.

(set-option :mbqi false)

Кстати, ошибка затрагивает только примеры, содержащие литералы вида (= x y), где x и y - универсальные переменные.

Кстати, хотя ваш пример выполним, Z3 не может построить модель для него (даже после исправления ошибки).На самом деле, после исправления ошибки, Z3 выдает ответ unknown.Средство поиска моделей (используется в Z3) способно находить только те модели, в которых интерпретация неинтерпретированных видов (таких как PZ) конечна.Это ограничение может измениться в будущем.

...