如何在 z3py 中求和答案

【问题标题】：How to formulate summation in z3py如何在 z3py 中求和
【发布时间】：2015-05-29 03:51:32
【问题描述】：

我对 z3py 很陌生。我正在尝试在 z3py 中编写以下 2 个表达式

和

关于该问题的更多信息可以找到 here

我在 stackoverflow 上搜索了很多，发现了一个 similar question

但很遗憾，我无法得到足够满意的答案。

我尝试在 SMT 中编写第一个代码，方法如下：

#InputGroup, BlockGroup, OutputGroup contain some integer values to represent blocks
InputGroup = [0,1,2]
BlockGroup = [2,3,4,5,6]
OutputGroup = [7,8,9]
Groups = [InputGroup, BlockGroup, OutputGroup]

NumberOfTasks = len(InputGroup)+ len(BlockGroup)+ len(OutputGroup)
M = Function('M', Intsort(), Intsort())
Task = Function('Task', Intsort(), Intsort(), Intsort())
summation1 = Int('summation1')

# each group from the Groups is represented by its index number
for r, g in enumerate(Groups): 
    for m in range(0, NumberOfTasks):
        if(m in g):
            s.add(summation1 == summation1+ M(Task(r,m)))

和SMT中的第二个表达式如下：

NumberOfInputs = len(InputGroup)
NumberOfBlocks = len(BlockGroup)
NumberOfOutputs = len(OutputGroup)
Node = Function('Node', Intsort(), Intsort(), Intsort())
f = Function('f', Intsort(), Intsort(), Intsort())

for r, g in enumerate(Groups):
    if(r != Groups.index(InputGroup) and r != Groups.index(OutputGroup)):
        for i in range(0,(NumberOfInputs+NumberOfBlocks+NumberOfOutputs)):
            summation2 = Int('summation2')
            for m in range(0, (NumberOfTasks)):
                if(m in g and i in g):
                    s.add(summation2 == summation2+ f(Node(r,i), Task(r,m)))
            s.add(summation2 == 1)

虽然我从上述方程中得到了令人满意的结果，但我从中得到的模型有点可疑。我只是想知道我是否正确地表达了这一点。

【问题讨论】：

标签： z3 smt z3py

【解决方案1】：

我想你想改变：

# each group from the Groups is represented by its index number
for r, g in enumerate(Groups): 
    for m in range(0, NumberOfTasks):
        if(m in g):
           s.add(summation1 == summation1+ M(Task(r,m)))

到这样的事情：

# each group from the Groups is represented by its index number
sumTerms = [M(Task(r,m)) 
                  for r, g in enumerate(Groups): 
                     for m in range(0, NumberOfTasks):
                          if(m in g)]
s.add(summation1 == Sum(sumTerms))

第二个例子也是如此。

【讨论】：