Package io.github.cvc5

package io.github.cvc5
  • Class
    Description
    AbstractPlugin
    A cvc5 plugin abstract class.
    Command
    Encapsulation of a command.
    Context
    The Context class is responsible for tracking and deleting pointers to native C++ cvc5 objects associated with their corresponding Java counterparts.
    CVC5ApiException
    Base class for all API exceptions.
    CVC5ApiOptionException
    An option-related API exception.
    CVC5ApiRecoverableException
    A recoverable API exception.
    CVC5ParserException
    A parser-related API exception.
    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.
    IOracle
    Functional interface representing an oracle function that operates on an array of Term objects and produces a single Term as output.
    Kind
    Enum representing the set of possible values for Kind.
    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>
    A simple generic container class to hold a pair of objects.
    Proof
    A cvc5 Proof.
    ProofRewriteRule
    Enum representing the set of possible values for ProofRewriteRule.
    ProofRule
    Enum representing the set of possible values for ProofRule.
    Result
    Encapsulation of a three-valued solver result, with explanations.
    RoundingMode
    Enum representing the set of possible values for RoundingMode.
    SkolemId
    Enum representing the set of possible values for SkolemId.
    Solver
    A cvc5 solver.
    Sort
    The sort of a cvc5 term.
    SortKind
    Enum representing the set of possible values for SortKind.
    Stat
    Represents a snapshot of a single statistic value.
    Statistics
    Represents a snapshot of the solver statistics.
    SymbolManager
    Symbol manager.
    SynthResult
    Encapsulation of a solver synth result.
    Term
    A cvc5 Term.
    TermManager
    A cvc5 term manager.
    Triplet<A,B,C>
    A generic container class to hold a triplet of objects.
    UnknownExplanation
    Enum representing the set of possible values for UnknownExplanation.
    Utils
    A utility class containing static helper methods commonly used across the application.
    Utils.OS
    Represent the operating system types supported by cvc5.