From: Mathias Preiner Date: Thu, 31 Mar 2022 02:30:21 +0000 (-0700) Subject: docs: Remove api namespace. (#8455) X-Git-Tag: cvc5-1.0.0~104 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f66e2adea08350ac68dea456e26aa111752f064b;p=cvc5.git docs: Remove api namespace. (#8455) --- diff --git a/docs/api/cpp/CMakeLists.txt b/docs/api/cpp/CMakeLists.txt index 4d637dee0..daa117997 100644 --- 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 67f2c8053..f51f55756 100644 --- 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 ` 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 ` class is the main entry point to cvc5. +The :doc:`quickstart guide ` 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 ` class is the main entry point to cvc5. .. container:: hide-toctree @@ -33,17 +33,17 @@ For most applications, the :cpp:class:`Solver ` class is the Class hierarchy ^^^^^^^^^^^^^^^ -``namespace cvc5::api {`` +``namespace cvc5 {`` - * class :cpp:class:`CVC5ApiException ` - * class :cpp:class:`CVC5ApiRecoverableException ` + * class :cpp:class:`CVC5ApiException ` + * class :cpp:class:`CVC5ApiRecoverableException ` * class :ref:`api/cpp/datatype:datatype` - * class :cpp:class:`const_iterator ` + * class :cpp:class:`const_iterator ` * class :ref:`api/cpp/datatypeconstructor:datatypeconstructor` - * class :cpp:class:`const_iterator ` + * class :cpp:class:`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 ` + * enum :cpp:enum:`UnknownExplanation ` * class :ref:`api/cpp/roundingmode:roundingmode` * class :ref:`api/cpp/solver:solver` * class :ref:`api/cpp/sort:sort` - * class :cpp:class:`Stat ` - * class :cpp:class:`Statistics ` + * class :cpp:class:`Stat ` + * class :cpp:class:`Statistics ` * class :ref:`api/cpp/synthresult:synthresult` * class :ref:`api/cpp/term:term` - * class :cpp:class:`const_iterator ` + * class :cpp:class:`const_iterator ` ``}`` diff --git a/docs/api/cpp/datatype.rst b/docs/api/cpp/datatype.rst index 7c5325ec1..3fc4e284f 100644 --- 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 90b48e8e1..1b9a7876e 100644 --- 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 7cb5b6a8c..9161d4dae 100644 --- 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 d3927b805..f4f94a430 100644 --- 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 22ac01aa4..34602a92d 100644 --- 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 5fa65e5e5..2c62ab40c 100644 --- 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 -` and :cpp:class:`CVC5ApiRecoverableException -` (which is derived from -:cpp:class:`CVC5ApiException `). +` and :cpp:class:`CVC5ApiRecoverableException +` (which is derived from +:cpp:class:`CVC5ApiException `). If any method fails with a :cpp:class:`CVC5ApiRecoverableException -`, the solver behaves as if the failing +`, 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 -`, the associated object may be in an unsafe state +`, 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 dc7291f67..e5c9493e5 100644 --- 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 996691524..f10ed2695 100644 --- a/docs/api/cpp/kind.rst +++ b/docs/api/cpp/kind.rst @@ -1,21 +1,21 @@ Kind ==== -Every :cpp:class:`Term ` has an associated kind. +Every :cpp:class:`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 `, +:cpp:enumerator:`CONST_BITVECTOR `, a free constant symbol has kind -:cpp:enumerator:`CONSTANT `, +:cpp:enumerator:`CONSTANT `, an equality over terms of any sort has kind -:cpp:enumerator:`EQUAL `, and a universally -quantified formula has kind :cpp:enumerator:`FORALL `. +:cpp:enumerator:`EQUAL `, and a universally +quantified formula has kind :cpp:enumerator:`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 a320125a2..9034cda3b 100644 --- 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 eb7848210..d1761c5eb 100644 --- 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 88320a508..66435840a 100644 --- 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 ` instance: +First, create a cvc5 :cpp:class:`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 9ba1aaaaf..c01e64deb 100644 --- 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 a54d1a65c..6626157eb 100644 --- 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 17529f09b..53bb6bd04 100644 --- 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 7cbf46271..528f27bcd 100644 --- a/docs/api/cpp/sort.rst +++ b/docs/api/cpp/sort.rst @@ -1,18 +1,18 @@ Sort ==== -The :cpp:class:`Sort ` class represents the sort of a -:cpp:class:`Term `. +The :cpp:class:`Sort ` class represents the sort of a +:cpp:class:`Term `. -A :cpp:class:`Sort ` can be hashed (using -:cpp:class:`std::hash\`) and serialized to an output stream -(using :cpp:func:`cvc5::api::operator<<()`). +A :cpp:class:`Sort ` can be hashed (using +:cpp:class:`std::hash\`) and serialized to an output stream +(using :cpp:func:`cvc5::operator<<()`). -Class :cpp:class:`Sort ` offers the default constructor -only to create a null Sort. Instead, the :cpp:class:`Solver ` +Class :cpp:class:`Sort ` offers the default constructor +only to create a null Sort. Instead, the :cpp:class:`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 `) - - Created with :cpp:func:`cvc5::api::Solver::mkSetSort()` + - Created with :cpp:func:`cvc5::Solver::mkSetSort()` - *Relation* (:ref:`Theory of Sets and Relations `) - - 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 77fab9545..069f2b851 100644 --- 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 ` object that can +represented by a :cpp:class:`Statistics ` object that can be obtained from :cpp:func:`Solver::getStatistics() -`. It is a copy of the internal solver +`. It is a copy of the internal solver statistics at this point in time. -The :cpp:class:`Statistics ` object is essentially a +The :cpp:class:`Statistics ` object is essentially a mapping from names (as ``std::string``) to statistic values, represented by the -:cpp:class:`Stat ` class. A :cpp:class:`Stat ` +:cpp:class:`Stat ` class. A :cpp:class:`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() `, -:cpp:func:`Stat::isDouble() `, etc) and obtaining -the actual value (:cpp:func:`Stat::getInt() `, -:cpp:func:`Stat::getDouble() `, etc). Histograms +(:cpp:func:`Stat::isInt() `, +:cpp:func:`Stat::isDouble() `, etc) and obtaining +the actual value (:cpp:func:`Stat::getInt() `, +:cpp:func:`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`` 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 ` object only shows statistics +:cpp:class:`Statistics ` object only shows statistics that are both public and changed. The :cpp:func:`Statistics::begin() -` method has Boolean flags ``internal`` and +` 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 1765f48c6..c65289ba1 100644 --- 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 1f112a58a..cb7812cac 100644 --- a/docs/api/cpp/term.rst +++ b/docs/api/cpp/term.rst @@ -1,19 +1,19 @@ Term ==== -The :cpp:class:`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 ` enum. -The :cpp:class:`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:`isValue()` and :code:`getValue()`, which returns the constant values in the best type standard C++ offers). +The :cpp:class:`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 ` enum. +The :cpp:class:`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:`isValue()` and :code:`getValue()`, which returns the constant values in the best type standard C++ offers). -Additionally, a :cpp:class:`Term ` can be hashed (using :cpp:class:`std::hash\`) 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 ` can be hashed (using :cpp:class:`std::hash\`) 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 ` only offers the default constructor to create a null term. Instead, the :cpp:class:`Solver ` class provides factory functions for all other terms, e.g., :code:`Solver::mkTerm()` for generic terms and :code:`Solver::mk()` for constant values of a given type. +The :cpp:class:`Term ` only offers the default constructor to create a null term. Instead, the :cpp:class:`Solver ` class provides factory functions for all other terms, e.g., :code:`Solver::mkTerm()` for generic terms and :code:`Solver::mk()` 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 9047c1d57..657b89ea2 100644 --- a/docs/api/python/base/kind.rst +++ b/docs/api/python/base/kind.rst @@ -5,7 +5,7 @@ Every :py:class:`Term ` has a kind which represents its type, for example whether it is an equality (:py:obj:`Equal `), a conjunction (:py:obj:`And `), or a bit-vector addtion (:py:obj:`BVAdd `). -The kinds below directly correspond to the enum values of the C++ :cpp:enum:`Kind ` enum. +The kinds below directly correspond to the enum values of the C++ :cpp:enum:`Kind ` enum. .. autoclass:: cvc5.Kind :members: diff --git a/docs/conf.py.in b/docs/conf.py.in index 5817c586e..1e6174e85 100644 --- 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 abcd3b3e9..06567fbc3 100644 --- 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() `, - :cpp:func:`getOption() `, - :cpp:func:`getOptionNames() `, - :cpp:func:`getOptionInfo() ` +- C++ API: :cpp:func:`setOption() `, + :cpp:func:`getOption() `, + :cpp:func:`getOptionNames() `, + :cpp:func:`getOptionInfo() ` - Java API: ``setOption()``, ``getOption()``, ``getOptionNames()``, ``getOptionInfo()`` - Base Python API: :py:func:`setOption() `, :py:func:`getOption() `, diff --git a/docs/resource-limits.rst b/docs/resource-limits.rst index bc20ed10e..bb4e3fbdf 100644 --- 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 `, and :ref:`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 ` and :ref:`rlimit ` restrict time and resource usage over the whole lifetime of the :cpp:class:`solver ` object, respectively. -In contrast to that, :ref:`tlimit-per ` and :ref:`rlimit-per ` apply to every check individually (:cpp:func:`checkSat `, :cpp:func:`checkSatAssuming `, :cpp:func:`checkEntailed `, etc). +The limits configured using :ref:`tlimit ` and :ref:`rlimit ` restrict time and resource usage over the whole lifetime of the :cpp:class:`solver ` object, respectively. +In contrast to that, :ref:`tlimit-per ` and :ref:`rlimit-per ` apply to every check individually (:cpp:func:`checkSat `, :cpp:func:`checkSatAssuming `, :cpp:func:`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 `). +Then, it returns `unknown` (with an :cpp:enum:`explanation `). 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 263104978..a2d81c7dc 100644 --- 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() ` API +The statistics can be inspected via the :cpp:func:`Solver::getStatistics() ` API function, or printed using the following options: - :ref:`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() `, +Statistics, obtained via :cpp:func:`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 ` object or by querying it by name. +:cpp:class:`Statistics ` object or by querying it by name. -A statistic value (of type :cpp:class:`Stat `) has two general -properties, :cpp:func:`isInternal() ` and -:cpp:func:`isDefault() `. -:cpp:func:`isInternal() ` indicates whether a +A statistic value (of type :cpp:class:`Stat `) has two general +properties, :cpp:func:`isInternal() ` and +:cpp:func:`isDefault() `. +:cpp:func:`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() ` checks whether the +:cpp:func:`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 a458b44b2..d3e32fb28 100644 --- 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 )`` | ``solver.mkBagSort(cvc5::api::Sort elementSort);`` | +| Sort | ``(Bag )`` | ``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 e0d731d28..2ba8906e2 100644 --- 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 , ..., )`` | ``std::vector sorts = { ... };`` | +| Tuple Sort | ``(Tuple , ..., )`` | ``std::vector sorts = { ... };`` | | | | | | | | ``Sort s = solver.mkTupleSort(sorts);`` | +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ diff --git a/docs/theories/separation-logic.rst b/docs/theories/separation-logic.rst index a971c76fb..55811ed25 100644 --- 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 )`` | ``solver.mkSepNil(cvc5::api::Sort sort);`` | +| Nil Element | ``(as sep.nil )`` | ``solver.mkSepNil(cvc5::Sort sort);`` | +----------------------+----------------------------------------------+--------------------------------------------------------------------+ diff --git a/docs/theories/sets-and-relations.rst b/docs/theories/sets-and-relations.rst index 4a6501653..88c38aa27 100644 --- 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 )`` | ``solver.mkSetSort(cvc5::api::Sort elementSort);`` | +| Sort | ``(Set )`` | ``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 , ..., )`` | ``std::vector sorts = { ... };`` | +| Tuple Sort | ``(Tuple , ..., )`` | ``std::vector 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 s = solver.mkSetSort(cvc5::api::Sort tupleSort);`` | +| Relation Sort | ``(Set (Tuple , ..., ))`` | ``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});`` | | | | |