smt - 为什么CVC4产品运营商不适用于套装?
问题描述
我正在修改 CVC4 对集合和关系的支持,并希望能够使用product
运算符来构建两个集合的笛卡尔积。但是,此运算符仅适用于关系。
这是馈送到 CVC4 的示例输入:
(set-logic ALL_SUPPORTED)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun es1 () (Set S1))
(declare-fun es2 () (Set S2))
(declare-fun es1s2 () (Set (Tuple S1 S2)))
(assert (= es1s2 (product es1 es2)))
这会导致以下错误消息:
(error " Relational operator operates on non-relations (sets of tuples)")
然后我发现 CVC4 期望product
运算符适用于元组集。以下处理成功:
(set-logic ALL_SUPPORTED)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun e1 () (Set (Tuple S1)))
(declare-fun e2 () (Set (Tuple S2)))
(declare-fun es1s2 () (Set (Tuple S1 S2)))
(assert (= es1s2 (product e1 e2)))
CVC4 可以在这里将集合视为具有该集合元素的 1 元组的集合。
- 是否有任何基本问题阻止它发生这种行为?
解决方案
这就是语法在 CVC4 中的工作方式。我在工作中使用它,我们专门处理集合论。对于具有有限关系的集合上的大多数操作,CVC4 期望有元组。
这个链接可能会有所帮助:https ://cvc4.github.io/sets-and-relations 所以,有限集的操作通常可以在没有元组的情况下进行,而有限关系需要元组。
另外,我发现这篇论文有助于理解 CVC4 中 set 实现背后的理论:https ://homepage.cs.uiowa.edu/~tinelli/papers/MenEtAl-CADE-17.pdf
推荐阅读
- pandas - 用于数据处理和作业调度的 Apache Airflow 或 Apache Beam
- c - 返回列表中的第一个节点
- vba - 如何在 Range 中使用变量?
- html - html iframe 创建一个白色背景
- java - 从 mysql blob 中读取 java.io.File
- unix - 在 unix 中将文本附加到文件的最后一行
- paw-app - 如何使用 Mac 的 PAW API 工具将变量用作 URL 参数?
- php - PHP - 重定向到上一页
- css - JavaFX 按钮周围有烦人的空白
- centos - Ansible:我需要使用一个循环中的变量,并独立使用每个变量