isla-cat 🐱

isla-cat 是一个Rust库，用于将用于描述硬件松散内存模型的herd（herd）的cat文件转换为适用于Z3和CVC4等SMT求解器的形式。

它还包含一个小型二进制程序 cat2smt，该程序可以在命令行上翻译此类cat文件。

关于cat语言的文档可以在 这里 找到。

许可

catlib子目录中的 .cat 文件在herd（LICENSE.txt）下采用CeCILL-B许可。

tests目录中的 .cat 文件同样在CeCILL-B许可下，但 aarch64.cat 在ARM Ltd.下采用3-clause BSD许可。

限制

cat有一些特性不易（甚至根本不可能）转换为SMT。粗略地说，这支持定义事件集合和关系的cat片段。更正式地说，我们支持的cat片段由以下语法定义

expr ::= 0
       | id
       | expr? | expr^-1
       | ~expr
       | [expr]
       | expr | expr
       | expr ; expr | expr \ expr | expr & expr | expr * expr
       | expr expr
       | let id = expr in expr
       | ( expr )

binding ::= id = expr

closure_binding ::= id = expr^+
                  | id = expr^*

id ::= [a-zA-Z_][0-9a-z_.-]*

def ::= let binding { and binding }
      | let closure_binding
      | let funbinding
      | include string
      | show expr as id
      | show id {, id }
      | unshow id {, id }
      | [ flag ] check expr [ as id ]

funbinding ::= id ( id ) = expr

check ::= checkname | ~checkname

checkname ::= acyclic | irreflexive | empty