Изменить переменную в Z3 python

Question

Я пишу какое-то приложение, которое имитирует какое-то правило. Я нахожу, что фиксированная точка Z3py мне нужна. Мое приложение план может быть следующим: (Fp = Fixedpoint())

1. Объявить некоторые целые переменные, например:. А, Ь, с = Ints ('аб с') и зарегистрировать в fixedpoint - р (a, b, c)

2. Следуйте за свойством некоторых переменных (факт), увеличивайте или уменьшайте некоторые другие переменные. например: , если (a> 0 и b> 0), то c = c + 1

3. Запрос, если целевая переменная удовлетворяет некоторому условию, например. запрос (цель> 0)

Я не знаю, как использовать правило для указания 2. Может ли кто-нибудь сказать мне, возможно ли это сделать?

Answer 1

Я взял пример вы изложенный и создали пример:

• http://rise4fun.com/Z3Py/kD1P

Я надеюсь, что это помогает.

Z3 печатает UNSAT, потому что запрос недоступен. Затем он отображает инвариант, удостоверяющий, что запрос недоступен.

Более подробно

Чтобы объявить свойство с тремя аргументами сделать:

P = Function('P', IntSort(), IntSort(), IntSort(), BoolSort()) 

Чтобы зарегистрировать его для fixedpoint двигателя:

fp.register_relation(P) 

добавить любые правила, которые вы имеете в виду:

fp.rule(P(-1,1,-10)) 
fp.rule(P(a,b,c+1), [a > 0, b > 0, P(a,b,c)]) 
fp.rule(P(a+1,b,c-1), [a <= 0, b < 0, P(a,b,c)]) 

Первое правило гласит что-то о том, какие свойства сохраняются первоначально. Второе правило гласит, что с может быть увеличено, если а> 0, Ь> 0.

Наконец спросить, если какое-то свойство достижима:

print fp.query(P(a,b,c),c > 0)