Получение всех решений логического выражения в Z3Py никогда не заканчивается - PullRequest
Новая
       21

Получение всех решений логического выражения в Z3Py никогда не заканчивается

1 голос
/ 26 марта 2020

Вероятно, базовый c вопрос, связанный с Z3: я пытаюсь получить все решения логического выражения, например, для a OR b, я хочу получить {(true, true),(false,true),(true,false)}

На основе других найденных ответов Например, Z3: найти все подходящие модели , у меня есть следующий код: 

a = Bool('a')
b = Bool('b')

f1=Or(a,b)
s=Solver()
s.add(f1)

while s.check() == sat:
  print s
  s.add(Not(And(a == s.model()[a], b == s.model()[b])))

Проблема в том, что он входит в бесконечное l oop, как на второй итерации: ограничение a == s.model()[a] оценивается как ложное b / c s.model()[a] больше не существует.

Может кто-нибудь сказать, что я делаю неправильно?

1 Ответ

1 голос
/ 26 марта 2020

Я бы посоветовал вам попробовать написать l oop следующим образом: 

from z3 import *

a = Bool('a')
b = Bool('b')

f1 = Or(a,b)
s = Solver()
s.add(f1)

while s.check() == sat:

    m = s.model()

    v_a = m.eval(a, model_completion=True)
    v_b = m.eval(b, model_completion=True)

    print("Model:")
    print("a := " + str(v_a))
    print("b := " + str(v_b))

    bc = Or(a != v_a, b != v_b)
    s.add(bc)

Вывод: 

Model:
a := True
b := False
Model:
a := False
b := True
Model:
a := True
b := True

Аргумент model_completion=True необходим, потому что в противном случае m.eval(x) ведет себя как отношение тождества для любой логической переменной x с неважным значением в текущей модели m и возвращает x в результате вместо True/False. ( См. Связанный Q / A )

ПРИМЕЧАНИЕ: , поскольку z3 любезно отмечает все равно булевы переменные, альтернативным вариантом будет написать собственный генератор моделей, который автоматически завершает любую частичную модель. Это уменьшит количество звонков до s.check(). Влияние этой реализации на производительность трудно измерить, но оно может быть немного быстрее.

...