z3 - 在 SMT2 中定义位向量的规则

Question

我已经从使用 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)) ) ) )

Answer 1

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

话虽如此，大多数求解器将允许非标准组合。只需省略set-logic命令，您可能会很幸运。例如，Z3 可以很好地接受您的查询，而无需该set-logic部分；我刚试过。。