New C++ Api: Initial setup of Api documentation. (#6295)

This configures the initial setup for generating Api documentation with
Sphinx via Breathe and Doxygen. All fixes in the documentation of the
cvc5.h header are for the purpose of eliminating warnings. This PR does
not check for completeness of the documentation, and does not yet tweak
the documentation to be nice, beautiful and consistent, which is
postponed to future PRs.

Configure with `--docs`, and then make. This will generate a `docs`
directory in the build directory. The Sphinx documentation can be found
at `build/docs/sphinx/index.html`. Doxygen documentation is only
generated as xml under `build/docs/doxygen`.

This PR further proposes a new style for copyright headers. If this
style is approved, I will submit a PR to update the update_copyright.pl
script.

1 files changed, 17 insertions, 13 deletions

diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 188c8d0b6..e149770fa 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -1,18 +1,16 @@
-/*********************                                                        */
-/*! \file cvc5_kind.h
- ** \verbatim
+/***
  ** Top contributors (to current version):
  **   Aina Niemetz, Andrew Reynolds, Makai Mann
- ** This file is part of the CVC4 project.
+ ** This file is part of the cvc5 project.
  ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief The term kinds of the CVC4 C++ API.
- **
- ** The term kinds of the CVC4 C++ API.
- **/
+ ** directory for licensing information.
+ */
+
+/**
+ * The term kinds of the cvc5 C++ API.
+ */
 
 #include "cvc4_export.h"
 
@@ -152,7 +150,9 @@ enum CVC4_EXPORT Kind : int32_t
    * (see https://planetmath.org/hilbertsvarepsilonoperator) if there is no x
    * that satisfies F. But if such x exists, the witness operator does not
    * enforce the axiom that ensures uniqueness up to logical equivalence:
-   * forall x. F \equiv G => witness x. F =  witness x. G
+   * \verbatim
+   *   forall x. F \equiv G => witness x. F =  witness x. G
+   * \endverbatim
    *
    * For example if there are 2 elements of type T that satisfy F, then the
    * following formula is satisfiable:
@@ -1564,7 +1564,9 @@ enum CVC4_EXPORT Kind : int32_t
   CONST_ARRAY,
   /**
    * Equality over arrays a and b over a given range [i,j], i.e.,
-   * \forall k . i <= k <= j --> a[k] = b[k]
+   * \verbatim
+   *   \forall k . i <= k <= j --> a[k] = b[k]
+   * \endverbatim
    *
    * Parameters: 4
    *   -[1]: First array
@@ -1956,7 +1958,9 @@ enum CVC4_EXPORT Kind : int32_t
    * A set comprehension is specified by a bound variable list x1 ... xn,
    * a predicate P[x1...xn], and a term t[x1...xn]. A comprehension C with the
    * above form has members given by the following semantics:
-   * forall y. ( exists x1...xn. P[x1...xn] ^ t[x1...xn] = y ) <=> (member y C)
+   * \verbatim
+   *  forall y. ( exists x1...xn. P[x1...xn] ^ t[x1...xn] = y ) <=> (member y C)
+   * \endverbatim
    * where y ranges over the element type of the (set) type of the
    * comprehension. If t[x1..xn] is not provided, it is equivalent to y in the
    * above formula.