Получить соответствующее имя переменной Python для имени модели Z3 - PullRequest
Новая
       11

Получить соответствующее имя переменной Python для имени модели Z3

0 голосов
/ 09 января 2019

Есть ли способ получить соответствующее имя переменной python для имени модели z3?

Предположим, у меня есть следующий код: 

from z3 import *

s = Solver()

a = [Real('a_%s' % k) for k in range(10)]

for i in range(10):
    s.add(a[i] > 10)

s.check()

m = s.model()
for d in m:
    print(d, m[d])

Здесь d в m равны a_0, a_1, a_2,..., a_9, а все их значения равны 11. Я пытаюсь установить некоторые ограничения, которые делают переменные не равными предыдущему результату проверки, например: 

s.add(a[0] != m['a_0']
...
s.add(a[9] != m['a_9']

Поэтому мой вопрос заключается в том, что у Z3 есть метод для получения соответствующего имени переменной python для имени модели z3? Если так, то мне не нужно перечислять все имена переменных. Потому что это будет огромной работой, если у нас будет много переменных. То, чего я хочу достичь, может быть следующим: 

m = s.model()
for d in m:
    s.add(corresponding_python_variabl_name(d) != m[d])

Имеет ли Z3 эту функцию corresponding_python_variable_name()? Заранее спасибо!

1 Ответ

0 голосов
/ 09 января 2019

Похоже, вы пытаетесь создать все возможные модели?

Если это так, используйте следующий шаблон: 

from z3 import *

s = Solver()

a = [Real('a_%s' % k) for k in range(10)]

for i in range(10):
    s.add(a[i] > 10)

while s.check() == sat:
   m = s.model()

   if not m:
       break

   print m

   s.add(Not(And([v() == m[v] for v in m])))

Обратите внимание, что в этом цикле будет столько разных моделей, сколько есть; так что если у вас много моделей (потенциально бесконечных с Real s, как в вашей задаче), то это будет продолжаться вечно. (Или до тех пор, пока не закончится память / процессор и т. Д.)

...