Examples

Examples are available in the test-suite/ folder of the source code. Do ./configure.sh and make to compile each of them.

Toys

Short examples you can play with. They illustrate the functionalities of Cybele.

Transitivity

Proves inequalities using transitivity. The non-deterministic choices of hypothesis can be pre-computed in OCaml.

Congruence

Decides equalities over first-order terms using the congruence-closure algorithm. Relies on an union-find easily implemented using references.

Lattice

Decides inequalities overs lattices using the Whitman algorithm. The non-deterministic choices can be pre-computed in OCaml. This is thus faster than the implementation of James and Hinze.