Z3 C api: переменная типа многомерного массива вызывает неверный результат

вот контекст Z3:

    (forall ((X (Array Int (Array Int Real))) (i Int) (j Int))
     (let ((a!1 (* (- 1) (to_int (select (select X i) j)))))
        (= (+ (testArr X i j) a!1) 0))))

это означает:

forall X,i,j. testArr(X,i,j) == X[i][j]

теперь я пытаюсь доказать два похожих утверждения:

 1 (=> (= (select (select Z i1) j1) (select (select X i) j))
       (= (select (select Z i1) j1)  (testArr X i j)))

а также

 2 (=> (= v (select (select X i) j))
       (= v (to_real (testArr X i j))))

второе утверждение Z3 возвращает действительное значение, но первое утверждение Z3 возвращает неверное значение, а в другом примере Z3 иногда возвращает неизвестное значение. почему??


z3
person Lewis.Lee    schedule 02.03.2015    source источник
comment
Не могли бы вы добавить весь файл проблемы? Неясно, являются ли все необъявленные переменные (X, Z, i1, v) неколичественными или универсальными. Кроме того, есть ли определение testArr или вы просите Z3 придумать новое определение функции?   -  person Christoph Wintersteiger    schedule 02.03.2015
comment
Спасибо за вашу помощь. Я только что решил эту проблему. Причиной этой проблемы является несоответствие типов. Тип возвращаемого значения testArr — целочисленный, но тип X[i][j] — реальный, поэтому Z3 автоматически добавляет to_int или to_real. Когда я изменяю тип возвращаемого значения функции testArr на real.Z3 возвращает действительный.   -  person Lewis.Lee    schedule 02.03.2015
comment
Отлично, спасибо, что сообщили нам! По умолчанию Z3 действительно конвертирует целые и вещественные числа, что может сбивать с толку. См. также: stackoverflow.com/questions/26027628/   -  person Christoph Wintersteiger    schedule 02.03.2015