如何獲取z3中給定的可能整數集合中的整數列表？

Question

最小示例如下：給定一組可能的整數[1, 2, 3]使用z3py創建大小爲5的任意列表。允許重複。

預期的結果是一樣的東西[1, 1, 1, 1, 1]或[3, 1, 2, 2, 3]等

如何解決這個問題，以及如何實現「選擇」？最後，我想找到所有解決方案，可以通過添加其他約束來解決，如link中所述。任何幫助將非常感激。

Answer 1

下面應該工作：

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