свежие переменные не отображаются в найденных моделях

Question

Я использую z3 для написания статической проверки.У меня следующая проблема:

>>> from z3 import *
>>> s = Solver()
>>> s.add(FreshInt() + FreshInt() > 0)
>>> s.check()
sat
>>> s.model()
[]

Как видите, свежие переменные не отображаются в модели.Я также не могу получить их значение:

>>> a = FreshInt()
>>> s.add(a > 3)
>>> s.check()
sat
>>> s.model()
[]
>>> s.model()[a]

Я просмотрел документы, но не могу найти способ изменить это поведение.Я мог бы генерировать уникальные переменные самостоятельно, но было бы неплохо, если бы z3 позаботился об этом за меня.Может ли кто-нибудь указать мне правильное направление?Или это невозможно изменить в z3py?

Answer 1

FreshInt / FreshReal и т. Д. Предназначены для создания внутренних переменных, которые не видны пользователю.Вместо этого вы должны использовать Int('name') и Real('name') для создания переменных уровня пользователя, которые будут отображаться в моделях.

Если вы действительно хотите увидеть значение, вы можете добавить функцию observer и использовать ее следующим образомthis:

from z3 import *

def observeInt(s, a):
    obs = Int('observer')
    s.add(obs == a)
    # might want to check the following really returns sat!
    s.check()
    print s.model()[obs]

s = Solver()
a = FreshInt()
s.add(a + FreshInt() > 0)
s.add(a > 12)
print s.check()
observeInt(s, a)

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

sat
13

Очевидно, что это не дешево (поскольку включает вызов check), но это безопасно и так долго, как используетсяв ситуациях отладки для сильной руки z3, как вы выразились, это должно сработать.

Answer 2

Вы можете обойти это ограничение следующим образом:

freshIntIdx = 0

def myFreshInt():
    global freshIntIdx
    freshIntIdx += 1;
    return Int('fi' + str(freshIntIdx))

a = myFreshInt()
b = myFreshInt()
s = Solver()
s.add(a + b > 5, a > 0, b > 0, a + b < 10)
print(s.check())
m = s.model()
print("a = %s" % m[a])
print("b = %s" % m[b])