CODEWITHSUNDEEP
pythonz3smtz3py
the_endian
the_endian

Reputation: 2525

How to get a list of combinations in z3py?

I have a list in python of integers like this:

myList = [97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57]

I want to get Z3 to output various sets or lists of numbers which are all members of myList... Essentially, I want to use Z3 to get additional lists of numbers which all exist in myList but are in various different orders. Put differently, I want to get various outputs from Z3 which contain numbers in the set myList above.

I am having trouble doing this with Z3py because I do not know how to have z3 return a list or a set as the model when I call s.model(), assuming s = Solver().

Upvotes: 0

Views: 658

Answers (1)

alias
alias

Reputation: 30460

from z3 import *

myList = [97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57]

s = Solver ()
pick = []
for (i, v) in enumerate(myList):
  b = Bool ('pick_%d' % i)
  s.add(b == b)
  pick += [(b, v)]

while (s.check() == sat):
    m = s.model()

    chosen = []
    block  = []
    for (p, v) in pick:
        if m.eval(p, model_completion=True):
            chosen += [v]
            block.append(Not(p))
        else:
            block.append(p)

    print chosen
    s.add(Or(block))

Note that this will print 2^n solutions where n is the number of elements in your list; so it'll take a while to finish if n is large!

Upvotes: 1

Related Questions