0

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).

Rauf
  • 27
  • 6
  • I suppose the list is also accessible so that you can get the elements? I think Python's reduce operator should do the trick nicely in functional style, see e.g.: http://stackoverflow.com/questions/10366374/what-is-the-pythonic-equivalent-to-the-fold-function-from-functional-program – Christoph Wintersteiger Apr 30 '15 at 10:50
  • lambda and reduce functions do evaluate the result as true of false, whereas I am interested to write disjunction automatically, I dont want reduce to evaluate it.I just want to bring it into this form... Or(x==0,x==1,x==2,x==3) as my goal is to pass it to z3. – Rauf Apr 30 '15 at 18:04
  • Not sure I understand what you would like to do. What is the problem with using a standard 'for i in ...' loop? – Christoph Wintersteiger May 01 '15 at 11:21

0 Answers0