diff options
Diffstat (limited to 'docs/binary/binary.rst')
| -rw-r--r-- | docs/binary/binary.rst | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/docs/binary/binary.rst b/docs/binary/binary.rst index 91e2493e7..44a177afb 100644 --- a/docs/binary/binary.rst +++ b/docs/binary/binary.rst @@ -1,11 +1,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 |