Documentation for using SPACER

[shazqadeer]

Where can I find documentation for using Spacer (or any CHC solving) in Z3?

[agurfinkel]

I'm not sure we have a single source of documentation. It depends on what you want to do.

Here is a Jupyter notebook from a SYNASC Tutorial Nikolaj and I did a year ago. It shows various things you can do through the API: https://github.com/agurfinkel/spacer-on-jupyter/blob/master/Dagstuhl2019.ipynb

If you want to use SMT-LIB interface, there is documentation and benchmarks at chc-comp: https://chc-comp.github.io/
In particular, https://chc-comp.github.io/format.html

There is also a repo of useful tools to manipulate and convert between formats: https://github.com/chc-comp/chc-tools

If all of these fail you, email me or ask here.