Commit Graph

6 Commits

Author SHA1 Message Date
Mathias Preiner
d01e59c13b Update copyright headers for release 1.0 (#8539) 2022-04-05 20:38:57 +00:00
Mathias Preiner
bbcd471ed4 Introduce internal namespace and remove api namespace. (#8443)
The public cvc5 API now lives in the cvc5 namespace. All internal parts were moved into the (new) internal namespace.
The final hierarchy will be as follows:

cvc5
  ~~ public API
  ::context
  ::internal
  ::parser
  ::main

After this PR it will be:

cvc5
  ~~ public API
  ::internal
      ::context
      ::main
  ::parser
2022-03-29 23:23:01 +00:00
Andrew Reynolds
2f1483e2e3 Remove unecessary methods from the API (#8260)
Removes checkEntailed from Solver.
Removes isEntailed, isNotEntailed, isEntailedUnknown from Result.
Removes isSubsortOf, isFunctionLike, getUninterpretedSortName, getSortConstructorName from Sort.

Updates examples and unit tests.
2022-03-14 18:29:30 +00:00
Andrew Reynolds
4972960da7 Check for free variables in several SolverEngine calls (#8130)
Fixes the nightlies due to ensuring that a unit test fails in production (it was failing only in debug).

Fixes #8127.
2022-02-24 18:28:58 +00:00
Haniel Barbosa
59bbcb5aa5 CVC4 -> cvc5 in cpp API examples (#6746) 2021-06-15 18:29:08 +00:00
Gereon Kremer
7440f0568b 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 06:30:45 +00:00