库介绍

razor-fol：一个用于解析和语法处理一阶（逻辑）公式的库。
razor-chase：一个用于构造一阶理论模型的库。剃刀：一阶理论的模型发现工具。

Github地址

https://github.com/salmans/rusty-razor

运行

solve

使用solve命令查找<input>文件中编写的理论模型：

razor solve -i <input>

--count参数限制了要构建的模型的数量：

razor solve -i <input> --count <number>

有界模型查找

与传统的模型查找器（例如Alloy）不同，Razor不需要用户为其构造的模型的大小提供界限。但是，当在带有无限的模型的理论上运行时，Razor进程可能永远不会终止。可以证明，在不满足要求的理论（即，没有模型的理论）上运行非常长的时间之后，Razor可以保证能够终止（尽管这可能需要很长时间才能完成）这是一阶逻辑的半判定性的直接结果。

为了保证有穷性，请使用--bound 带有domain参数值的命令，通过结果模型的元素数量限制结果模型的大小：

razor solve -i <input> --bound domain=<number>