CODEWITHSUNDEEP
z3smtz3py
Rauf
Rauf

Reputation: 27

Building disjunction automatically

I have to build disjunctive/conjunctive formula automatically, all I know is the length of list from where I have to acquire the values of variables, e.g:

x=Int('x')    
list= [0,1,2,3]
solver=Solver()

one approach to do this manually:

solver.add(Or(x==0,x==1,x==2,x==3))

Is it possible to load values of x from a list automatically within a loop or any list comprehension approach? as all I know is the len(list).

Upvotes: 0

Views: 197

Answers (1)

Ali Raeisdnaei
Ali Raeisdnaei

Reputation: 1

Yes I believe that the z3.Or takes in a tuple, so we can just use the python constructs to build that.

solver.add(Or(tuple([x == obj for obj in list])))

Upvotes: 0

Related Questions