| Interface | Description |
|---|---|
| IOracle |
| Class | Description |
|---|---|
| AbstractPlugin | |
| Command | |
| Context | |
| Datatype |
A cvc5 datatype.
|
| DatatypeConstructor |
A cvc5 datatype constructor.
|
| DatatypeConstructorDecl |
A cvc5 datatype constructor declaration.
|
| DatatypeDecl |
A cvc5 datatype declaration.
|
| DatatypeSelector |
A cvc5 datatype selector.
|
| Grammar |
A Sygus Grammar.
|
| InputParser |
This class is the main interface for retrieving commands and expressions
from an input using a parser.
|
| Op |
A cvc5 operator.
|
| OptionInfo |
Holds some description about a particular option, including its name, its
aliases, whether the option was explicitly set by the user, and information
concerning its value.
|
| Pair<K,V> | |
| Proof |
A cvc5 Proof.
|
| Result |
Encapsulation of a three-valued solver result, with explanations.
|
| Solver |
A cvc5 solver.
|
| Sort |
The sort of a cvc5 term.
|
| Stat |
Represents a snapshot of a single statistic value.
|
| Statistics | |
| SymbolManager | |
| SynthResult |
Encapsulation of a solver synth result.
|
| Term |
A cvc5 Term.
|
| TermManager |
A cvc5 term manager.
|
| Triplet<A,B,C> | |
| Utils |
| Enum | Description |
|---|---|
| Kind | |
| ProofRewriteRule | |
| ProofRule | |
| RoundingMode | |
| SkolemId | |
| SortKind | |
| UnknownExplanation | |
| Utils.OS |
| Exception | Description |
|---|---|
| CVC5ApiException | |
| CVC5ApiOptionException | |
| CVC5ApiRecoverableException | |
| CVC5ParserException |