z3 - 在 z3 中定义 Set

Question

要在 Z3 中创建一组 3 个元素 (1,2,3)，我使用以下代码：

(define-sort Set () ( Array Int Bool ) )
(declare-const s Set ) 
( assert  ( and ( = ( select s 1 ) true )  ( = ( select s 2 ) true ) 
           ( = ( select s 3 ) true )  ) )

我得到的模型如下：

(model 
  (define-fun s () (Array Int Bool)
    (_ as-array k!0))
  (define-fun k!0 ((x!1 Int)) Bool
    (ite (= x!1 2) true
    (ite (= x!1 3) true
    (ite (= x!1 1) true
      true))))
)

但相反，我怎样才能获得表格的模型：

(model    (define-fun s () (Array Int Bool)
    (_ as-array k!0))   (define-fun k!0 ((x!1 Int)) Bool
    (ite (= x!1 2) true
    (ite (= x!1 3) true
    (ite (= x!1 1) true
      false)))) )

以便集合成员以外的元素不包含在集合中。

Answer 1

您可以通过从空集开始来实现这一点，即定义为false无处不在的数组。

这是一个例子：

(declare-const s1 (Array Int Bool))

(assert (= s1
  (store
    (store
      (store 
        ((as const (Array Int Bool)) false)
        1 true)
      2 true)
    3 true)
))

(check-sat)
(get-model)