代码之家 › 专栏 › 技术社区 › Jivan

z3中的部分解释常量

smt z3

Jivan · 技术社区 · 7 年前

在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))

1 回复 | 直到 7 年前

alias 7 年前

你只需用 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))
)

推荐文章

nyuw · 量词中的非零向量

7 年前

waskyo · 更改z3位向量操作的类型

7 年前

tjhance · z3无量词的数据类型匹配

7 年前

Pushpa · 理解Z3中的量词遍历

7 年前

Pushpa · 将Z3 QBF公式直接转换为pcnf

7 年前

Jivan · z3中的部分解释常量

7 年前

Jivan · 组合z3中给定项集的元素

7 年前

OrenIshShalom · KLEE的Z3无限循环

7 年前

jmite · Z3中的全面评估结果?

7 年前

tyr.bentsen · Z3:表示线性代数性质

7 年前