Z3 Forall z tablicą

Question

Z3 dostarcza nieznanego prostego problemu:

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

Odkryłem, że staje się sat, jeśli zaprzecza forall, ale wydaje się, że jest to szczególnie prosta rzecz, której nie można rozwiązać.

To powoduje problemy, ponieważ klasa problemów, które chcę rozwiązać, jest bardziej podobna do:

(declare-fun u () Int)
(assert
 (forall ((y (Array Int Int)) )
     (=> 
        (= u 0) (<= (select y 1) 0))
 )
)
(check-sat)

Gdzie samo zanegowanie forall nie jest tym samym problemem, więc nie można tego zrobić tutaj. Czy jest jakiś sposób, aby przedstawić ten problem Z3, aby uzyskać wynik un / sat?

Answer 1

Problemy z kwantyfikatorami są zawsze problematyczne w rozwiązaniach SMT, szczególnie jeśli dotyczą one tablic i naprzemiennych kwantyfikatorów, jak w twoim przykładzie. Zasadniczo masz exits u. forall y. P(u, y). Z3 lub jakikolwiek inny solver SMT będzie miał trudności z rozwiązywaniem tego rodzaju problemów.

Kiedy masz stwierdzenie wyrażone ilościowo, tak jak robisz to forallna najwyższym poziomie lub zagnieżdżonym exists, logika staje się pół-rozstrzygalna. Z3 używa MBQI (instancji kwantyfikatora opartego na modelu) do heurystycznego rozwiązywania takich problemów, ale najczęściej to zawodzi. Problem nie polega tylko na tym, że z3 nie jest w stanie: nie ma procedury decyzyjnej dla takich problemów, a z3 robi wszystko, co w jego mocy.

Możesz spróbować podać wzorce kwantyfikatorów dla takich problemów, aby pomóc z3, ale nie widzę łatwego sposobu na zastosowanie tego w twoim problemie. (Wzorce kwantyfikatorów mają zastosowanie, gdy masz niezinterpretowane funkcje i kwantyfikowane aksjomaty. Zobaczhttps://rise4fun.com/z3/tutorialcontent/guide#h28). Więc nie sądzę, że to zadziała. Nawet jeśli tak, wzorce są bardzo skomplikowane w programowaniu i nie są odporne na zmiany w specyfikacji, które w przeciwnym razie mogłyby wyglądać nieszkodliwie.

Jeśli masz do czynienia z takimi kwantyfikatorami, solwery SMT prawdopodobnie nie są dobrze dopasowane. Przyjrzyj się półautomatycznym dowodom twierdzeń, takim jak Lean, Isabelle, Coq itp., Które mają na celu radzenie sobie z kwantyfikatorami w znacznie bardziej zdyscyplinowany sposób. Oczywiście tracisz pełną automatyzację, ale większość z tych narzędzi może używać solwera SMT do realizacji celów cząstkowych, które są wystarczająco „łatwe”. W ten sposób nadal wykonujesz „ciężkie podnoszenie” ręcznie, ale większość celów pośrednich jest automatycznie obsługiwana przez z3. (Szczególnie w przypadku Lean, patrz tutaj:https://leanprover.github.io/)

Answer 2

Jest jeden dodatkowy (prawy) nawias zamykający, który należy usunąć. Dodaj także assert przed instrukcją forall.

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

Uruchom powyższy kod, a jako odpowiedź powinieneś otrzymać unsat.

W przypadku drugiego programu odpowiedź aliasu może być przydatna.