Z3: znajdowanie wszystkich satysfakcjonujących modeli

Question

Próbuję odzyskać wszystkie możliwe modele dla niektórych teorii pierwszego rzędu za pomocą Z3, solver SMT opracowany przez Microsoft Research. Oto minimalne przykład roboczych:

(declare-const f Bool) 
(assert (or (= f true) (= f false))) 

W tym przypadku zdań istnieją dwa satysfakcjonujące zadania: f->true i f->false. Ponieważ Z3 (i ogólnie solucje SMT) będą próbować znaleźć tylko jeden satysfakcjonujący model, znalezienie wszystkich rozwiązań nie będzie bezpośrednio możliwe. Here Znalazłem użyteczne polecenie o nazwie (next-sat), ale wygląda na to, że najnowsza wersja Z3 już tego nie obsługuje. To trochę niefortunne dla mnie i generalnie myślę, że polecenie jest całkiem użyteczne. Czy istnieje inny sposób robienia tego?

Answer 1

Jednym ze sposobów osiągnięcia tego jest użycie jednego z interfejsów API wraz z możliwością generowania modelu. Następnie można użyć wygenerowanego modelu z jednego testu sprawdzalności, aby dodać ograniczenia, aby zapobiec używaniu poprzednich wartości modelu w kolejnych kontrolach zgodności, dopóki nie będzie bardziej satysfakcjonujących zadań. Oczywiście, musisz używać sortowania skończonego (lub mieć pewne ograniczenia zapewniające to), ale możesz użyć tego z nieskończonymi sortami, jeśli nie chcesz znaleźć wszystkich możliwych modeli (np. Zatrzymaj się po wygenerowaniu wiązki) .

Oto przykład przy użyciu z3py (link do z3py skrypt: http://rise4fun.com/Z3Py/a6MC):

a = Int('a') 
b = Int('b') 

s = Solver() 
s.add(1 <= a) 
s.add(a <= 20) 
s.add(1 <= b) 
s.add(b <= 20) 
s.add(a >= 2*b) 

while s.check() == sat: 
    print s.model() 
    s.add(Or(a != s.model()[a], b != s.model()[b])) # prevent next model from using the same assignment as a previous model 

Generalnie, używając dysjunktywnej wszystkich zaangażowanych stałych powinien działać (np a i b tutaj). Wylicza wszystkie przypisania liczb całkowitych dla a i b (między 1 i 20) spełniające a >= 2b. Na przykład, jeśli mamy ograniczyć a i b leżeć między 1 i 5 Zamiast wyjście jest:

[b = 1, a = 2] 
[b = 2, a = 4] 
[b = 1, a = 3] 
[b = 2, a = 5] 
[b = 1, a = 4] 
[b = 1, a = 5]