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 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 TermManager
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
}
}