Может ли z3py добавить новое утверждение после чтения модели?

Мы можем использовать следующий код, чтобы решить головоломку Dog, Cat, Mouse в учебнике.

dog, cat, mouse = Ints('dog cat mouse')

s = Solver();
s.add(dog>=1)
s.add(cat>=1)
s.add(mouse>=1)
s.add(dog+cat+mouse==100)
s.add(1500 * dog + 100 * cat + 25 * mouse == 10000)

print s.check()
print s.model()

Ну, я знаю, что могу использовать

m=s.model
for d in m.decls():
    print  "%s = %s" % (d.name(), m[d])

чтобы получить имена и значения переменных. Например, cat = 41. Интересно, могу ли я создать новое утверждение из имен и значений, таких как cat != 41. Я использовал

s.add(d.name != m[d]) 
s.add("%s != %s" % (d.name(), m[d]))

Но ни один из них не может работать. Кто-нибудь знает, как добавить новое утверждение, прочитав имена и значения модели? Большое спасибо.


z3 z3py
person Kun    schedule 04.03.2016    source источник

Ответы (1)


arrow_upward
0
arrow_downward

В for d in m.decls(): d — это func_decl, т. е. только объявление, а не переменная (постоянная функция), поэтому нам нужно применить его к своим аргументам, которые здесь пусты. Таким образом, мы можем сделать:

m = s.model()
for d in m.decls():
    v = d() # <-- Note parenthesis ()
    print("%s != %s" % (v, m[d]))
    s.add(v != m[d])

print(s)
print(s.check())

получить

...
cat != 41
mouse != 56
dog != 3
[dog >= 1,
 cat >= 1,
 mouse >= 1,
 dog + cat + mouse == 100,
 1500*dog + 100*cat + 25*mouse == 10000,
 41 != cat,
 56 != mouse,
 3 != dog]
unsat

получить

person Christoph Wintersteiger    schedule 04.03.2016