我已在 SMT 中从使用 Int 改为使用 Bit Vectors。但是，逻辑 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)) ) ) )
最佳答案
严格来说，你运气不好。根据http://smtlib.cs.uiowa.edu/logics.shtml ，不存在同时包含量词和位向量的逻辑。
话虽如此，大多数求解器都允许非标准组合。只需省略 set-logic 命令，您可能会很幸运。例如，Z3 可以在没有 set-logic 部分的情况下很好地处理您的查询；我刚刚尝试过..
关于z3 - 定义 SMT2 中位向量的规则，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/31415377/