1

当我组合数组和量词时，Z3 通常会生成包含array-ext. 例如，此测试用例生成以下模型：

(define-fun pipeid () (Array Int Int)
  (_ as-array k!2))
(define-fun valid () (Array Int Bool)
  (_ as-array k!0))
(define-fun ispipe () (Array Int Bool)
  (_ as-array k!1))
(define-fun pipeid_ab () Int
  2)
(define-fun fd () Int
  0)
(define-fun k!3 ((x!1 Int)) Int
  (ite (= x!1 0) 0
    (array-ext (_ as-array k!0) (_ as-array k!1))))
(define-fun k!0!4 ((x!1 Int)) Bool
  (ite (= x!1 3) false
    true))
(define-fun k!0 ((x!1 Int)) Bool
  (k!0!4 (k!3 x!1)))
(define-fun k!1 ((x!1 Int)) Bool
  true)
(define-fun k!2!5 ((x!1 Int)) Int
  (ite (= x!1 3) 4
    1))
(define-fun k!2 ((x!1 Int)) Int
  (k!2!5 (k!3 x!1)))

首先，array-extink!3是什么意思？我拼凑了(array-ext a b)一些索引x，其中a [ x ] != b [ x ]，但要么我拼凑的内容不正确，要么我无法理解以上的循环k!0定义k!3。

其次，如何从这些模型中提取具体值？我知道通常不可能直接在模型中表示数组的具体值，但我想至少了解它的具体值是什么，并能够以某种形式从模型中提取它。即使查询单个数组索引似乎也无济于事：

 model.evaluate(pipeid[1]) => If(array-ext(as-array, as-array) = 3, 4, 1)

谢谢。

4

1 回答 1

2

array-ext是内部功能符号。它用于实现数组扩展性。话虽如此，它不应该出现在模型中。基于模型的量词实例化 (MBQI) 模块意外地“泄漏”array-ext到模型中。我解决了这个问题。

该修复程序已在unstable（进行中的）分支中可用。它也将在每晚构建中可用。

这是修复错误后的输出：

(define-fun pipeid () (Array Int Int)
  (_ as-array k!2))
(define-fun valid () (Array Int Bool)
  (_ as-array k!0))
(define-fun ispipe () (Array Int Bool)
  (_ as-array k!1))
(define-fun pipeid_ab () Int
  2)
(define-fun fd () Int
  0)
(define-fun k!3 ((x!1 Int)) Int
  0)
(define-fun k!0!4 ((x!1 Int)) Bool
  (ite (= x!1 3) false
    true))
(define-fun k!0 ((x!1 Int)) Bool
  (k!0!4 (k!3 x!1)))
(define-fun k!1 ((x!1 Int)) Bool
  true)
(define-fun k!2!5 ((x!1 Int)) Int
  (ite (= x!1 3) 4
    1))
(define-fun k!2 ((x!1 Int)) Int
  (k!2!5 (k!3 x!1)))
pipeid[0] => 1
pipeid[1] => 1
于 2013-06-21T01:03:46.823 回答