<p>在z3py中可以有多种方法来编写这个示例。对于列出的约束,您可以使用符号数组、未解释的函数或为100个元素中的每个元素使用单独的变量</p>
<h2>使用数组</h2>
<p>这种情况下最简单的方法是使用数组:即将<code>Int -> Int</code>函数建模为数组:</p>
<pre class="lang-py prettyprint-override"><code>from z3 import *
A = Array('A', IntSort(), IntSort())
s = Solver()
total = 0
for i in range(100):
s.add(A[i] > 10)
total = total + A[i]
s.add(total == 10000)
s.add(A[ 3] == 190)
s.add(A[12] == 1200)
k = Int('k')
s.add(ForAll(k, (Implies(Or(k < 0, k >= 100), A[k] == 0))))
if s.check() == sat:
m = s.model()
for i in range(100):
v = m.evaluate(A[i]).as_long()
print("%3d: %d" % (i, v))
</code></pre>
<p>运行时,此选项将打印:</p>
<pre><code> 0: 131
1: 19
2: 436
3: 190
4: 12
5: 11
6: 19
7: 24
8: 11
9: 13
10: 133
11: 134
12: 1200
13: 39
14: 132
15: 134
16: 134
17: 134
18: 30
19: 132
20: 132
21: 38
22: 16
23: 132
24: 22
25: 132
26: 134
27: 27
28: 134
29: 76
30: 130
31: 15
32: 132
33: 134
34: 31
35: 123
36: 35
37: 58
38: 123
39: 64
40: 49
41: 20
42: 139
43: 24
44: 134
45: 11
46: 132
47: 132
48: 22
49: 11
50: 134
51: 134
52: 134
53: 132
54: 132
55: 11
56: 134
57: 11
58: 11
59: 132
60: 11
61: 71
62: 134
63: 58
64: 132
65: 132
66: 134
67: 134
68: 39
69: 74
70: 132
71: 134
72: 134
73: 11
74: 18
75: 134
76: 16
77: 132
78: 17
79: 132
80: 132
81: 132
82: 15
83: 132
84: 132
85: 134
86: 15
87: 132
88: 134
89: 18
90: 132
91: 132
92: 132
93: 132
94: 12
95: 132
96: 22
97: 121
98: 24
99: 11
</code></pre>
<p>您可以汇总打印的值,以确保它确实为您提供<code>10000</code></p>
<h2>使用未解释的函数</h2>
<p>您还可以将<code>A</code>建模为未解释的函数。对上述内容而言,所需的更改实际上微不足道:</p>
<pre class="lang-py prettyprint-override"><code>from z3 import *
A = Function('A', IntSort(), IntSort())
s = Solver()
total = 0
for i in range(100):
s.add(A(i) > 10)
total = total + A(i)
s.add(total == 10000)
s.add(A( 3) == 190)
s.add(A(12) == 1200)
k = Int('k')
s.add(ForAll(k, (Implies(Or(k < 0, k >= 100), A(k) == 0))))
if s.check() == sat:
m = s.model()
for i in range(100):
v = m.evaluate(A(i)).as_long()
print("%3d: %d" % (i, v))
</code></pre>
<p>这张照片是:</p>
<pre><code> 0: 11
1: 11
2: 11
3: 190
4: 11
5: 11
6: 11
7: 11
8: 11
9: 11
10: 11
11: 11
12: 1200
13: 11
14: 11
15: 11
16: 11
17: 11
18: 11
19: 11
20: 11
21: 11
22: 11
23: 11
24: 11
25: 11
26: 11
27: 11
28: 11
29: 11
30: 11
31: 11
32: 11
33: 11
34: 11
35: 11
36: 11
37: 11
38: 11
39: 11
40: 11
41: 11
42: 11
43: 11
44: 11
45: 11
46: 11
47: 11
48: 11
49: 11
50: 11
51: 11
52: 11
53: 11
54: 11
55: 11
56: 11
57: 11
58: 11
59: 11
60: 11
61: 11
62: 11
63: 11
64: 11
65: 11
66: 11
67: 11
68: 11
69: 11
70: 11
71: 11
72: 11
73: 11
74: 7543
75: 11
76: 11
77: 11
78: 11
79: 11
80: 11
81: 11
82: 11
83: 11
84: 11
85: 11
86: 11
87: 11
88: 11
89: 11
90: 11
91: 11
92: 11
93: 11
94: 11
95: 11
96: 11
97: 11
98: 11
99: 11
</code></pre>
<p>在这种情况下,模型非常不同,但很容易看到它有<code>A(3) = 190</code>、<code>A(12) = 1200</code>、<code>A(74) = 7543</code>,所有其他条目都设置为11;总共给你<code>190 + 1200 + 7543 + 11 * 97 = 10000</code></p>
<h2>使用独立变量</h2>
<p>第三种方法是在python数组中分配100个整数元素,并分别对单个元素声明约束。这将导致最简单的模型,因为它不会使用任何量化。当然,这将模拟范围<code>0..99</code>之外的元素隐式为0的事实,因此仅当不需要显式提及此约束时才使用此选项。同样,编码几乎相同:</p>
<pre class="lang-py prettyprint-override"><code>from z3 import *
A = [Int('A_%d' % i) for i in range(100)]
s = Solver()
total = 0
for i in range(100):
s.add(A[i] > 10)
total = total + A[i]
s.add(total == 10000)
s.add(A[ 3] == 190)
s.add(A[12] == 1200)
if s.check() == sat:
m = s.model()
for i in range(100):
v = m.evaluate(A[i]).as_long()
print("%3d: %d" % (i, v))
</code></pre>
<p>为了简洁起见,我省略了这个输出。请注意,在本例中,我们如何使用<code>A</code>作为python列表,而不是z3py本身直接支持的符号数组</p>
<h2>总结</h2>
<p>最后,您描述的约束非常简单,可以使用这三种技术。哪一个是最好的取决于您想要建模的其他约束。(特别是,您希望避免大量使用量词,如上面的<code>ForAll</code>,因为SMT解算器通常不能很好地处理量词。这个问题足够简单,所以不会造成问题,但当约束变得复杂时,它会增加解算时间或导致解算器回答<code>unknown</code>。)</p>
<p>希望这能让你开始。祝你好运</p>