z3 с квантификаторами и массивами, а также соответствующий код C для Seahorn

Приведенная ниже программа возвращает unsat при запуске на z3.

(assert ( forall ( (y (Array Int Int)) ) 
   (= (select y 1) 0) 
))
(check-sat)

Я не понимаю, что на самом деле означает строка forall; Значит ли это, что для всех массивов - Int y [Int], есть ли возможность y[1] == 0 ? Если да, то SAT, иначе UNSAT? Почему z3 возвращает unsat, когда я запускаю приведенный выше код?

Вот код C, который я написал для Seahorn, соответствующий вышеуказанному файлу smt2.

#include "seahorn/seahorn.h"
extern int nd();

int main(void){

int n = nd();

assume(n>0);

int y[n]; 

for(int i = 0; i < n; i++)
{
    sassert(y[1]=0);        
}

}

Я преобразовал код C в файл smt2 с помощью Seahorn, а затем отформатировал его с помощью format.py из CHC Comp 2020, а затем запустил z3 в отформатированном файле, который дает - unsat.

Хотя ответ обоих файлов одинаков, я не думаю, что это правильный код. В исходном файле smt2 указано Forall array y, тогда как мой код c говорит, что для всех элементов массива y. Как мне написать правильный код C для этой проблемы?

[Обратите внимание: я ссылался на учебник z3, но все равно не ясно]


arrays z3 smt quantifiers
person user8616916    schedule 31.08.2020    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Смысл этого утверждения:

(assert ( forall ( (y (Array Int Int)) ) 
   (= (select y 1) 0) 
))

есть: для всех массивов y, проиндексированных целыми числами и содержащих целые числа, элемент в позиции 1 всегда равен 0.

И ясно, что это неудовлетворительно. Есть много массивов, в которых элемент в позиции 1 не равен 0, поэтому ваше количественное утверждение терпит неудачу, и вы получаете unsat в качестве ответа.

Обратите внимание, что любая универсальная квантифицированная аксиома для массивов обречена быть невыполнимой, если она не утверждает что-то тривиальное: какое свойство вы можете написать, которое верно для всех таких массивов? Их не так много.

Трудно догадаться, что вы пытаетесь сделать, но в целом вы хотите сказать: У меня есть массив, и я знаю, что его первый элемент равен 0. В этом случае используйте экзистенциальный. Любая переменная, объявленная на верхнем уровне в запросе SMTLib, считается экзистенциальной. Нравится:

(declare-fun A () (Array Int Int))

; assert first element of `A` is `0`
(assert (= (select A 1) 0))

; .. now add other constraints, etc.

Этот подход, по сути, говорит z3 рассматривать все массивы A так, чтобы они имели 0 в своей 1-й позиции; и является типичным для задач проверки программного обеспечения. (Где это ограничение будет связано с частью инициализации вашей программы.)

person alias    schedule 31.08.2020
comment
Спасибо за ответ. Я прочитал этот вопрос, stackoverflow.com/questions/63604436 /z3-forall-with-array/, недавно, и я получил там же программу smt2. У вас есть идея, как представить эту программу smt2 на языке C? смысл.. представляющий для всех массивов в C..? - person user8616916; 31.08.2020
comment
Вы можете использовать C API z3, который позволяет создавать foralls. См. здесь: z3prover.github.io/api/html/ - person alias; 01.09.2020
comment
Хорошо, спасибо.. но меня особенно интересовала программа c, для морского рога. Поскольку для Seahorn пока нет тега, в stackoverflow я не смог добавить этот тег. Пожалуйста, рассмотрите возможность добавления этого тега. Спасибо! - person user8616916; 01.09.2020
comment
Я не мог добавить новый тег, так как для того, чтобы сделать то же самое, пользователь должен иметь более 1500 баллов. - person user8616916; 01.09.2020
comment
Я создал для вас тег морского рога, хотя вполне вероятно, что у переполнения стека нет значительного сообщества, которое наблюдает за этим тегом. Вы можете увеличить пробег, напрямую связавшись с ними на их собственном веб-сайте или подобном. - person alias; 01.09.2020