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.

Quickstart Guide
- Example
Exceptions
- cvc5::CVC5ApiException
- cvc5::CVC5ApiRecoverableException
  - CVC5ApiRecoverableException()
  - CVC5ApiRecoverableException()
- cvc5::parser::ParserException
Command
- cvc5::parser::Command
Datatype
- cvc5::Datatype
- operator<<()
DatatypeConstructor
- cvc5::DatatypeConstructor
- operator<<()
DatatypeConstructorDecl
- cvc5::DatatypeConstructorDecl
- operator<<()
- operator<<()
DatatypeDecl
- cvc5::DatatypeDecl
- operator<<()
DatatypeSelector
- cvc5::DatatypeSelector
- operator<<()
DriverOptions
- cvc5::DriverOptions
  - in()
  - err()
  - out()
Grammar
- cvc5::Grammar
- operator<<()
InputParser
- cvc5::parser::InputParser
Kind
- Kind
- operator<<()
- to_string()
- std::hash< cvc5::Kind >
  - operator()()
Modes
- BlockModelsMode
  - LITERALS
  - VALUES
- operator<<()
- to_string()
- LearnedLitType
- operator<<()
- to_string()
- ProofComponent
- operator<<()
- to_string()
- ProofFormat
  - NONE
  - DOT
  - LFSC
  - ALETHE
  - CPC
  - DEFAULT
- operator<<()
- to_string()
- FindSynthTarget
- operator<<()
- to_string()
Op
- cvc5::Op
- operator<<()
- std::hash< cvc5::Op >
  - operator()()
OptionInfo
- cvc5::OptionInfo
- operator<<()
Plugin
- cvc5::Plugin
Proof
- cvc5::Proof
- std::hash< cvc5::Proof >
  - operator()()
ProofRule and ProofRewriteRule
- ProofRule
- operator<<()
- to_string()
- std::hash< cvc5::ProofRule >
  - operator()()
- ProofRewriteRule
- operator<<()
- to_string()
- std::hash< cvc5::ProofRewriteRule >
  - operator()()
Result
- cvc5::Result
- operator<<()
RoundingMode
- RoundingMode
- operator<<()
- to_string()
Solver
- cvc5::Solver
Sort
- cvc5::Sort
- operator<<()
- std::hash< cvc5::Sort >
  - operator()()
SortKind
- SortKind
- operator<<()
- to_string()
- std::hash< cvc5::SortKind >
  - operator()()
Statistics
- cvc5::Statistics
- operator<<()
- cvc5::Stat
- operator<<()
SymbolManager
- cvc5::parser::SymbolManager
SynthResult
- cvc5::SynthResult
- operator<<()
Term
- cvc5::Term
- operator<<()
- operator<<()
- operator<<()
- operator<<()
- operator<<()
- operator<<()
- std::hash< cvc5::Term >
  - operator()()
TermManager
- cvc5::TermManager
UnknownExplanation
- UnknownExplanation
- operator<<()
- to_string()

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 Proof
class Result
class Plugin
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
enum class ProofRule
enum class ProofRewriteRule

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::ProofFormat
- enum class for cvc5::modes::FindSynthTarget

}

namespace parser {

}

}