#python #z3 #z3py
#python #z3 #z3py
Вопрос:
В качестве примера возьмем следующее:
from z3 import *
a, b, c, d, e = Bools('a b c d e')
s = Solver()
s.add(Implies(a, b))
s.add(Implies(c, d))
s.add(a)
print s.check()
print s.model()
z3 возвращает:
sat
[a = True, b = True, c = False, d = False]
это модель, в которой говорится, что c и d являются ложными. Но на самом деле эти две переменные могут быть либо true, либо false. Кажется, что z3 возвращает модель, которая присваивает False переменным решения (т. Е. Переменным, значения которых не имеют значения) по умолчанию. Есть ли какой-либо способ получить эти переменные решения? В этом примере это так [c, d, e] .
Комментарии:
1. Смотрите это: github.com/Z3Prover/z3/blob/master/src/api/python/z3 /…
2. Спасибо за ответ! Этот метод
consequences(self, assumptions, variables)может делать то, что я хочу. Но когда я проводил некоторый тест, я обнаружил, что эффективность этого метода недостаточно высока. Я сделал только 1 предположение и проверил около 1500 переменных, и для завершения этого метода потребовалось около 6 секунд (я использовал z3 в проекте, который должен ответить через 2 секунды). Интересно, есть ли какие-либо другие способы или методы решения моей проблемы с более высокой производительностью?