blob: 44a177afb0d32f0d649632a10a1cdb78d951fbbc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
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, but cvc5 also supports other :doc:`input languages <languages>`.
The behavior of cvc5 can be changed with a number of :doc:`options <options>`, and :doc:`output tags <output-tags>` allow to extract structured information about the solving process.
Alternatively, cvc5 features :doc:`several APIs <../api/api>` for different programming languages.
.. toctree::
:maxdepth: 2
quickstart
languages
options
output-tags
|
