Z3: encontrar todos os modelos satisfatórios

Eu estou tentando recuperar todos os modelos possíveis para alguma teoria de primeira ordem usando o Z3, um solucionador de SMT desenvolvido pela Microsoft Research. Aqui está um exemplo mínimo de trabalho:

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

Neste caso proposicional existem duas atribuições satisfatórias: f->true e f->false . Como o Z3 (e os solucionadores de SMT em geral) só tentarão encontrar um modelo satisfatório, encontrar todas as soluções não é diretamente possível. Aqui encontrei um comando útil chamado (next-sat) , mas parece que a última versão do Z3 não suporta mais isso. Isso é um pouco infeliz para mim e, em geral, acho que o comando é bastante útil. Existe outra maneira de fazer isso?

    Uma maneira de conseguir isso é usar uma das APIs, juntamente com o recurso de geração de modelos. Você pode então usar o modelo gerado a partir de uma verificação de satisfazibilidade para adicionar restrições para evitar que valores de modelo anteriores sejam usados ​​em verificações de satisfabilidade subsequentes, até que não haja atribuições mais satisfatórias. Claro, você tem que estar usando tipos finitos (ou ter algumas restrições garantindo isso), mas você poderia usar isso com tipos infinitos também, se você não quer encontrar todos os modelos possíveis (ou seja, parar depois de gerar um monte) .

    Aqui está um exemplo usando o z3py (link para o script z3py: 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 

    Em geral, usar o disjunto de todas as constantes envolvidas deve funcionar (por exemplo, b aqui). Isso enumera todas as atribuições de inteiros para b (entre 1 e 20 ) satisfazendo a >= 2b . Por exemplo, se restringirmos a e b para ficar entre 1 e 5 , a saída é:

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