CHC Tools

Tools to manipulate CHC

Here are some of the utilities that would be nice to have:

1. chc2rules -- convert CHC smt-lib to Z3 rules extensions
2. rules2chc -- convert Z3-rules to CHC smt-lib
3. chc2ts -- convert CHC/Rules to Transition System (only possible for linear CHC)
4. chc2btor -- convert to btor format
5. btor2chc -- convert btor to chc
6. chc_is_model -- check wether a given M is a model for CHC C
7. chc_is_refute -- check whether a given refutation R is a refutation for a given CHC C
8. ts_is_invar -- check whether given model is an inductive invariant of a Ts
9. ts_is_trace -- check whether a given trace is a counterexample of a Ts
10. chcstats -- statistic
11. chcpp -- pretty printing