2

根据秒。SMT-LIBv2 Language and Tools: A Tutorial 的3.9.3 可以在 SMT-LIBv2中声明这样的复合排序：

(set-logic QF_UF)
(declare-sort Triple 3)
(declare-fun state () (Triple Bool Bool Bool))

我正在使用 CVC4，它似乎接受这种语法。但是我如何访问这些元素？我尝试了以下方法（以及我在网上找到的各种变体）：

(assert (_ state 1))
(assert (select 1 state))

但看起来这些运算符只适用于向量和数组。我找不到任何使用这种复合排序的示例，也找不到有关在教程或语言标准中访问这些元素的任何内容。它是如何完成的？还是我完全误解了这个功能的用途？

我的应用程序：我想对一个时间问题进行编码，并希望以将旧状态转换为新状态的状态转换函数的形式进行编码，因此我可以在试验系统时编写如下内容：

....
(declare-fun initial_state () MyStateSort)
(declare-fun state_after_step_1 () MyStateSort)
(declare-fun state_after_step_2 () MyStateSort)
(assert (= (MyTransitionFunc initial_state) state_after_step_1)
(assert (= (MyTransitionFunc state_after_step_1) state_after_step_2)
4

1 回答 1

0

这是我自己的问题的答案。如果任何人都可以发布一个用户定义排序的用例示例，其中 arity > 0，我会很乐意接受这个答案。

在更仔细地阅读了 SMT-LIBv2 标准之后，我现在认为 arity > 0 的排序声明仅适用于理论定义（用于声明类似 的排序Array），而不是用户提供的代码。David Cok 的教程中的示例似乎具有误导性，因为它表明这可用于声明复合排序。我在其他任何地方都没有发现任何迹象。这包括完整的 SMT-LIB 基准测试，其中不包含一个数量 > 0 的排序声明。

应该使用未解释的函数来创建复杂数据结构的等价物，而不是“复合排序”。例子：

(set-logic QF_UF)
(declare-sort CONTAINER_SORT 0)
(declare-fun CONTAINER_MEMBER_1 (CONTAINER_SORT) Bool)
(declare-fun CONTAINER_MEMBER_2 (CONTAINER_SORT) Bool)
(declare-fun INSTANCE_1 () CONTAINER_SORT)
(declare-fun INSTANCE_2 () CONTAINER_SORT)

这将有效地声明以下 4 个独立的 Bool 表达式。

(CONTAINER_MEMBER_1 INSTANCE_1)
(CONTAINER_MEMBER_2 INSTANCE_1)

(CONTAINER_MEMBER_1 INSTANCE_2)
(CONTAINER_MEMBER_2 INSTANCE_2)
于 2014-12-24T15:53:36.820 回答