2

我已经非常仔细地查看了文档和指南，并自己尝试了一些事情。然而，我的问题的解决方案却让我望而却步。

这是本教程关于记录的内容，但我不清楚如何让它适合我的需要：

(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))
(declare-const p1 (Pair Int Int))
(declare-const p2 (Pair Int Int))

我正在寻找用于声明5 个字段、2 个整数和 3 个布尔值的记录的 SMT-LIB2 语法。

然后我想要一个数组/一组这些记录。

我还在寻找我将用来在某些记录集上创建 $\forall$ 语句的语法。

我尽力利用所提供的资源，但一无所获。

谢谢。

4

1 回答 1

3

以下是如何使用 2 个整数和 3 个布尔值创建记录：

(declare-datatypes () ((R5 (mk-R5 (el1 Int) (el2 Int) (el3 Bool) (el4 Bool) (el5 Bool)))))

(declare-const r1 R5)
(declare-const r2 R5)

(assert (not (= r1 r2)))

(check-sat)
(get-model)

Z3 回应：

sat
(model
  (define-fun r2 () R5
    (mk-R5 1 0 false false false))
  (define-fun r1 () R5
    (mk-R5 0 0 false false false))
)

希望这会让你开始。关于量词，它类似于所有其他量词的用法；最好提出具体问题以获得更好的答案。

于 2017-01-05T19:25:07.247 回答