Czy Z3 może być używany do wnioskowania o podciągach?

Question

Próbuję użyć Z3 do uzasadnienia podłańcuchów i napotkałem pewne nieintuicyjne zachowanie. Z3 zwraca 'sat', gdy zostanie poproszony o ustalenie, czy "xy" pojawia się w ciągu "xy", ale zwraca "nieznany", gdy pytanie "x" jest w "x", lub "x" w "xy".

mam skomentował poniższy kod, żeby zilustrować ten problem:

(set-logic AUFLIA) 
(declare-sort Char 0) 

;characters to build strings are _x_ and _y_ 
(declare-fun _x_() Char) 
(declare-fun _y_() Char) 
(assert (distinct _x_ _y_)) 

;string literals 
(declare-fun findMeX() (Array Int Char)) 
(declare-fun findMeXY() (Array Int Char)) 
(declare-fun x() (Array Int Char)) 
(declare-fun xy() (Array Int Char)) 
(declare-fun length ((Array Int Char)) Int) 

;set findMeX = 'x' 
(assert (= (select findMeX 0) _x_)) 
(assert (= (length findMeX) 1)) 

;set findMeXY = 'xy' 
(assert (= (select findMeXY 0) _x_)) 
(assert (= (select findMeXY 1) _y_)) 
(assert (= (length findMeXY) 2)) 

;set x = 'x' 
(assert (= (select x 0) _x_)) 
(assert (= (length x) 1)) 

;set xy = 'xy' 
(assert (= (select xy 0) _x_)) 
(assert (= (select xy 1) _y_)) 
(assert (= (length xy) 2)) 

teraz, że problem jest skonfigurowana, staramy się znaleźć podciągi:

;search for findMeX='x' in x='x' 

(push 1) 
(assert 
    (exists 
    ((offset Int)) 
    (and 
     (<= offset (- (length x) (length findMeX))) 
     (>= offset 0) 
     (forall 
     ((index Int)) 
     (=> 
      (and 
      (< index (length findMeX)) 
      (>= index 0)) 
      (= 
      (select x (+ index offset)) 
      (select findMeX index))))))) 

(check-sat) ;'sat' expected, 'unknown' returned 
(pop 1) 

Gdybyśmy zamiast szukać findMeXY w xy, solver zwraca 'sat', zgodnie z oczekiwaniami. Wydaje się, że ponieważ solver może obsłużyć to zapytanie dla "xy", powinno być w stanie obsłużyć to dla "x". Ponadto, wyszukując findMeX='x' w 'xy='xy', zwraca "nieznany".

Czy ktoś może zaproponować wyjaśnienie, a może alternatywny model wyrażania tego problemu w rozwiązaniu SMT?

Answer 1

Krótka odpowiedź dla obserwowanego zachowania to: Z3 zwraca "nieznany", ponieważ twoje asercje zawierają kwantyfikatory.

Z3 zawiera wiele procedur i heurystyk do obsługi kwantyfikatorów. Z3 wykorzystuje technikę nazywaną modelowaniem ilościowym (MBQI) do modelowania modeli do zadawania takich zapytań jak Twoja. Pierwszym krokiem jest ta procedura polegająca na utworzeniu interpretacji kandydata na podstawie interpretacji spełniającej wolne twierdzenia kwantyfikatora. Niestety, w bieżącym Z3 ten krok nie współdziała płynnie z teorią macierzy. Podstawowym problemem jest to, że interpretacja zbudowana przez teorię macierzy nie może być modyfikowana przez ten moduł.

Prawidłowe pytanie brzmi: dlaczego to działa, gdy usuwamy komendy push/pop? Działa, ponieważ Z3 stosuje bardziej agresywne kroki upraszczające (preprocessing), gdy nie są używane przyrostowe polecenia rozwiązywania (takie jak polecenia push i pop).

Widzę dwa możliwe obejścia problemu.

• Można uniknąć kwantyfikatorów i dalej używać teorii tablic. Jest to wykonalne w twoim przykładzie, ponieważ znasz długość wszystkich "łańcuchów". W ten sposób można rozszerzyć kwantyfikator. Chociaż takie podejście może wydawać się niezręczne, jest ono stosowane w praktyce oraz w wielu narzędziach do weryfikacji i testowania.

• Możesz uniknąć teorii macierzy. Deklarujesz ciąg znaków jako typ nieinterpretowany, tak jak zrobiłeś to dla Char. Następnie deklarujesz funkcję char-of, która ma zwrócić i-ty znak ciągu. Możesz dokonać aksjomatyzacji tej operacji. Na przykład, można powiedzieć, że dwa ciągi są równe, jeśli mają taką samą długość i zawierają te same znaki:

(assert (forall ((s1 String) (s2 String)) 
       (=> (and 
        (= (length s1) (length s2)) 
        (forall ((i Int)) 
          (=> (and (<= 0 i) (< i (length s1))) 
           (= (char-of s1 i) (char-of s2 i))))) 
        (= s1 s2)))) 

Poniższy link zawiera skrypt zakodowany przy użyciu drugiego podejścia: http://rise4fun.com/Z3/yD3

Drugie podejście jest bardziej atrakcyjne i pozwoli ci udowodnić bardziej skomplikowane właściwości dotyczące łańcuchów. Jednak bardzo łatwo jest napisać zadowalające skwantyfikowane formuły, że Z3 nie będzie w stanie zbudować modelu. The Z3 Guide opisuje główne możliwości i ograniczenia modułu MBQI. Zawiera może decydujące fragmenty, które mogą być obsługiwane przez Z3. BTW, pamiętaj, że upuszczenie teorii tablic nie będzie dużym problemem, jeśli masz kwantyfikatory. Przewodnik pokazuje, jak kodować tablice za pomocą kwantyfikatorów i funkcji.

można znaleźć więcej informacji o tym, jak MBQI działa w następujących dokumentach:

• Complete instantiation for quantified SMT formulas

• Efficiently Solving Quantified Bit-Vector Formula