Z3: trovare tutti i modelli soddisfacenti

Question

Sto cercando di recuperare tutti i possibili modelli per alcune teorie del primo ordine usando Z3, un risolutore SMT sviluppato da Microsoft Research. Ecco un esempio di lavoro minima:

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

In questo caso proposizionale ci sono due assegnazioni soddisfacenti: f->true e f->false. Poiché Z3 (e risolutori SMT in generale) cercheranno solo di trovare un modello soddisfacente, trovare tutte le soluzioni non è direttamente possibile. Here Ho trovato un utile comando chiamato (next-sat), ma sembra che l'ultima versione di Z3 non supporti più questo. Questo è un po 'sfortunato per me, e in generale penso che il comando sia abbastanza utile. C'è un altro modo per farlo?

Answer 1

Un modo per ottenere ciò è utilizzare una delle API, insieme alla capacità di generazione del modello. È quindi possibile utilizzare il modello generato da un controllo di soddisfacibilità per aggiungere vincoli per impedire l'utilizzo dei precedenti valori del modello nelle successive verifiche di soddisfacibilità, fino a quando non vi sono più assegnazioni soddisfacenti. Ovviamente, devi usare gli ordinamenti finiti (o avere alcuni vincoli che lo assicurino), ma potresti usare questo anche con infiniti tipi se non vuoi trovare tutti i modelli possibili (cioè fermati dopo aver generato un mucchio) .

Ecco un esempio utilizzando z3py (link z3py script: 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 

In generale, utilizzando la disgiunti di tutte le costanti coinvolte dovrebbe funzionare (ad esempio, a e b qui). Questo enumera tutti i compiti interi per a e b (tra 1 e 20) che soddisfano a >= 2b. Ad esempio, se ci limitiamo a e b giacere tra 1 e 5 invece, l'uscita è:

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