验证查询公式、SMT 求解器、Z3、STP

【问题标题】：Validation query formulation, SMT solver, Z3, STP验证查询公式、SMT 求解器、Z3、STP
【发布时间】：2014-01-31 10:37:26
【问题描述】：

我有一个布尔公式f(a, b, x, y)。其中 a 和 b 是布尔表达式，x 和 y 是位向量表达式。 a 和 b 是布尔表达式，可能使用表达式 a, b, x 和 y。

我想为有效性定义以下查询：

f(a, b, x, y)* such that *a = false && b = false 

f(a, b, x, y)* such that *a = true && b = false

在某种程度上，我需要替换公式中 a 和 b 的值暗示的双方。

请告知如何创建这样的查询。

【问题讨论】：

标签： z3 smt

【解决方案1】：

为什么不为 a 创建一个新变量？然后，您可以断言以下内容：（断言（不是一个））（断言（不是 b））（断言（f a b x y））（断言a2）（断言（非（f a2 b x y））） (check-sat)

当且仅当上述查询不可满足时，您的查询才有效，因为绑定被表示为断言并且暗示被否定（并被展平为两个断言）

【讨论】：