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] е real, така че Z3 автоматично добавя към_int или към_real. Когато променя типа на връщане на функцията testArr на real.Z3 връща валидно.   -  person Lewis.Lee    schedule 02.03.2015
comment
Страхотно, благодаря, че ни съобщи! По подразбиране Z3 наистина ще конвертира между int и reals, което може да бъде объркващо. Вижте също: stackoverflow.com/questions/26027628/   -  person Christoph Wintersteiger    schedule 02.03.2015