C++ API 

The C++ API is the primary interface for cvc5 and exposes the full functionality of cvc5. The 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 Solver class is the main entry point to cvc5.

Class hierarchy 

namespace cvc5 {

class CVC5ApiException

class CVC5ApiRecoverableException

class Datatype

class const_iterator

class DatatypeConstructor

class const_iterator

class DatatypeConstructorDecl

class DatatypeDecl

class DatatypeSelector

class DriverOptions

class Grammar

class Op

class OptionInfo

class Result

class Solver

class Sort

class Stat

class Statistics

class SynthResult

class Term

class const_iterator

enum class Kind

enum class SortKind

enum class RoundingMode

enum class UnknownExplanation

namespace modes {

enum classes for configuration modes
- enum class for cvc5::modes::BlockModelsMode
- enum class for cvc5::modes::LearnedLitType
- enum class for cvc5::modes::ProofComponent
- enum class for cvc5::modes::FindSynthTarget

}

namespace parser {

class Command

class InputParser

class ParserException

class SymbolManager

}