docs/binary/binary.rst

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://smt-lib.org/language.shtml>`_
* `SyGuS-IF <https://sygus-org.github.io/language/>`_


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


.. toctree::
    :hidden:

    quickstart
Add more examples to the documentation (#6569) This PR adds (most of) the existing examples to the documentation, and does some other minor updates on the documentation. Some details: - for consistency, all cpp examples are moved from examples/api to examples/api/cpp - add capabilities for SMT-LIB examples, and two simple smt2 examples - more docs/examples/*.rst files - two new documentation categories: installation (how to obtain, compile and install cvc5) and binary (about the cvc5 binary) 2021-05-26 08:30:45 +02:00			`Binary Documentation`
			`====================`

Various minor docs improvements (#7626) This PR does a number of minor improvements to the docs. 2021-11-11 18:27:53 -08:00			`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
Refactor documentation (#8288) This PR moves some stuff around in our documentation. Most notably, it moves some sections out of the "Binary documentation" to become their own top-level sections. While doing so, it refactors a few things in options and statistics to be more agnostic to the way cvc5 is used. To allow for command-output being used in regular (not auto-generated) documentation, we add a new extension that takes care of injecting the build folder into a new wrapper run-command. 2022-03-21 22:19:11 +01:00			`interface.`

			`The cvc5 binary supports the following input languages:`

Fix broken links to SMT-LIB (#10721) I am getting that the links to SMT-LIB in https://cvc5.github.io/docs/cvc5-1.1.2/ no longer work. This updates the links on main to use a URL that works for me. 2024-05-03 08:38:51 -05:00			* `SMT-LIB v2 <http://smt-lib.org/language.shtml>`_
Update sygus URL in docu (#10287) The old sygus domain seems to be squatted now. In response to issue #10285 2024-01-18 12:32:18 -06:00			* `SyGuS-IF <https://sygus-org.github.io/language/>`_
Refactor documentation (#8288) This PR moves some stuff around in our documentation. Most notably, it moves some sections out of the "Binary documentation" to become their own top-level sections. While doing so, it refactors a few things in options and statistics to be more agnostic to the way cvc5 is used. To allow for command-output being used in regular (not auto-generated) documentation, we add a new extension that takes care of injecting the build folder into a new wrapper run-command. 2022-03-21 22:19:11 +01:00
Various minor docs improvements (#7626) This PR does a number of minor improvements to the docs. 2021-11-11 18:27:53 -08:00
			Alternatively, cvc5 features :doc:`several APIs <../api/api>` for different programming languages.
Add a binary / SMT-LIB quickstart (#7315) This PR adds a binary/SMT-LIBv2 quickstart example, based on the cpp quickstart example. 2021-10-07 11:26:31 -07:00

Add more examples to the documentation (#6569) This PR adds (most of) the existing examples to the documentation, and does some other minor updates on the documentation. Some details: - for consistency, all cpp examples are moved from examples/api to examples/api/cpp - add capabilities for SMT-LIB examples, and two simple smt2 examples - more docs/examples/*.rst files - two new documentation categories: installation (how to obtain, compile and install cvc5) and binary (about the cvc5 binary) 2021-05-26 08:30:45 +02:00			`.. toctree::`
Various improvements and fixes in the documentation (#8551) This PR contains a variety of fixed and improvements to the documentation. 2022-04-04 12:09:47 -07:00			`:hidden:`
Add more examples to the documentation (#6569) This PR adds (most of) the existing examples to the documentation, and does some other minor updates on the documentation. Some details: - for consistency, all cpp examples are moved from examples/api to examples/api/cpp - add capabilities for SMT-LIB examples, and two simple smt2 examples - more docs/examples/*.rst files - two new documentation categories: installation (how to obtain, compile and install cvc5) and binary (about the cvc5 binary) 2021-05-26 08:30:45 +02:00
Add a binary / SMT-LIB quickstart (#7315) This PR adds a binary/SMT-LIBv2 quickstart example, based on the cpp quickstart example. 2021-10-07 11:26:31 -07:00			`quickstart`