Сравнение модели Python Z3 - PullRequest
Новая
       9

Сравнение модели Python Z3

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

Имея набор формул и используя z3py для создания двух моделей old_model = solver.model() и new_model. Как получить список имен переменных, имеющих разные назначения в двух моделях?

Необходимо общее решение, учитывающее все свободные переменные в наборе формул. Если возможно, есть случай, когда переменная определяется как var = Int('varname') m и используется только в формуле ForAll(var, ...), эта переменная var не должна учитываться при начале сравнения моделей.

Идея состоит в том, чтобы использовать сравнение во время отладки и видеть, существуют ли какие-либо неожиданные переменные, которые определяют различия между моделями, или эта переменная не должна появляться в модели.

1 Ответ

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

Непонятно, о чем вы спрашиваете; но когда z3 дает вам модель, это просто словарь, отображающий переменные в их значения. Вы можете легко держать их в Python: 

from z3 import *

s = Solver()

x, y, z = Ints('x y z')

s.add(x + y > 5)

s.add(ForAll([z], z > z-1))

s.check()
m = s.model()

print m

# get the variables:
for v in m:
  print v

Это печатает: 

[y = 0, x = 6]
y
x

Как видите, y и x есть, а z нет; как вы хотели, я думаю. Если у вас есть несколько моделей, вы можете просто запросить их по отдельности, искать различия и заниматься программированием по вашему желанию. Это то, что вы ищете?

...