Comment obtenir une liste d'entiers d'un ensemble donné d'entiers possibles dans z3?

Question

L'exemple minimal est le suivant: Étant donné un ensemble d'entiers possibles [1, 2, 3] créer une liste arbitraire de taille 5 en utilisant z3py. Les doublons sont autorisés.

Le résultat attendu est quelque chose comme [1, 1, 1, 1, 1] ou [3, 1, 2, 2, 3], etc.

Comment résoudre ce problème et comment mettre en œuvre « choisir »? Enfin, je voudrais trouver toutes les solutions qui peuvent être faites en ajoutant des contraintes supplémentaires comme expliqué dans link. Toute aide sera très appréciée.

Answer 1

Ce qui suit devrait fonctionner:

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