如何在z3py中制定求和

Question

我對z3py非常陌生。 我想在z3py編寫以下兩個表達式

和

對這個問題的更多信息，可以發現 here

我做搜索計算器一很多，並遇到了一個 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) 

雖然我從上述等式令人滿意的結果，我從中得到的模型是有問題的。 我只想知道我是否正確地表達了這一點。

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

同樣地，對於第二個例子。