擅长:python、mysql、java
<p>一阶逻辑中使用的术语、原子和文字的“教科书”定义不能直接应用于Z3表达式。在Z3中,我们允许像<code>f(And(a, b)) > 0</code>和<code>f(ForAll([x], g(x) == 0))</code>这样的表达式,其中<code>f</code>是一个从布尔到整数的函数。这种扩展并没有增加表现力,但在编写问题时它们非常方便。SMT2.0标准还允许“term”<code>if-then-else</code>表达式。这是另一个允许我们在“术语”中嵌套“公式”的功能。示例:<code>g(If(And(a, b), 1, 0))</code>。在</p>
<p>在实现操作Z3表达式的过程时,我们有时需要区分布尔表达式和非布尔表达式。在本例中,“term”只是一个没有布尔排序的表达式。在</p>
<pre><code>def is_term(a):
return not is_bool(a)
</code></pre>
<p>在其他实例中,我们希望以一种特殊的方式处理布尔连接词(<code>And</code>,<code>Or</code>,…)。例如,我们定义了一个CNF转换器。在本例中,我们将“atom”定义为任何不是量词的布尔表达式、一个(自由)变量或一个不是布尔连接词的应用程序。在</p>
^{pr2}$
<p>在我们定义原子之后,字面量可以定义为:</p>
^{3}$
<p>下面是一个示例,演示了这些函数(也可以在<a href="http://rise4fun.com/Z3Py/NCQ0" rel="nofollow">rise4fun</a>上在线获得):</p>
<pre><code>x = Int('x')
p, q = Bools('p q')
f = Function('f', IntSort(), BoolSort())
g = Function('g', IntSort(), IntSort())
print is_literal(Not(x > 0))
print is_literal(f(x))
print is_atom(Not(x > 0))
print is_atom(f(x))
print is_atom(x)
print is_term(f(x))
print is_term(g(x))
print is_term(x)
print is_term(Var(1, IntSort()))
</code></pre>