All Classes and Interfaces
Class
Description
A cvc5 plugin abstract class.
Enum representing the set of possible values for BlockModelsMode.
Encapsulation of a command.
The
Context class is responsible for tracking and deleting pointers to
native C++ cvc5 objects associated with their corresponding Java counterparts.Base class for all API exceptions.
An option-related API exception.
A recoverable API exception.
A parser-related API exception.
A cvc5 datatype.
A cvc5 datatype constructor.
A cvc5 datatype constructor declaration.
A cvc5 datatype declaration.
A cvc5 datatype selector.
Enum representing the set of possible values for FindSynthTarget.
A Sygus Grammar.
Enum representing the set of possible values for InputLanguage.
This class is the main interface for retrieving commands and expressions
from an input using a parser.
Enum representing the set of possible values for Kind.
Enum representing the set of possible values for LearnedLitType.
A cvc5 operator.
Enum representing the set of possible values for OptionCategory.
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.
A simple generic container class to hold a pair of objects.
A cvc5 Proof.
Enum representing the set of possible values for ProofComponent.
Enum representing the set of possible values for ProofFormat.
Enum representing the set of possible values for ProofRewriteRule.
Enum representing the set of possible values for ProofRule.
Encapsulation of a three-valued solver result, with explanations.
Enum representing the set of possible values for RoundingMode.
Enum representing the set of possible values for SkolemId.
A cvc5 solver.
The sort of a cvc5 term.
Enum representing the set of possible values for SortKind.
Represents a snapshot of a single statistic value.
Represents a snapshot of the solver statistics.
Symbol manager.
Encapsulation of a solver synth result.
A cvc5 Term.
A cvc5 term manager.
A generic container class to hold a triplet of objects.
Enum representing the set of possible values for UnknownExplanation.
A utility class containing static helper methods commonly used across the application.
Represent the operating system types supported by cvc5.