擅长:python、mysql、java
<p>在下面,您可以找到问题的直接SMT编码,<em>除了求和要求的</em></p>
<pre><code>(set-option :smt.mbqi true) ; also try false (e-matching instead of MBQI)
(declare-fun A (Int) Int)
(assert
(=
10000
(+
(A 1)
(A 2)
(A 3)
; ...
(A 99))))
; A(x) > 10 where 0<x<100
(assert (forall ((x Int))
(implies
(and (< 0 x) (< x 100))
(> (A x) 10))))
; A(x) = 0 where x>= 100
(assert (forall ((x Int))
(implies
(>= x 100)
(> (A x) 10))))
; A(3) = 190
(assert (= (A 3) 190))
; A(12) = 1200
(assert (= (A 12) 1200))
(check-sat)
</code></pre>
<p>几句话:</p>
<ul>
<li><p>所有SMT功能都是合计的;如果要对部分函数进行编码,必须显式地对函数的域进行建模,并使定义公理以参数是否在域中为条件。不过,Z3仍将为您提供该功能的总体模型</p>
</li>
<li><p>在SMT中,由于没有求和理解运算符,所以任意求和编码是非常重要的。不过,您的情况更简单,因为您的总和覆盖静态已知数量的元素(<em>0<;x<;100</em>)</p>
</li>
<li><p>如果Z3py提供了一种方便的源代码语法,可以在静态已知的许多元素上生成和,我不会感到惊讶</p>
</li>
</ul>