定义SMT2中位向量的规则

Question

我已经在SMT中从使用Int转换为位向量。然而，逻辑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部分的情况下可以很好地处理您的查询;