Czy Z3 może być używany do wstępnego przetwarzania problemów?

Question

Prowadzenie nowych badań nad rozwiązaniami SMT jest wielokrotnie utrudnione przez fakt, że dostępne problemy wymagają wielu sztuczek i technik przetwarzania wstępnego, które nie są bezpośrednio związane z procedurami decyzyjnymi. Często są one niepublikowane lub wymagają czasu, aby odpowiednio zaimplementować i zoptymalizować, a ponadto utrudniają porównywanie i zrozumienie różnych rozwiązań.

Czy możliwe jest użycie Z3 jako preprocesora, który może zająć problem i zrzucić go w formie wstępnie przetworzonej (takiej, która sama z3 używa do rozwiązania problemu)?

Nie widzę żadnych opcji wiersza poleceń, ale domyślam się, że może być jakiś sposób, aby to osiągnąć, poprzez strategie, interfejs Pythona lub nawet napisanie jakiegoś dodatkowego kodu.

Answer 1

Tak, Z3 może być używany jako pre-procesor. Polecenie apply pozwala użytkownikowi zastosować taktykę i zrzucić ją jako benchmark SMT 2.0. Oto przykład (również dostępny w Internecie na http://rise4fun.com/Z3/eutO):

(declare-const x Real) 
(declare-const y Real) 

(assert (forall ((n Real)) (or (< x n) (< n y)))) 
(assert (= (< x y) (< x 100.0))) 

(apply (then qe nnf) :print false :print-benchmark true) 

W powyższym przykładzie, QE (eliminacja kwantyfikator) i NNF (negacja-normal-form) taktyka są stosowane do problemu wejściowego.

Niektóre dodatkowe punkty:

• Kilka taktyka produkować tylko equisatisfiable wyników. W związku z tym model wynikowego testu porównawczego niekoniecznie jest modelem pierwotnej formuły. Możemy poprosić Z3, aby zrzucił powiązany "model-konwerter" (opcja :print-model-converter true). Konwerter modelu koduje kroki używane przez Z3 do konwersji modelu dla wynikowej formuły na model oryginalnej formuły. Jednak nie ma standardu dla drukowania modeli konwerterów, a Z3 nie może odczytać tych opisów. Oczywiście możemy skleić wszystko razem za pomocą programowych interfejsów API.

• Mały zestaw taktyk w ramach (tylko zaufane wyniki mogą być zaufane) lub wyższy (tylko niesatysfakcjonujące wyniki mogą być zaufane) przybliżenia. Są one zwykle używane w modelu lub znalezieniu dowodów. Kiedy Z3 wyświetli wynikowy cel, poinformuje, że wynik jest dokładny (można zaufać sat i unsat).