docs/api/cpp/classes/solver.rst

Solver
======

This class represents a cvc5 solver instance.

:cpp:class:`Terms <cvc5::Term>`, :cpp:class:`Sorts <cvc5::Sort>` and
:cpp:class:`Ops <cvc5::Op>` are not tied to a :cpp:class:`cvc5::Solver`
but associated with a :cpp:class:`cvc5::TermManager` instance, which can be
shared between solver instances.

Solver options are configured via :cpp:func:`cvc5::Solver::setOption()`
and queried via :cpp:func:`cvc5::Solver::getOption()`
(for more information on configuration options, see :doc:`../../../options`).
Information about a specific option can be retrieved via
:cpp:func:`cvc5::getOptionInfo()` (see :doc:`optioninfo`).

----

.. doxygenclass:: cvc5::Solver
    :project: cvc5
    :members:
    :undoc-members:
New C++ Api: Initial layout of Api documentation. (#6325) 2021-04-09 15:28:18 -07:00			`Solver`
			`======`

docs: Refactor and extend C++ documentation. (#10006) 2023-09-11 09:31:57 -07:00			`This class represents a cvc5 solver instance.`

			:cpp:class:`Terms <cvc5::Term>`, :cpp:class:`Sorts <cvc5::Sort>` and
			:cpp:class:`Ops <cvc5::Op>` are not tied to a :cpp:class:`cvc5::Solver`
c++ api: Expose TermManager to the API. (#10426) This introduces a TermManager object, which will, in the future, be the sole object responsible for handling/managing terms and sorts. For now, all corresponding functions in `cvc5::Solver` are marked as deprecated, as is constructor `cvc5::Solver::Solver()`, since in the future a solver instance must be constructed from a term manager instance. Currently, we maintain a static thread_local term manager instance to not break the API and continue providing constructor `cvc5::Solver::Solver()`. Note that this already converts all C++ unit tests to use the TermManager except for a single test `getStatistics()` in `test/unit/api/cpp/solver_black.cpp`. Statistics handling is currently still maintained on the solver level. The statistics we maintain, however, concern terms only and will eventually be refactored to be tracked in the NodeManager. Further note that the Java and Python APIs will be refactored in separate PRs. 2024-03-08 11:39:13 -08:00			but associated with a :cpp:class:`cvc5::TermManager` instance, which can be
			`shared between solver instances.`
docs: Refactor and extend C++ documentation. (#10006) 2023-09-11 09:31:57 -07:00
			Solver options are configured via :cpp:func:`cvc5::Solver::setOption()`
			and queried via :cpp:func:`cvc5::Solver::getOption()`
docs: cpp: Restructure directory, tweak class hierarchy. (#11040) 2024-07-12 11:05:13 -07:00			(for more information on configuration options, see :doc:`../../../options`).
docs: Refactor and extend C++ documentation. (#10006) 2023-09-11 09:31:57 -07:00			`Information about a specific option can be retrieved via`
			:cpp:func:`cvc5::getOptionInfo()` (see :doc:`optioninfo`).

			`----`

docs: Remove api namespace. (#8455) 2022-03-30 19:30:21 -07:00			`.. doxygenclass:: cvc5::Solver`
New C++ Api: Initial layout of Api documentation. (#6325) 2021-04-09 15:28:18 -07:00			`:project: cvc5`
			`:members:`
			`:undoc-members:`