CODEWITHSUNDEEP
counterz3smtz3py
Mark Jin
Mark Jin

Reputation: 2903

z3py: How to implement a counter in z3?

I want to design logics similar to a counter in Z3py.

If writing python script, we usually define a variable "counter" and then keep incrementing it when necessary. However, in Z3, there is no variant. Therefore, instead of defining an variant, I define a trace of that variant.

This is a sample code. Suppose there is an array "myArray" of size 5, and the elements in the array are 1 or 2. I want to assert a constraint that there must be two '2's in "myArray"

from z3 import *

s = Solver()
myArray = IntVector('myArray',5)
for i in range(5):
    s.add(Or(myArray[i]==1,myArray[i]==2))
counterTrace = IntVector('counterTrace',6)
s.add(counterTrace[0]==0)
for i in range(5):
    s.add(If(myArray[i]==2,counterTrace[i+1]==counterTrace[i]+1,counterTrace[i+1]==counterTrace[i]))
s.add(counterTrace[5]==2)
print s.check()
print s.model()

My question is that is this an efficient way of implementing the concept of counter in Z3? In my real problem, which is more complicated, this is really inefficient.

Upvotes: 1

Views: 1219

Answers (1)

usr
usr

Reputation: 171206

You can do this but it is much easier to create the sum over myArray[i] == 2 ? 1 : 0. That way you don't need to assert anything and you are dealing with normal expressions.

Upvotes: 1

Related Questions