Definiowanie teorii zbiorów za pomocą Z3/SMT-LIB2

Question

Próbuję zdefiniować teorię zbiorów (połączenie, przecięcie itp.) dla Z3 przy użyciu interfejsu SMTLIB. Niestety moja obecna definicja zawiesza się z3 dla trywialnego zapytania, więc domyślam się, że brakuje mi jednej prostej opcji/flag.

oto odnośnik: http://rise4fun.com/Z3/JomY

 
(declare-sort Set) 
(declare-fun emp() Set) 
(declare-fun add (Set Int) Set) 
(declare-fun cup (Set Set) Set) 
(declare-fun cap (Set Set) Set) 
(declare-fun dif (Set Set) Set) 
(declare-fun sub (Set Set) Bool) 
(declare-fun mem (Int Set) Bool) 
(assert (forall ((x Int)) (not (mem x emp)))) 
(assert (forall ((x Int) (s1 Set) (s2 Set)) 
      (= (mem x (cup s1 s2)) (or (mem x s1) (mem x s2))))) 
(assert (forall ((x Int) (s1 Set) (s2 Set)) 
      (= (mem x (cap s1 s2)) (and (mem x s1) (mem x s2))))) 
(assert (forall ((x Int) (s1 Set) (s2 Set)) 
      (= (mem x (dif s1 s2)) (and (mem x s1) (not (mem x s2)))))) 
(assert (forall ((x Int) (s Set) (y Int)) 
      (= (mem x (add s y)) (or (mem x s) (= x y))))) 

(declare-fun z3v8() Bool) 
(assert (not z3v8)) 
(check-sat) 

Wszelkie wskazówkę co do czego mi brakuje?

Ponadto, z tego co wiem, nie ma standardowego kodowania operacji ustawionych na przykład SMT-LIB2 Z3.mk_set_{add,del,empty,...} (dlatego próbuję uzyskać tę funkcję za pomocą kwantyfikatorów). Czy to prawda? A może jest inna droga?

Dzięki!

Ranjit.

Answer 1

Twoja formuła jest satysfakcjonująca, a Z3 nie jest w stanie wytworzyć modelu dla tego rodzaju formuły. Zauważ, że będzie musiał wygenerować interpretację dla niezinterpretowanego sortowania Set. Istnieje kilka alternatyw, które możesz rozważyć.

1- Wyłącz moduł tworzenia kwantyfikatora opartego na modelu (MBQI). BTW, wszystkie narzędzia oparte na Boogie (VCC, Dafny, Coral itp.) To robią. Aby wyłączyć moduł MBQI, musimy użyć

(set-option :auto-config false) 
(set-option :mbqi false) 

uwaga: w branży work-in-progress, opcja :mbqi została zmieniona na :smt.mbqi.

Minusy: gdy moduł MBQI jest wyłączony, Z3 zwykle zwraca unknown dla satysfakcjonujących formuł zawierających kwantyfikator.

2- Koduje zestawy T jako tablice od T do wartości logicznej. Z3 obsługuje rozszerzoną teorię macierzy. Rozszerzona teoria ma dwóch nowych operatorów: ((_ const T) a) stałych tablic, ((_ map f) a b) operator mapy. This paper opisuje rozszerzoną teorię tablicową i sposób kodowania operacji ustawionych, takich jak połączenie i przecięcie za jego pomocą. Strona internetowa rise4fun ma przykłady. Jest to dobra alternatywa, jeśli są to jedyne kwantyfikatory w twoim problemie, ponieważ problem jest teraz w rozstrzygającym fragmencie. Z drugiej strony, jeśli masz dodatkowe kwantyfikowane formuły zawierające zestawy, prawdopodobnie będzie to źle działać. Problem polega na tym, że model zbudowany przez teorię macierzy jest nieświadomy istnienia dodatkowych kwantyfikatorów.

Na przykład jak zakodować powyższe operatorów za pomocą const i map zobacz: http://rise4fun.com/Z3/DWYC

3- okazje zestawy T jak funkcje z T na Bool. Takie podejście zwykle działa dobrze, jeśli nie mamy zestawów zestawów lub nieinterpretowanych funkcji, które przyjmują zestawy jako argumenty. samouczek online Z3 ma przykład (sekcja Kwantyfikatory).