在 SMT2 中定义位向量的规则

【问题标题】：Defining Rules for Bit Vectors in SMT2在 SMT2 中定义位向量的规则
【发布时间】：2015-10-03 14:33:51
【问题描述】：

我已经从使用 Int 切换到 SMT 中的位向量。但是，逻辑 QF_BV 不允许在您的脚本中使用任何量词，我需要定义 FOL 规则。我知道如何消除存在量词，但全称量词？该怎么做？

想象一下这样的代码：

(set-logic QF_AUFBV)

(define-sort Index () (_ BitVec 3))

(declare-fun P (Index) Bool)

(assert (forall ((i Index)) (= (P (bvadd i #b001)) (not (P i)) ) ) )

【问题讨论】：

标签： z3 smt quantifiers bitvector first-order-logic

【解决方案1】：

严格来说，你运气不好。根据http://smtlib.cs.uiowa.edu/logics.shtml，不存在同时包含量词和位向量的逻辑。

话虽如此，大多数求解器将允许非标准组合。只需省略set-logic 命令，您可能会很幸运。例如，Z3 在没有 set-logic 部分的情况下可以很好地处理您的查询；我刚试过。。

【讨论】：

确实，Z3 也能识别 UFBV 和 BV 逻辑（没有 QF_）。 SMTLIB 中也有一些针对这些的基准，所以我希望它们很快就会成为官方逻辑。
新的 SMT-LIB 2.5 标准定义了 (set-logic ALL) 用于选择求解器支持的最通用逻辑。（SMT-LIB 2.5 于 2015 年 6 月 28 日发布。）