Add more examples to the documentation (#6569)
authorGereon Kremer <nafur42@gmail.com>
Wed, 26 May 2021 06:30:45 +0000 (08:30 +0200)
committerGitHub <noreply@github.com>
Wed, 26 May 2021 06:30:45 +0000 (06:30 +0000)
commit7440f0568b99842d87cb1f86eec21aed9f46b92a
tree1fa6a41efcf4bb0946bac7ea43abc8cdcbd2a0c8
parent14b4666bec5cf6a8058254d740e94eda388f4760
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)
61 files changed:
docs/binary/binary.rst [new file with mode: 0644]
docs/binary/options.rst [new file with mode: 0644]
docs/conf.py.in
docs/cpp/cpp.rst
docs/examples/bitvectors.rst [new file with mode: 0644]
docs/examples/bitvectors_and_arrays.rst [new file with mode: 0644]
docs/examples/combination.rst [new file with mode: 0644]
docs/examples/datatypes.rst
docs/examples/examples.rst
docs/examples/exceptions.rst [new file with mode: 0644]
docs/examples/extract.rst [new file with mode: 0644]
docs/examples/floatingpoint.rst [new file with mode: 0644]
docs/examples/helloworld.rst
docs/examples/lineararith.rst
docs/examples/sequences.rst [new file with mode: 0644]
docs/examples/sets.rst [new file with mode: 0644]
docs/examples/strings.rst [new file with mode: 0644]
docs/examples/sygus-fun.rst [new file with mode: 0644]
docs/examples/sygus-grammar.rst [new file with mode: 0644]
docs/examples/sygus-inv.rst [new file with mode: 0644]
docs/ext/examples.py
docs/genindex.rst [new file with mode: 0644]
docs/index.rst
docs/installation/installation.rst [new file with mode: 0644]
docs/options.rst [deleted file]
docs/python/python.rst
examples/CMakeLists.txt
examples/api/CMakeLists.txt [deleted file]
examples/api/bitvectors.cpp [deleted file]
examples/api/bitvectors_and_arrays.cpp [deleted file]
examples/api/combination.cpp [deleted file]
examples/api/cpp/CMakeLists.txt [new file with mode: 0644]
examples/api/cpp/bitvectors.cpp [new file with mode: 0644]
examples/api/cpp/bitvectors_and_arrays.cpp [new file with mode: 0644]
examples/api/cpp/combination.cpp [new file with mode: 0644]
examples/api/cpp/datatypes.cpp [new file with mode: 0644]
examples/api/cpp/extract.cpp [new file with mode: 0644]
examples/api/cpp/helloworld.cpp [new file with mode: 0644]
examples/api/cpp/linear_arith.cpp [new file with mode: 0644]
examples/api/cpp/sequences.cpp [new file with mode: 0644]
examples/api/cpp/sets.cpp [new file with mode: 0644]
examples/api/cpp/strings.cpp [new file with mode: 0644]
examples/api/cpp/sygus-fun.cpp [new file with mode: 0644]
examples/api/cpp/sygus-grammar.cpp [new file with mode: 0644]
examples/api/cpp/sygus-inv.cpp [new file with mode: 0644]
examples/api/cpp/utils.cpp [new file with mode: 0644]
examples/api/cpp/utils.h [new file with mode: 0644]
examples/api/datatypes.cpp [deleted file]
examples/api/extract.cpp [deleted file]
examples/api/helloworld.cpp [deleted file]
examples/api/linear_arith.cpp [deleted file]
examples/api/sequences.cpp [deleted file]
examples/api/sets.cpp [deleted file]
examples/api/smtlib/helloworld.smt2 [new file with mode: 0644]
examples/api/smtlib/linear_arith.smt2 [new file with mode: 0644]
examples/api/strings.cpp [deleted file]
examples/api/sygus-fun.cpp [deleted file]
examples/api/sygus-grammar.cpp [deleted file]
examples/api/sygus-inv.cpp [deleted file]
examples/api/utils.cpp [deleted file]
examples/api/utils.h [deleted file]