Search code examples
z3constraint-programmingz3py

How to get a list of integers from a given set of possible integers in z3?


Minimal example is the following: Given a set of possible integers [1, 2, 3] create an arbitrary list of size 5 using z3py. Duplicates are allowed.

The expected result is something like [1, 1, 1, 1, 1] or [3, 1, 2, 2, 3], etc.

How to tackle this problem and how to implement 'choosing'? Finally, I would like to find all solutions which can be done by adding additional constraints as explained in link. Any help will be very appreciated.


Solution

  • The following should work:

    from z3 import *
    
    def choose(elts, acceptable):
        s = Solver()
        s.add(And([Or([x == v for v in acceptable]) for x in Ints(elts)]))
    
        models = []
        while s.check() == sat:
            m = s.model ()
            if not m:
                break
            models.append(m)
            block = Not(And([v() == m[v] for v in m]))
            s.add(block)
    
        return models
    
    print choose('a b c d e', [1, 2, 3])