1

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.

Aliman
  • 43
  • 6

1 Answers1

1

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])
alias
  • 28,120
  • 2
  • 23
  • 40
  • Amazing! I see you don't use any `Array` or quantifiers but you simply define a variable for each field separately and place the constraint. Perfect, thanks! – Aliman Aug 11 '17 at 04:24