marciopocebon / etb

The Evidential Tool Bus

Evidential Tool Bus (ETB)

See the file INSTALL for installation instruction, in particular external dependencies required to get ETB running.

The demos/ directory contains demos of ETB:

• 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

The doc/ directory contains the documentation, including reference manuals

The src/ directory contains the source code (see the README there for more details)

The tests/ directory contains test scripts