1

我有以下 SMT-Lib2 脚本：

(set-option :produce-models true)
(declare-fun s0 () Int)
(declare-fun table0 (Int) (_ BitVec 8))
(assert (= (table0 0) #x00))
(assert
   (let ((s3 (ite (or (< s0 0) (<= 1 s0)) #x01 (table0 s0))))
   (let ((s5 (ite (bvuge s3 #x02) #b1 #b0)))
   (= s5 #b1))))
(check-sat)
(get-model)

在 Mac 上运行 Z3 v3.2 时，我得到：

sat
(model 
  ;; universe for (_ BitVec 8):
  ;;   bv!val!2 bv!val!3 bv!val!0 bv!val!1 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun bv!val!2 () (_ BitVec 8))
  (declare-fun bv!val!3 () (_ BitVec 8))
  (declare-fun bv!val!0 () (_ BitVec 8))
  (declare-fun bv!val!1 () (_ BitVec 8))
  ;; cardinality constraint:
  (forall ((x (_ BitVec 8)))
          (and (= x bv!val!2) (= x bv!val!3) (= x bv!val!0) (= x bv!val!1)))
  ;; -----------
  (define-fun s0 () Int
    (- 1))
  (define-fun table0 ((x!1 Int)) (_ BitVec 8)
    (ite (= x!1 0) bv!val!0
    (ite (= x!1 (- 1)) bv!val!3
      bv!val!0)))
)

其中指出 s0 = -1 是一个模型。但是，对于 s0 = -1，我们有 s3 = 1 和 s5 = #b0，这使得断言为假。事实上，我很确定上述基准是不能令人满意的。

我在 Z3 输出中注意到的一件事是它为基数约束提供的量化公式。它说：

  ;; cardinality constraint:
  (forall ((x (_ BitVec 8)))
          (and (= x bv!val!2) (= x bv!val!3) (= x bv!val!0) (= x bv!val!1)))

断言是一个连词，听起来很奇怪；这不应该是一种分离吗？我不确定这是否是问题的根本原因，但听起来确实很可疑。

4

1 回答 1

1

Z3有两个问题。首先，您是对的，模型打印机中有错字。它应该是“或”而不是“和”。第二个问题是Z3没有安装位向量理论，被(_ BitVec 8)视为未解释排序。这是预处理器中的一个错误，用于确定问题所在的逻辑。您可以通过在文件开头添加以下命令来解决此错误：

(set-option :auto-config false)

这些错误已得到修复，该修复将在下一个版本中提供。

于 2012-02-24T16:48:29.490 回答