Definieren einer Theorie von Sätzen mit Z3/SMT-LIB2

Question

Ich versuche, eine Theorie von Sätzen (Vereinigung, Kreuzung etc.) für Z3 zu definieren, die die SMTLIB-Schnittstelle verwenden. Leider hängt meine aktuelle Definition z3 für eine triviale Abfrage, also denke ich, dass mir einige einfache Option/Flags fehlen.

hier ist der Link: 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) 

Jeder Hinweis, was ich vermisst habe?

Auch, was ich sagen kann, gibt es keine Standard-SMT-LIB2 Kodierung der Set-Operationen, z.B. Z3.mk_set_{add,del,empty,...} (weshalb ich versuche, diese Funktionalität über Quantifizierer zu bekommen.) Ist das korrekt? Oder gibt es eine andere Route?

Danke!

Ranjit.

Answer 1

Ihre Formel ist erfüllbar, und Z3 ist nicht in der Lage, ein Modell für diese Art von Formel zu erstellen. Beachten Sie, dass es eine Interpretation für die nicht interpretierte Sortierung Set generieren muss. Es gibt ein paar Alternativen, die Sie in Betracht ziehen können.

1- Deaktivieren Sie das model-based quantifier instanziation (MBQI) -Modul. BTW, alle Boogie-basierten Tools (VCC, Dafny, Coral, etc.) tun das. Um den MBQI Modul zu deaktivieren, haben wir

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

Bemerkung verwenden: in dem Work-in-progress Zweig die Option :mbqi wurde :smt.mbqi umbenannt.

Nachteile: Wenn das MBQI-Modul deaktiviert ist, gibt Z3 normalerweise unknown für erfüllbare Formeln zurück, die Quantifizierer enthalten.

2- Codieren Sie Sätze von T als Arrays von T nach Boolean. Z3 unterstützt erweiterte Array-Theorie. Die erweiterte Theorie hat zwei neue Operatoren: ((_ const T) a) Konstante Arrays, ((_ map f) a b) Kartenoperator. This paper beschreibt die erweiterte Array-Theorie und beschreibt, wie Mengenoperationen wie Vereinigungen und Überschneidungen, die sie verwenden, codiert werden. Die rise4fun Website hat Beispiele. Dies ist eine gute Alternative, wenn dies die einzigen Quantifizierer in Ihrem Problem sind, da das Problem jetzt in einem entscheidbaren Fragment liegt. Auf der anderen Seite, wenn Sie zusätzliche quantifizierte Formeln haben, die Mengen enthalten, wird dies wahrscheinlich schlecht funktionieren. Das Problem ist, dass das durch die Array-Theorie gebildete Modell die Existenz der zusätzlichen Quantifizierer nicht kennt.

Zum Beispiel, wie die oben genannten Operatoren zu kodieren const verwenden und siehe Karte: http://rise4fun.com/Z3/DWYC

3- Stellen Sätze von T als Funktionen von T bis Bool. Dieser Ansatz funktioniert normalerweise gut, wenn wir keine Mengen von Mengen oder nicht interpretierte Funktionen haben, die Mengen als Argumente annehmen. Das Z3-Online-Tutorial enthält ein Beispiel (Abschnitt Quantifizierer).