证据工具总线。
EvidentialToolBus的Python项目详细描述
证据工具总线提供
请参阅文件install以获取安装说明,特别是 运行ETB所需的外部依赖项。
demos/目录包含etb的demos:
- allsat/ implements an ALLSAT solver using the ETB on top of the yices SMT solver.
- allsat2/ implements an ALLSAT solver using the ETB on top of the yices2 SMT solver.
- make/ shows how to use the ETB to implement a distributed make tools that keeps track of all dependencies between source and objects files.
- k-induction/ shows two ways to implement a simple k-induction procedure on top of the ETB. It shows how derivation rules can be used to establish a fact, and inference rules can be used to extract a proof of that fact.
- hybridSal/ shows how to integrate separate tools in a complete workflow.
- vc/ shows a demo of a wrapper that dynamically creates lemmata (generated clauses)
- blackwhite/ shows a demo of the pure Datalog with recursion but without any wrappers
文档包含文档,包括参考手册
src包含源代码(有关详细信息,请参阅此处的自述文件)
测试包含测试脚本