docs: Remove api namespace. (#8455)

diff --git a/docs/api/cpp/CMakeLists.txt b/docs/api/cpp/CMakeLists.txt
index 4d637dee029c64f380fab96430105f3eb1b2fbfa..daa117997d68eaa6ad4885277c26291229f8971d 100644 (file)
--- a/docs/api/cpp/CMakeLists.txt
+++ b/docs/api/cpp/CMakeLists.txt
@@ -17,9 +17,12 @@ find_package(Doxygen REQUIRED)
 # basic parameters
 set(DOXYGEN_INPUT_DIR ${PROJECT_SOURCE_DIR}/src/api/cpp)
 set(DOXYGEN_OUTPUT_DIR ${CMAKE_CURRENT_BINARY_DIR}/doxygen)
-set(DOXYGEN_INPUT
-    "${DOXYGEN_INPUT_DIR}/cvc5.h ${DOXYGEN_INPUT_DIR}/cvc5_kind.h ${PROJECT_SOURCE_DIR}/src/proof/proof_rule.h"
-)
+set(DOXYGEN_INPUT "\
+${DOXYGEN_INPUT_DIR}/cvc5.h \
+${DOXYGEN_INPUT_DIR}/cvc5_kind.h \
+${DOXYGEN_INPUT_DIR}/cvc5_types.h \
+${PROJECT_SOURCE_DIR}/src/proof/proof_rule.h \
+")
 set(DOXYGEN_INDEX_FILE ${DOXYGEN_OUTPUT_DIR}/xml/index.xml)
 
 # create doxygen config file
@@ -38,6 +41,7 @@ add_custom_command(
   DEPENDS
     ${DOXYGEN_INPUT_DIR}/cvc5.h
     ${DOXYGEN_INPUT_DIR}/cvc5_kind.h
+    ${DOXYGEN_INPUT_DIR}/cvc5_types.h
     ${PROJECT_SOURCE_DIR}/src/proof/proof_rule.h
   COMMENT "Generating doxygen API docs"
 )

diff --git a/docs/api/cpp/cpp.rst b/docs/api/cpp/cpp.rst
index 67f2c805304e79ff537d8b9ae3d0791638d0a597..f51f55756be55351cf6233fd9b3b851a8afc7d8e 100644 (file)
--- a/docs/api/cpp/cpp.rst
+++ b/docs/api/cpp/cpp.rst
@@ -2,8 +2,8 @@ C++ API
 =====================
 
 The C++ API is the primary interface for cvc5 and exposes the full functionality of cvc5.
-The :doc:`quickstart guide <quickstart>` gives a short introduction, while the following class hierarchy of the ``cvc5::api`` namespace provides more details on the individual classes.
-For most applications, the :cpp:class:`Solver <cvc5::api::Solver>` class is the main entry point to cvc5.
+The :doc:`quickstart guide <quickstart>` gives a short introduction, while the following class hierarchy of the ``cvc5`` namespace provides more details on the individual classes.
+For most applications, the :cpp:class:`Solver <cvc5::Solver>` class is the main entry point to cvc5.
 
 
 .. container:: hide-toctree
@@ -33,17 +33,17 @@ For most applications, the :cpp:class:`Solver <cvc5::api::Solver>` class is the
 Class hierarchy
 ^^^^^^^^^^^^^^^
 
-``namespace cvc5::api {``
+``namespace cvc5 {``
 
-  * class :cpp:class:`CVC5ApiException <cvc5::api::CVC5ApiException>`
-  * class :cpp:class:`CVC5ApiRecoverableException <cvc5::api::CVC5ApiRecoverableException>`
+  * class :cpp:class:`CVC5ApiException <cvc5::CVC5ApiException>`
+  * class :cpp:class:`CVC5ApiRecoverableException <cvc5::CVC5ApiRecoverableException>`
   * class :ref:`api/cpp/datatype:datatype`
 
-    * class :cpp:class:`const_iterator <cvc5::api::Datatype::const_iterator>`
+    * class :cpp:class:`const_iterator <cvc5::Datatype::const_iterator>`
 
   * class :ref:`api/cpp/datatypeconstructor:datatypeconstructor`
 
-    * class :cpp:class:`const_iterator <cvc5::api::DatatypeConstructor::const_iterator>`
+    * class :cpp:class:`const_iterator <cvc5::DatatypeConstructor::const_iterator>`
 
   * class :ref:`api/cpp/datatypeconstructordecl:datatypeconstructordecl`
   * class :ref:`api/cpp/datatypedecl:datatypedecl`
@@ -54,16 +54,16 @@ Class hierarchy
   * class :ref:`api/cpp/optioninfo:optioninfo`
   * class :ref:`api/cpp/result:result`
 
-    * enum :cpp:enum:`UnknownExplanation <cvc5::api::Result::UnknownExplanation>`
+    * enum :cpp:enum:`UnknownExplanation <cvc5::Result::UnknownExplanation>`
 
   * class :ref:`api/cpp/roundingmode:roundingmode`
   * class :ref:`api/cpp/solver:solver`
   * class :ref:`api/cpp/sort:sort`
-  * class :cpp:class:`Stat <cvc5::api::Stat>`
-  * class :cpp:class:`Statistics <cvc5::api::Statistics>`
+  * class :cpp:class:`Stat <cvc5::Stat>`
+  * class :cpp:class:`Statistics <cvc5::Statistics>`
   * class :ref:`api/cpp/synthresult:synthresult`
   * class :ref:`api/cpp/term:term`
 
-    * class :cpp:class:`const_iterator <cvc5::api::Term::const_iterator>`
+    * class :cpp:class:`const_iterator <cvc5::Term::const_iterator>`
 
 ``}``

diff --git a/docs/api/cpp/datatype.rst b/docs/api/cpp/datatype.rst
index 7c5325ec1061b5ba8c9dc699dbc8fa1b500f26ba..3fc4e284f04571ea85715714035fc47022248429 100644 (file)
--- a/docs/api/cpp/datatype.rst
+++ b/docs/api/cpp/datatype.rst
@@ -1,7 +1,7 @@
 Datatype
 ========
 
-.. doxygenclass:: cvc5::api::Datatype
+.. doxygenclass:: cvc5::Datatype
     :project: cvc5
     :members:
     :undoc-members:

diff --git a/docs/api/cpp/datatypeconstructor.rst b/docs/api/cpp/datatypeconstructor.rst
index 90b48e8e1c3043a631f3c13bd3970b2e987ab00f..1b9a7876ecf24fb42a73ad38623723a182fae81e 100644 (file)
--- a/docs/api/cpp/datatypeconstructor.rst
+++ b/docs/api/cpp/datatypeconstructor.rst
@@ -1,7 +1,7 @@
 DatatypeConstructor
 ===================
 
-.. doxygenclass:: cvc5::api::DatatypeConstructor
+.. doxygenclass:: cvc5::DatatypeConstructor
     :project: cvc5
     :members:
     :undoc-members:

diff --git a/docs/api/cpp/datatypeconstructordecl.rst b/docs/api/cpp/datatypeconstructordecl.rst
index 7cb5b6a8c0dbb95059acf4b351392764f793e7d0..9161d4dae27ac4351bfb5181c1b0d80c1da6b848 100644 (file)
--- a/docs/api/cpp/datatypeconstructordecl.rst
+++ b/docs/api/cpp/datatypeconstructordecl.rst
@@ -1,7 +1,7 @@
 DatatypeConstructorDecl
 =======================
 
-.. doxygenclass:: cvc5::api::DatatypeConstructorDecl
+.. doxygenclass:: cvc5::DatatypeConstructorDecl
     :project: cvc5
     :members:
     :undoc-members:

diff --git a/docs/api/cpp/datatypedecl.rst b/docs/api/cpp/datatypedecl.rst
index d3927b805b0ab938baa0cd80c2d719e026c32a64..f4f94a430d31bf987b8278ce221246d315e9ad6c 100644 (file)
--- a/docs/api/cpp/datatypedecl.rst
+++ b/docs/api/cpp/datatypedecl.rst
@@ -1,7 +1,7 @@
 DatatypeDecl
 ============
 
-.. doxygenclass:: cvc5::api::DatatypeDecl
+.. doxygenclass:: cvc5::DatatypeDecl
     :project: cvc5
     :members:
     :undoc-members:

diff --git a/docs/api/cpp/datatypeselector.rst b/docs/api/cpp/datatypeselector.rst
index 22ac01aa421390c97c72f041387aff926becf98c..34602a92d9e6fdc4f70ad8d69288954154c7e924 100644 (file)
--- a/docs/api/cpp/datatypeselector.rst
+++ b/docs/api/cpp/datatypeselector.rst
@@ -1,7 +1,7 @@
 DatatypeSelector
 ================
 
-.. doxygenclass:: cvc5::api::DatatypeSelector
+.. doxygenclass:: cvc5::DatatypeSelector
     :project: cvc5
     :members:
     :undoc-members:

diff --git a/docs/api/cpp/exceptions.rst b/docs/api/cpp/exceptions.rst
index 5fa65e5e52dade397176c9698ed9c9c066cd4858..2c62ab40c328b960f5d7c2d39a8d877b98e713a8 100644 (file)
--- a/docs/api/cpp/exceptions.rst
+++ b/docs/api/cpp/exceptions.rst
@@ -3,25 +3,25 @@ Exceptions
 
 The cvc5 API communicates certain errors using exceptions. We broadly
 distinguish two types of exceptions: :cpp:class:`CVC5ApiException
-<cvc5::api::CVC5ApiException>` and :cpp:class:`CVC5ApiRecoverableException
-<cvc5::api::CVC5ApiRecoverableException>` (which is derived from
-:cpp:class:`CVC5ApiException <cvc5::api::CVC5ApiException>`).
+<cvc5::CVC5ApiException>` and :cpp:class:`CVC5ApiRecoverableException
+<cvc5::CVC5ApiRecoverableException>` (which is derived from
+:cpp:class:`CVC5ApiException <cvc5::CVC5ApiException>`).
 
 If any method fails with a :cpp:class:`CVC5ApiRecoverableException
-<cvc5::api::CVC5ApiRecoverableException>`, the solver behaves as if the failing
+<cvc5::CVC5ApiRecoverableException>`, the solver behaves as if the failing
 method was not called. The solver can still be used safely.
 
 If, however, a method fails with a :cpp:class:`CVC5ApiException
-<cvc5::api::CVC5ApiException>`, the associated object may be in an unsafe state
+<cvc5::CVC5ApiException>`, the associated object may be in an unsafe state
 and it should no longer be used.
 
 
-.. doxygenclass:: cvc5::api::CVC5ApiException
+.. doxygenclass:: cvc5::CVC5ApiException
     :project: cvc5
     :members:
     :undoc-members:
 
-.. doxygenclass:: cvc5::api::CVC5ApiRecoverableException
+.. doxygenclass:: cvc5::CVC5ApiRecoverableException
     :project: cvc5
     :members:
     :undoc-members:

diff --git a/docs/api/cpp/grammar.rst b/docs/api/cpp/grammar.rst
index dc7291f67dbc11b73e7dbe623c8c2657786a413f..e5c9493e5d0b5fc20ef2e7cfd9a9e5b39be88e5f 100644 (file)
--- a/docs/api/cpp/grammar.rst
+++ b/docs/api/cpp/grammar.rst
@@ -1,7 +1,7 @@
 Grammar
 =======
 
-.. doxygenclass:: cvc5::api::Grammar
+.. doxygenclass:: cvc5::Grammar
     :project: cvc5
     :members:
     :undoc-members:

diff --git a/docs/api/cpp/kind.rst b/docs/api/cpp/kind.rst
index 996691524cd93627e7206c2da2c90767e85c1bae..f10ed26951393eef5a7b09b73f3dbf7bc7cf0c50 100644 (file)
--- a/docs/api/cpp/kind.rst
+++ b/docs/api/cpp/kind.rst
@@ -1,21 +1,21 @@
 Kind
 ====
 
-Every :cpp:class:`Term <cvc5::api::Term>` has an associated kind.
+Every :cpp:class:`Term <cvc5::Term>` has an associated kind.
 This kind distinguishes if the Term is a value, constant, variable or operator,
 and what kind of each.
 For example, a bit-vector value has kind
-:cpp:enumerator:`CONST_BITVECTOR <cvc5::api::Kind::CONST_BITVECTOR>`,
+:cpp:enumerator:`CONST_BITVECTOR <cvc5::Kind::CONST_BITVECTOR>`,
 a free constant symbol has kind
-:cpp:enumerator:`CONSTANT <cvc5::api::Kind::CONSTANT>`,
+:cpp:enumerator:`CONSTANT <cvc5::Kind::CONSTANT>`,
 an equality over terms of any sort has kind
-:cpp:enumerator:`EQUAL <cvc5::api::Kind::EQUAL>`, and a universally
-quantified formula has kind :cpp:enumerator:`FORALL <cvc5::api::Kind::FORALL>`.
+:cpp:enumerator:`EQUAL <cvc5::Kind::EQUAL>`, and a universally
+quantified formula has kind :cpp:enumerator:`FORALL <cvc5::Kind::FORALL>`.
 
-.. doxygenenum:: cvc5::api::Kind
+.. doxygenenum:: cvc5::Kind
     :project: cvc5
 
-.. doxygenstruct:: std::hash< cvc5::api::Kind >
+.. doxygenstruct:: std::hash< cvc5::Kind >
     :project: std
     :members:
     :undoc-members:

diff --git a/docs/api/cpp/op.rst b/docs/api/cpp/op.rst
index a320125a2caf66ef10745625d6a7881c7efde29c..9034cda3b105cfcb2d1703a35d171cca8e802837 100644 (file)
--- a/docs/api/cpp/op.rst
+++ b/docs/api/cpp/op.rst
@@ -1,11 +1,11 @@
 Op
 ==
 
-.. doxygenclass:: cvc5::api::Op
+.. doxygenclass:: cvc5::Op
     :project: cvc5
     :members:
 
-.. doxygenstruct:: std::hash< cvc5::api::Op >
+.. doxygenstruct:: std::hash< cvc5::Op >
     :project: std
     :members:
     :undoc-members:

diff --git a/docs/api/cpp/optioninfo.rst b/docs/api/cpp/optioninfo.rst
index eb7848210fcf2e535dd644424930d6f18868a103..d1761c5eb52913de8989ac0441f41790cda03074 100644 (file)
--- a/docs/api/cpp/optioninfo.rst
+++ b/docs/api/cpp/optioninfo.rst
@@ -1,6 +1,6 @@
 OptionInfo
 ==========
 
-.. doxygenstruct:: cvc5::api::OptionInfo
+.. doxygenstruct:: cvc5::OptionInfo
     :project: cvc5
     :members:

diff --git a/docs/api/cpp/quickstart.rst b/docs/api/cpp/quickstart.rst
index 88320a508ff9bcbc489939f20f546ec27ce4aee7..66435840a392eeed19e8ee84767675cd45385561 100644 (file)
--- a/docs/api/cpp/quickstart.rst
+++ b/docs/api/cpp/quickstart.rst
@@ -1,7 +1,7 @@
 Quickstart Guide
 ================
 
-First, create a cvc5 :cpp:class:`Solver <cvc5::api::Solver>` instance:
+First, create a cvc5 :cpp:class:`Solver <cvc5::Solver>` instance:
 
 .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp
      :language: cpp
@@ -63,9 +63,9 @@ the constraints.
 The result we get from this satisfiability check is either ``sat``, ``unsat``
 or ``unknown``.
 It's status can be queried via
-:cpp:func:`cvc5::api::Result::isSat`,
-:cpp:func:`cvc5::api::Result::isUnsat` and
-:cpp:func:`cvc5::api::Result::isSatUnknown`.
+:cpp:func:`cvc5::Result::isSat`,
+:cpp:func:`cvc5::Result::isUnsat` and
+:cpp:func:`cvc5::Result::isSatUnknown`.
 Alternatively, it can also be printed.
 
 .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp

diff --git a/docs/api/cpp/result.rst b/docs/api/cpp/result.rst
index 9ba1aaaafb5f3e8c0dcef628050a69092ded26fb..c01e64deb5d802e181f4e891ec8e81a5cce0cf97 100644 (file)
--- a/docs/api/cpp/result.rst
+++ b/docs/api/cpp/result.rst
@@ -1,7 +1,7 @@
 Result
 ======
 
-.. doxygenclass:: cvc5::api::Result
+.. doxygenclass:: cvc5::Result
     :project: cvc5
     :members:
     :undoc-members:

diff --git a/docs/api/cpp/roundingmode.rst b/docs/api/cpp/roundingmode.rst
index a54d1a65c295037c8ffc52856ec10253a2a95f3d..6626157eb166ed65ddff72eec53283f338c59fa1 100644 (file)
--- a/docs/api/cpp/roundingmode.rst
+++ b/docs/api/cpp/roundingmode.rst
@@ -1,10 +1,10 @@
 RoundingMode
 ============
 
-.. doxygenenum:: cvc5::api::RoundingMode
+.. doxygenenum:: cvc5::RoundingMode
     :project: cvc5
 
-.. doxygenstruct:: std::hash< cvc5::api::RoundingMode >
+.. doxygenstruct:: std::hash< cvc5::RoundingMode >
     :project: std
     :members:
     :undoc-members:

diff --git a/docs/api/cpp/solver.rst b/docs/api/cpp/solver.rst
index 17529f09b54cb4b54445a33191908e6332dffa0b..53bb6bd04e21920db4051b57617d779eb46f4f91 100644 (file)
--- a/docs/api/cpp/solver.rst
+++ b/docs/api/cpp/solver.rst
@@ -1,7 +1,7 @@
 Solver
 ======
 
-.. doxygenclass:: cvc5::api::Solver
+.. doxygenclass:: cvc5::Solver
     :project: cvc5
     :members:
     :undoc-members:

diff --git a/docs/api/cpp/sort.rst b/docs/api/cpp/sort.rst
index 7cbf46271e66cc3d3d98a16b1bf50d54d5a7a6b0..528f27bcd8f5c1257b2bf669257533a146329676 100644 (file)
--- a/docs/api/cpp/sort.rst
+++ b/docs/api/cpp/sort.rst
@@ -1,18 +1,18 @@
 Sort
 ====
 
-The :cpp:class:`Sort <cvc5::api::Sort>` class represents the sort of a
-:cpp:class:`Term <cvc5::api::Term>`.
+The :cpp:class:`Sort <cvc5::Sort>` class represents the sort of a
+:cpp:class:`Term <cvc5::Term>`.
 
-A :cpp:class:`Sort <cvc5::api::Sort>` can be hashed (using
-:cpp:class:`std::hash\<cvc5::api::Sort>`) and serialized to an output stream
-(using :cpp:func:`cvc5::api::operator<<()`).
+A :cpp:class:`Sort <cvc5::Sort>` can be hashed (using
+:cpp:class:`std::hash\<cvc5::Sort>`) and serialized to an output stream
+(using :cpp:func:`cvc5::operator<<()`).
 
-Class :cpp:class:`Sort <cvc5::api::Sort>` offers the default constructor
-only to create a null Sort. Instead, the :cpp:class:`Solver <cvc5::api::Solver>`
+Class :cpp:class:`Sort <cvc5::Sort>` offers the default constructor
+only to create a null Sort. Instead, the :cpp:class:`Solver <cvc5::Solver>`
 class provides factory functions for all other sorts, e.g.,
-:cpp:func:`cvc5::api::Solver::getBooleanSort()` for Sort Bool and
-:cpp:func:`cvc5::api::Solver::mkBitVectorSort()` for bit-vector
+:cpp:func:`cvc5::Solver::getBooleanSort()` for Sort Bool and
+:cpp:func:`cvc5::Solver::mkBitVectorSort()` for bit-vector
 sorts.
 
 Sorts are defined as standardized in the SMT-LIB standard for standardized
@@ -21,30 +21,30 @@ theories:
 
 - *Bag* (Multiset)
 
-  - Created with :cpp:func:`cvc5::api::Solver::mkBagSort()`
+  - Created with :cpp:func:`cvc5::Solver::mkBagSort()`
 
 - *Set* (:ref:`Theory of Sets and Relations <theory_reference_sets>`)
 
-  - Created with :cpp:func:`cvc5::api::Solver::mkSetSort()`
+  - Created with :cpp:func:`cvc5::Solver::mkSetSort()`
 
 - *Relation* (:ref:`Theory of Sets and Relations <theory_reference_sets>`)
 
-  - Created with :cpp:func:`cvc5::api::Solver::mkSetSort()` as a set of tuple
+  - Created with :cpp:func:`cvc5::Solver::mkSetSort()` as a set of tuple
     sorts
 
 - *Table*
 
-  - Created with :cpp:func:`cvc5::api::Solver::mkBagSort()` as a bag of tuple
+  - Created with :cpp:func:`cvc5::Solver::mkBagSort()` as a bag of tuple
     sorts
 
-.. doxygenclass:: cvc5::api::Sort
+.. doxygenclass:: cvc5::Sort
     :project: cvc5
     :members:
     :undoc-members:
 
-.. doxygenfunction:: cvc5::api::operator<<(std::ostream& out, const Sort& s)
+.. doxygenfunction:: cvc5::operator<<(std::ostream& out, const Sort& s)
 
-.. doxygenstruct:: std::hash< cvc5::api::Sort >
+.. doxygenstruct:: std::hash< cvc5::Sort >
     :project: std
     :members:
     :undoc-members:

diff --git a/docs/api/cpp/statistics.rst b/docs/api/cpp/statistics.rst
index 77fab9545a97e9578c0e55224ecfa22f3a87d39d..069f2b851c66e0a908876b6254d8c0284ffd18fd 100644 (file)
--- a/docs/api/cpp/statistics.rst
+++ b/docs/api/cpp/statistics.rst
@@ -3,20 +3,20 @@ Statistics
 
 The solver collects a variety of statistics that can be helpful in understanding
 what the solver is doing internally. The entirety of collected statistics are
-represented by a :cpp:class:`Statistics <cvc5::api::Statistics>` object that can
+represented by a :cpp:class:`Statistics <cvc5::Statistics>` object that can
 be obtained from :cpp:func:`Solver::getStatistics()
-<cvc5::api::Solver::getStatistics>`. It is a copy of the internal solver
+<cvc5::Solver::getStatistics>`. It is a copy of the internal solver
 statistics at this point in time.
 
-The :cpp:class:`Statistics <cvc5::api::Statistics>` object is essentially a
+The :cpp:class:`Statistics <cvc5::Statistics>` object is essentially a
 mapping from names (as ``std::string``) to statistic values, represented by the
-:cpp:class:`Stat <cvc5::api::Stat>` class. A :cpp:class:`Stat <cvc5::api::Stat>`
+:cpp:class:`Stat <cvc5::Stat>` class. A :cpp:class:`Stat <cvc5::Stat>`
 can hold values of different types (``int64_t``, ``double``, ``std::string`` and
 histograms) and can be inspected by identifying the type
-(:cpp:func:`Stat::isInt() <cvc5::api::Stat::isInt()>`,
-:cpp:func:`Stat::isDouble() <cvc5::api::Stat::isDouble()>`, etc) and obtaining
-the actual value (:cpp:func:`Stat::getInt() <cvc5::api::Stat::getInt()>`,
-:cpp:func:`Stat::getDouble() <cvc5::api::Stat::getDouble()>`, etc). Histograms
+(:cpp:func:`Stat::isInt() <cvc5::Stat::isInt()>`,
+:cpp:func:`Stat::isDouble() <cvc5::Stat::isDouble()>`, etc) and obtaining
+the actual value (:cpp:func:`Stat::getInt() <cvc5::Stat::getInt()>`,
+:cpp:func:`Stat::getDouble() <cvc5::Stat::getDouble()>`, etc). Histograms
 conceptually count the frequency of different values of an arbitrary type,
 usually an enumeration type. They are represented as ``std::map<std::string,
 uint64_t>`` where the key is the strings representation of one enumeration value
@@ -24,18 +24,18 @@ and the value is the frequency of this particular value.
 
 Statistics are generally categorized into public and internal statistics, and
 furthermore into changed and defaulted statistics. By default, iterating a
-:cpp:class:`Statistics <cvc5::api::Statistics>` object only shows statistics
+:cpp:class:`Statistics <cvc5::Statistics>` object only shows statistics
 that are both public and changed. The :cpp:func:`Statistics::begin()
-<cvc5::api::Statistics::begin()>` method has Boolean flags ``internal`` and
+<cvc5::Statistics::begin()>` method has Boolean flags ``internal`` and
 ``def`` to also show internal statistics and defaulted statistics, respectively.
 
 
-.. doxygenclass:: cvc5::api::Statistics
+.. doxygenclass:: cvc5::Statistics
     :project: cvc5
     :members: get, begin, end
     :undoc-members:
 
-.. doxygenclass:: cvc5::api::Stat
+.. doxygenclass:: cvc5::Stat
     :project: cvc5
     :members:
     :undoc-members:

diff --git a/docs/api/cpp/synthresult.rst b/docs/api/cpp/synthresult.rst
index 1765f48c6f0285025e639d15d4d46243c1436f7e..c65289ba1491c7158dcdf9660a56e55f0b5e8446 100644 (file)
--- a/docs/api/cpp/synthresult.rst
+++ b/docs/api/cpp/synthresult.rst
@@ -1,7 +1,7 @@
 SynthResult
 ===========
 
-.. doxygenclass:: cvc5::api::SynthResult
+.. doxygenclass:: cvc5::SynthResult
     :project: cvc5
     :members:
     :undoc-members:

diff --git a/docs/api/cpp/term.rst b/docs/api/cpp/term.rst
index 1f112a58a5532a79be52c02e9b4e37f851062283..cb7812cacd91c1a1b338ea13897d44cf7722ffa7 100644 (file)
--- a/docs/api/cpp/term.rst
+++ b/docs/api/cpp/term.rst
@@ -1,19 +1,19 @@
 Term
 ====
 
-The :cpp:class:`Term <cvc5::api::Term>` class represents arbitrary expressions that are Boolean or from some of the supported theories. The list of all supported types (or kinds) is given by the :cpp:enum:`Kind <cvc5::api::Kind>` enum.
-The :cpp:class:`Term <cvc5::api::Term>` class provides methods for general inspection (e.g., comparison, retrieve the kind and sort, access sub-terms), but also methods to retrieving constant values for the supported theories (i.e., :code:`is<Type>Value()` and :code:`get<Type>Value()`, which returns the constant values in the best type standard C++ offers).
+The :cpp:class:`Term <cvc5::Term>` class represents arbitrary expressions that are Boolean or from some of the supported theories. The list of all supported types (or kinds) is given by the :cpp:enum:`Kind <cvc5::Kind>` enum.
+The :cpp:class:`Term <cvc5::Term>` class provides methods for general inspection (e.g., comparison, retrieve the kind and sort, access sub-terms), but also methods to retrieving constant values for the supported theories (i.e., :code:`is<Type>Value()` and :code:`get<Type>Value()`, which returns the constant values in the best type standard C++ offers).
 
-Additionally, a :cpp:class:`Term <cvc5::api::Term>` can be hashed (using :cpp:class:`std::hash\<cvc5::api::Term>`) and given to output streams, including terms within standard containers like :code:`std::map`, :code:`std::set`, or :code:`std::vector`.
+Additionally, a :cpp:class:`Term <cvc5::Term>` can be hashed (using :cpp:class:`std::hash\<cvc5::Term>`) and given to output streams, including terms within standard containers like :code:`std::map`, :code:`std::set`, or :code:`std::vector`.
 
-The :cpp:class:`Term <cvc5::api::Term>` only offers the default constructor to create a null term. Instead, the :cpp:class:`Solver <cvc5::api::Solver>` class provides factory functions for all other terms, e.g., :code:`Solver::mkTerm()` for generic terms and :code:`Solver::mk<Type>()` for constant values of a given type.
+The :cpp:class:`Term <cvc5::Term>` only offers the default constructor to create a null term. Instead, the :cpp:class:`Solver <cvc5::Solver>` class provides factory functions for all other terms, e.g., :code:`Solver::mkTerm()` for generic terms and :code:`Solver::mk<Type>()` for constant values of a given type.
 
-.. doxygenclass:: cvc5::api::Term
+.. doxygenclass:: cvc5::Term
     :project: cvc5
     :members:
     :undoc-members:
 
-.. doxygenstruct:: std::hash< cvc5::api::Term >
+.. doxygenstruct:: std::hash< cvc5::Term >
     :project: std
     :members:
     :undoc-members:

diff --git a/docs/api/python/base/kind.rst b/docs/api/python/base/kind.rst
index 9047c1d5790a7b5dee5745e98c9b34d584612bc5..657b89ea2d9b138996fce1fce18ab77963e763b5 100644 (file)
--- a/docs/api/python/base/kind.rst
+++ b/docs/api/python/base/kind.rst
@@ -5,7 +5,7 @@ Every :py:class:`Term <cvc5.Term>` has a kind which represents its type, for
 example whether it is an equality (:py:obj:`Equal <cvc5.Kind.Equal>`), a
 conjunction (:py:obj:`And <cvc5.Kind.And>`), or a bit-vector addtion
 (:py:obj:`BVAdd <cvc5.Kind.BVAdd>`).
-The kinds below directly correspond to the enum values of the C++ :cpp:enum:`Kind <cvc5::api::Kind>` enum.
+The kinds below directly correspond to the enum values of the C++ :cpp:enum:`Kind <cvc5::Kind>` enum.
 
 .. autoclass:: cvc5.Kind
     :members:

diff --git a/docs/conf.py.in b/docs/conf.py.in
index 5817c586e59d1e39111c651e4aa3fdee07c9e9ef..1e6174e851f0ddd30512f84673358961f1dd68af 100644 (file)
--- a/docs/conf.py.in
+++ b/docs/conf.py.in
@@ -133,7 +133,7 @@ mathjax3_config = {
 # -- extension:: breathe -----------------------------------------------------
 breathe_default_project = "cvc5"
 breathe_domain_by_extension = {"h" : "cpp"}
-cpp_index_common_prefix = ["cvc5::api::"]
+cpp_index_common_prefix = ["cvc5::"]
 
 
 # -- extension:: sphinxcontrib.bibtex ----------------------------------------

diff --git a/docs/options.rst b/docs/options.rst
index abcd3b3e90d44902153dd2d548b65b11aacb6013..06567fbc3e6ff7fe24e5cf449f7dbbe0fed1ce6f 100644 (file)
--- a/docs/options.rst
+++ b/docs/options.rst
@@ -5,10 +5,10 @@ cvc5 can be configured at runtime using a wide range of options.
 When cvc5 is used as a binary, options can be set on the command line.
 Also, options can be set and inspected using the respective commands of the input language and the corresponding API functions:
 
-- C++ API: :cpp:func:`setOption() <cvc5::api::Solver::setOption()>`,
-  :cpp:func:`getOption() <cvc5::api::Solver::getOption()>`,
-  :cpp:func:`getOptionNames() <cvc5::api::Solver::getOptionNames()>`,
-  :cpp:func:`getOptionInfo() <cvc5::api::Solver::getOptionInfo()>`
+- C++ API: :cpp:func:`setOption() <cvc5::Solver::setOption()>`,
+  :cpp:func:`getOption() <cvc5::Solver::getOption()>`,
+  :cpp:func:`getOptionNames() <cvc5::Solver::getOptionNames()>`,
+  :cpp:func:`getOptionInfo() <cvc5::Solver::getOptionInfo()>`
 - Java API: ``setOption()``, ``getOption()``, ``getOptionNames()``, ``getOptionInfo()``
 - Base Python API: :py:func:`setOption() <cvc5.Solver.setOption()>`,
   :py:func:`getOption() <cvc5.Solver.getOption()>`,

diff --git a/docs/resource-limits.rst b/docs/resource-limits.rst
index bc20ed10e2574cfef915e6681fec0d04737e23e9..bb4e3fbdfea3edbf1aab805ff849595fb446d370 100644 (file)
--- a/docs/resource-limits.rst
+++ b/docs/resource-limits.rst
@@ -6,8 +6,8 @@ cvc5 supports limiting the time or *resources* it uses during solving via the op
 :ref:`rlimit <lbl-option-rlimit>`, and :ref:`rlimit-per <lbl-option-rlimit-per>`.
 All these options take a single non-negative number as an argument where giving zero explicitly disables the respective limit. For time limits the number is interpreted as the number of milliseconds, and for resource limits it indicates the amount of *resources*.
 
-The limits configured using :ref:`tlimit <lbl-option-tlimit>` and :ref:`rlimit <lbl-option-rlimit>` restrict time and resource usage over the whole lifetime of the :cpp:class:`solver <cvc5::api::Solver>` object, respectively.
-In contrast to that, :ref:`tlimit-per <lbl-option-tlimit-per>` and :ref:`rlimit-per <lbl-option-rlimit-per>` apply to every check individually (:cpp:func:`checkSat <cvc5::api::Solver::checkSat>`, :cpp:func:`checkSatAssuming <cvc5::api::Solver::checkSatAssuming>`, :cpp:func:`checkEntailed <cvc5::api::Solver::checkEntailed>`, etc).
+The limits configured using :ref:`tlimit <lbl-option-tlimit>` and :ref:`rlimit <lbl-option-rlimit>` restrict time and resource usage over the whole lifetime of the :cpp:class:`solver <cvc5::Solver>` object, respectively.
+In contrast to that, :ref:`tlimit-per <lbl-option-tlimit-per>` and :ref:`rlimit-per <lbl-option-rlimit-per>` apply to every check individually (:cpp:func:`checkSat <cvc5::Solver::checkSat>`, :cpp:func:`checkSatAssuming <cvc5::Solver::checkSatAssuming>`, :cpp:func:`checkEntailed <cvc5::Solver::checkEntailed>`, etc).
 
 Except for the overall time limit (see below), the limits are checked by cvc5 itself and the solver is in a safe state after exhausting a limit.
 Due to the way cvc5 checks these limits (see below), cvc5 may not precisely honor per-call time limits: if a subroutine requires a long time to finish without spending resources itself, cvc5 only realizes afterwards that the timeout has (long) passed.
@@ -31,7 +31,7 @@ All other limits are enforced centrally by the resource manager as follows.
 Whenever certain parts of the solver execute, they instruct the resource manager to *spend* a resource.
 As soon as the resource manager realizes that some limit is exhausted (either the resource limit or the per-check time limit is reached), it asynchronously instructs the core solver to interrupt the check.
 To not invalidate the internal state of the solver, and allow to use it again after an interrupt, the solver continues its work until it reaches a safe point in one of the core solving components.
-Then, it returns `unknown` (with an :cpp:enum:`explanation <cvc5::api::Result::UnknownExplanation>`).
+Then, it returns `unknown` (with an :cpp:enum:`explanation <cvc5::Result::UnknownExplanation>`).
 
 The intention of a resource limit is to be a deterministic measure that grows (linearly, if possible) with actual running time.
 Resources are spent when lemmas are generated and during a few select events like preprocessing, rewriting, decisions and restarts in the SAT solver, or theory checks.

diff --git a/docs/statistics.rst b/docs/statistics.rst
index 263104978b5f94058fe0ca83cf23ef051640a3c3..a2d81c7dc1da09e08d1aedc3e769e755c29c496d 100644 (file)
--- a/docs/statistics.rst
+++ b/docs/statistics.rst
@@ -2,7 +2,7 @@ Statistics
 ==========
 
 cvc5 collects a wide variety of statistics that give some insight on how it solves a particular input.
-The statistics can be inspected via the :cpp:func:`Solver::getStatistics() <cvc5::api::Solver::getStatistics()>` API
+The statistics can be inspected via the :cpp:func:`Solver::getStatistics() <cvc5::Solver::getStatistics()>` API
 function, or printed using the following options:
 
 - :ref:`stats <lbl-option-stats>` prints public statistics with non-default values
@@ -12,20 +12,20 @@ function, or printed using the following options:
 
 Statistics collection is only available if the ``ENABLE_STATISTICS`` cmake option
 is set to true, which is the case for all but competition builds.
-Statistics, obtained via :cpp:func:`Solver::getStatistics() <cvc5::api::Solver::getStatistics()>`,
+Statistics, obtained via :cpp:func:`Solver::getStatistics() <cvc5::Solver::getStatistics()>`,
 are always a snapshot of the statistics values that is decoupled from the
 solver object and will not change when the solver is used again or deallocated.
 Individual statistics values can be obtained via the API either by iterating over the 
-:cpp:class:`Statistics <cvc5::api::Statistics>` object or by querying it by name.
+:cpp:class:`Statistics <cvc5::Statistics>` object or by querying it by name.
 
-A statistic value (of type :cpp:class:`Stat <cvc5::api::Stat>`) has two general
-properties, :cpp:func:`isInternal() <cvc5::api::Stat::isInternal()>` and
-:cpp:func:`isDefault() <cvc5::api::Stat::isDefault()>`.
-:cpp:func:`isInternal() <cvc5::api::Stat::isInternal()>` indicates whether a
+A statistic value (of type :cpp:class:`Stat <cvc5::Stat>`) has two general
+properties, :cpp:func:`isInternal() <cvc5::Stat::isInternal()>` and
+:cpp:func:`isDefault() <cvc5::Stat::isDefault()>`.
+:cpp:func:`isInternal() <cvc5::Stat::isInternal()>` indicates whether a
 statistic is considered public or internal. Public statistics are considered to
 be part of the public API and should therefore remain stable across different
 minor versions of cvc5. There is no such guarantee for internal statistics.
-:cpp:func:`isDefault() <cvc5::api::Stat::isDefault()>` checks whether the
+:cpp:func:`isDefault() <cvc5::Stat::isDefault()>` checks whether the
 current value of a statistics is still the default value, or whether its value
 was changed.
 
@@ -44,5 +44,5 @@ Printing statistics on the command line looks like this:
 .. run-command:: bin/cvc5 --stats ../test/regress/cli/regress0/auflia/bug336.smt2
 
 Public statistics include some general information about the input file
-(``driver::filename`` and ``api::*``), the overall runtime (``global::totalTime``)
+(``driver::filename`` and ``*``), the overall runtime (``global::totalTime``)
 and the lemmas each theory sent to the core solver (``theory::*``).

diff --git a/docs/theories/bags.rst b/docs/theories/bags.rst
index a458b44b2f1f0acc7e4d4855a124bbd61485db0b..d3e32fb28633628d4c1d4c1f8d69c2c2fe896742 100644 (file)
--- a/docs/theories/bags.rst
+++ b/docs/theories/bags.rst
@@ -8,14 +8,14 @@ cvc5 supports the theory of finite bags using the following sorts, constants,
 functions and predicates.
 
 For the C++ API examples in the table below, we assume that we have created
-a `cvc5::api::Solver solver` object.
+a `cvc5::Solver solver` object.
 
 +----------------------+----------------------------------------------+-------------------------------------------------------------------------+
 |                      | SMTLIB language                              | C++ API                                                                 |
 +----------------------+----------------------------------------------+-------------------------------------------------------------------------+
 | Logic String         | ``(set-logic ALL)``                          | ``solver.setLogic("ALL");``                                             |
 +----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-| Sort                 | ``(Bag <Sort>)``                             | ``solver.mkBagSort(cvc5::api::Sort elementSort);``                      |
+| Sort                 | ``(Bag <Sort>)``                             | ``solver.mkBagSort(cvc5::Sort elementSort);``                           |
 +----------------------+----------------------------------------------+-------------------------------------------------------------------------+
 | Constants            | ``(declare-const X (Bag String)``            | ``Sort s = solver.mkBagSort(solver.getStringSort());``                  |
 |                      |                                              |                                                                         |

diff --git a/docs/theories/datatypes.rst b/docs/theories/datatypes.rst
index e0d731d28eb936b274e50da84fec9ac665be500a..2ba8906e25ff631e5db83b28d35d5045d6cd8f0f 100644 (file)
--- a/docs/theories/datatypes.rst
+++ b/docs/theories/datatypes.rst
@@ -169,7 +169,7 @@ Syntax/API
 ----------
 
 For the C++ API examples in the table below, we assume that we have created
-a `cvc5::api::Solver solver` object.
+a `cvc5::Solver solver` object.
 
 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
 |                    | SMTLIB language                        | C++ API                                                                                                                         |
@@ -212,7 +212,7 @@ a `cvc5::api::Solver solver` object.
 |                    |                                        |                                                                                                                                 |
 |                    |                                        | ``Term r = solver.mkTerm(Kind::APPLY_TESTER, {upd, t, u});``                                                                    |
 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
-| Tuple Sort         | ``(Tuple <Sort_1>, ..., <Sort_n>)``    | ``std::vector<cvc5::api::Sort> sorts = { ... };``                                                                               |
+| Tuple Sort         | ``(Tuple <Sort_1>, ..., <Sort_n>)``    | ``std::vector<cvc5::Sort> sorts = { ... };``                                                                                    |
 |                    |                                        |                                                                                                                                 |
 |                    |                                        | ``Sort s = solver.mkTupleSort(sorts);``                                                                                         |
 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+

diff --git a/docs/theories/separation-logic.rst b/docs/theories/separation-logic.rst
index a971c76fb7e0ffc65ebfd96bb481e09fb88655fa..55811ed25f51f2edb781ab0ebd8020936827e4e9 100644 (file)
--- a/docs/theories/separation-logic.rst
+++ b/docs/theories/separation-logic.rst
@@ -69,7 +69,7 @@ This command must be executed when the solver is in its Start mode (see page 52
 
 The syntax for the operators of separation logic is summarized in the following
 table. For the C++ API examples in this table, we assume that we have created
-a :cpp:class:`cvc5::api::Solver` object.
+a :cpp:class:`cvc5::Solver` object.
 
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
 |                      | SMTLIB language                              | C++ API                                                            |
@@ -86,7 +86,7 @@ a :cpp:class:`cvc5::api::Solver` object.
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
 | Magic Wand           | ``(wand c1 c1)``                             | ``solver.mkTerm(Kind::SEP_WAND, c1, c2);``                         |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
-| Nil Element          | ``(as sep.nil <Sort>)``                      | ``solver.mkSepNil(cvc5::api::Sort sort);``                         |
+| Nil Element          | ``(as sep.nil <Sort>)``                      | ``solver.mkSepNil(cvc5::Sort sort);``                              |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
 
 

diff --git a/docs/theories/sets-and-relations.rst b/docs/theories/sets-and-relations.rst
index 4a6501653908bc0059d39c02a2c45611342326aa..88c38aa27b0c922fdf13cbefb863f30dcd5773ec 100644 (file)
--- a/docs/theories/sets-and-relations.rst
+++ b/docs/theories/sets-and-relations.rst
@@ -10,7 +10,7 @@ cvc5 supports the theory of finite sets using the following sorts, constants,
 functions and predicates.  More details can be found in :cite:`BansalBRT17`.
 
 For the C++ API examples in the table below, we assume that we have created
-a `cvc5::api::Solver solver` object.
+a `cvc5::Solver solver` object.
 
 +----------------------+----------------------------------------------+-------------------------------------------------------------------------+
 |                      | SMTLIB language                              | C++ API                                                                 |
@@ -19,7 +19,7 @@ a `cvc5::api::Solver solver` object.
 |                      |                                              |                                                                         |
 |                      | ``(set-logic QF_UFLIAFS)``                   | ``solver.setLogic("QF_UFLIAFS");``                                      |
 +----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-| Sort                 | ``(Set <Sort>)``                             | ``solver.mkSetSort(cvc5::api::Sort elementSort);``                      |
+| Sort                 | ``(Set <Sort>)``                             | ``solver.mkSetSort(cvc5::Sort elementSort);``                           |
 +----------------------+----------------------------------------------+-------------------------------------------------------------------------+
 | Constants            | ``(declare-const X (Set Int)``               | ``Sort s = solver.mkSetSort(solver.getIntegerSort());``                 |
 |                      |                                              |                                                                         |
@@ -151,7 +151,7 @@ More details can be found in :cite:`MengRTB17`.
 +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
 | Logic String         | ``(set-logic QF_ALL)``                       | ``solver.setLogic("QF_ALL");``                                                     |
 +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
-| Tuple Sort           | ``(Tuple <Sort_1>, ..., <Sort_n>)``          | ``std::vector<cvc5::api::Sort> sorts = { ... };``                                  |
+| Tuple Sort           | ``(Tuple <Sort_1>, ..., <Sort_n>)``          | ``std::vector<cvc5::Sort> sorts = { ... };``                                       |
 |                      |                                              |                                                                                    |
 |                      |                                              | ``Sort s = solver.mkTupleSort(sorts);``                                            |
 +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
@@ -171,7 +171,7 @@ More details can be found in :cite:`MengRTB17`.
 |                      |                                              |                                                                                    |
 |                      |                                              | ``Term t = solver.mkTerm(Kind::APPLY_SELECTOR, {s, t});``                          |
 +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
-| Relation Sort        | ``(Set (Tuple <Sort_1>, ..., <Sort_n>))``    | ``Sort s = solver.mkSetSort(cvc5::api::Sort tupleSort);``                          |
+| Relation Sort        | ``(Set (Tuple <Sort_1>, ..., <Sort_n>))``    | ``Sort s = solver.mkSetSort(cvc5::Sort tupleSort);``                               |
 +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
 | Constants            | ``(declare-const X (Set (Tuple Int Int)``    | ``Sort s = solver.mkSetSort(solver.mkTupleSort({s_int, s_int});``                  |
 |                      |                                              |                                                                                    |