Binary Documentation
====================

The easiest way to use cvc5 is usually to invoke the cvc5 binary via the command line.
The :doc:`quickstart guide <quickstart>` gives a short introduction on how to use cvc5 via the SMT-LIBv2
interface.

The cvc5 binary supports the following input languages:

* `SMT-LIB v2 <http://smtlib.cs.uiowa.edu/language.shtml>`_
* `SyGuS-IF <https://sygus.org/language/>`_
* `TPTP <http://www.tptp.org/>`_


Alternatively, cvc5 features :doc:`several APIs <../api/api>` for different programming languages.


.. toctree::
    :hidden:

    quickstart