z3 中部分解释的 Const

Question

在 z3 中，可以像这样声明一个完全未解释的 const：

(declare-const x Int)

类似地，可以像这样定义一个完全解释的：

(define-fun y () Int 3)
; y == 3

给定一个代数数据类型，可以有一个完全解释的元组，如下所示：

(declare-datatypes () ((Item (mk-item (size Int) (weight Int)))))
(define-fun z () Item (mk-item 3 4))
; z == Item(size=3, weight=4)

... 或如下所示的非解释型：

(declare-const i1 (Item Int Int))

现在是否可以使用部分解释的数据类型，以便根据前面的示例，每个项目的 weight 都是固定的，而 size 可能会有所不同？

; (bad syntax, but I hope you get the idea)
; in this case the size is varying, but weight is fixed to 5
(declare-const i2 (Item Int 5))

Answer 1

您应该简单地用 declare-fun 声明它并断言您知道的部分相等：

(declare-datatypes () ((Item (mk-item (size Int) (weight Int)))))

(declare-fun x () Item)
(assert (= (weight x) 5))

(check-sat)
(get-model)

这会产生：

sat
(model
  (define-fun x () Item
    (mk-item 0 5))
)

Partially interpreted Const in z3