добавить итеративно в z3 - PullRequest
Новая
       12

добавить итеративно в z3

0 голосов
/ 30 октября 2019

Я хочу проверить значение a, b, c, и если значение 'a' равно 1, то 'x' прибавляется к единице. Продолжаем процесс для значений «b» и «c». Поэтому, если a = 1, b = 1, c = 1, результат x должен быть равен 3. Если a = 1, b = 1, c = 0, значит, результат x должен быть 2. Любые методы, которые будут реализованы вz3? Исходный код выглядит так: 

from z3 import *

a, b, c = Ints('a b c')
x, y = Ints('x y')
s = Solver()
s.add(If(a==1, x=x + 1, y = y-1))
s.add(If(b==1, x=x + 1, y = y-1))
s.add(If(c==1, x=x + 1, y = y-1))
s.check()
print s.model()

Есть предложения о том, что я могу сделать?

Ответы [ 2 ]

1 голос
/ 30 октября 2019

Этот тип «итеративной» обработки обычно моделируется путем развертывания назначений и создания так называемой формы SSA. (Статическое одиночное присвоение.) В этом формате каждая переменная назначается точно один раз, но может использоваться много раз. Обычно это делается каким-то базовым инструментом, поскольку это довольно утомительно, но вы можете сделать это и вручную. Применительно к вашей проблеме это будет выглядеть примерно так: 

from z3 import *

s = Solver()

a, b, c = Ints('a b c')

x0, x1, x2, x3 = Ints('x0 x1 x2 x3')

s.add(x0 == 0)
s.add(x1 == If(a == 1, x0+1, x0))
s.add(x2 == If(b == 1, x1+1, x1))
s.add(x3 == If(c == 1, x2+1, x2))

# Following asserts are not part of your problem, but
# they make the output interesting
s.add(b == 1)
s.add(c == 0)

# Find the model
if s.check() == sat:
   m = s.model()
   print("a=%d, b=%d, c=%d, x=%d" % (m[a].as_long(), m[b].as_long(), m[c].as_long(), m[x3].as_long()))

else:
    print "no solution"

Преобразование SSA применяется к переменной x, создавая столько экземпляров, сколько необходимо для моделирования назначений. При запуске эта программа выдает: 

a=0, b=1, c=0, x=1

Надеюсь, это поможет!

0 голосов
/ 31 октября 2019

Обратите внимание, что у z3 много функций. Здесь вы можете использовать Sum() для суммы списка. Внутри списка вы можете поместить простые переменные, но и выражение. Вот пример как простой, так и более сложной суммы: 

from z3 import *

a, b, c = Ints('a b c')
x, y = Ints('x y')
s = Solver()
s.add(a==1, b==0, c==1)
s.add(x==Sum([a,b,c]))
s.add(y==Sum([If(a==1,-1,0),If(b==1,-1,0),If(c==1,-1,0)]))
if s.check() == sat:
    print ("solution:", s.model())
else:
    print ("no solution possible")

Результат: solution: [y = 2, x = 2, c = 1, b = 0, a = 1]

Если ваша проблема более сложная, использование BitVecs вместо Ints может заставить ее выполнитьнемного быстрее.

edit: вместо Sum() вы также можете просто использовать сложение, как в

s.add (x == a + b + c) s.add (y ==If (a == 1, -1,0) + If (b == 1, -1,0) + If (c == 1, -1,0))

Sum() имеет смыслк удобочитаемости, когда у вас более длинный список переменных или когда переменные уже есть в списке.

...