Examples are available in the
test-suite/ folder of the source code. Do
make to compile each of them.
Short examples you can play with. They illustrate the functionalities of Cybele.
Proves inequalities using transitivity. The non-deterministic choices of hypothesis can be pre-computed in OCaml.
Decides equalities over first-order terms using the congruence-closure algorithm. Relies on an union-find easily implemented using references.