Package org.smtlib

Interface IResponse

All Superinterfaces:
INode
All Known Subinterfaces:
IAttributeValue, IExpr, IExpr.IAsIdentifier, IExpr.IAttribute<TT>, IExpr.IAttributedExpr, IExpr.IBinaryLiteral, IExpr.IDecimal, IExpr.IError, IExpr.IExists, IExpr.IFcnExpr, IExpr.IForall, IExpr.IHexLiteral, IExpr.IIdentifier, IExpr.IIndex, IExpr.ILambda, IExpr.ILet, IExpr.ILiteral, IExpr.IMatch, IExpr.INumeral, IExpr.IParameterizedIdentifier, IExpr.IPatternTerms, IExpr.IQualifiedIdentifier, IExpr.IStringLiteral, IExpr.ISymbol, IResponse.IAssertionsResponse, IResponse.IAssignmentResponse, IResponse.IAttributeList, IResponse.IError, IResponse.IProofResponse, IResponse.IUnsatAssumptionsResponse, IResponse.IUnsatCoreResponse, IResponse.IValueResponse, ISexpr, ISexpr.ISeq, ISexpr.IToken<T>
All Known Implementing Classes:
AbstractSolver.Pending, Pos.AbstractExpr, Response.AssertionsResponse, Response.AssignmentResponse, Response.Error, Response.ProofResponse, Response.Seq, Response.UnsatAssumptionsResponse, Response.UnsatCoreResponse, Response.ValueResponse, Sexpr, Sexpr.Seq, Sexpr.Token, SMTExpr, SMTExpr.AsIdentifier, SMTExpr.Attribute, SMTExpr.AttributedExpr, SMTExpr.BinaryLiteral, SMTExpr.Decimal, SMTExpr.Error, SMTExpr.Exists, SMTExpr.FcnExpr, SMTExpr.Forall, SMTExpr.HexLiteral, SMTExpr.Lambda, SMTExpr.Let, SMTExpr.Literal, SMTExpr.Match, SMTExpr.Numeral, SMTExpr.ParameterizedIdentifier, SMTExpr.PatternTerms, SMTExpr.StringLiteral, SMTExpr.Symbol
public interface IResponse extends INode
This interface represents responses that can be received from SMT-LIB commands.

  • Nested Class Summary

    Nested Classes
    Modifier and Type
    Interface
    Description
    static interface 
    IResponse.IAssertionsResponse
    Response type for get-assertions, carrying the list of currently asserted formulae.
    static interface 
    IResponse.IAssignmentResponse
    Response type for get-assignment, carrying a list of name-Boolean pairs.
    static interface 
    IResponse.IAttributeList
    Response type for get-info, carrying a list of attribute key-value pairs.
    static interface 
    IResponse.IError
    The interface for error responses
    static interface 
    IResponse.IFactory
    The factory interface for creating the standard IResponse singleton and structured instances.
    static interface 
    IResponse.IPair<T1,T2>
    An interface for simple pairs of objects; used to represent value/assignment response items
    static interface 
    IResponse.IProofResponse
    Response type for get-proof.
    static interface 
    IResponse.IUnsatAssumptionsResponse
    Response type for get-unsat-assumptions, carrying the assumptions (terms, e.g.
    static interface 
    IResponse.IUnsatCoreResponse
    Response type for get-unsat-core, carrying the names of the formulae in the unsat core.
    static interface 
    IResponse.IValueResponse
    Response type for get-value, carrying a list of expression-value pairs.

  • Method Summary

    Modifier and Type
    Method
    Description
    boolean
    isError()
    Returns true if the response is an error response
    boolean
    isOK()
    Returns true if the response is a SUCCESS response

    Methods inherited from interface org.smtlib.INode

    accept

  • Method Details

    • isOK

      boolean isOK()
      Returns true if the response is a SUCCESS response

    • isError

      boolean isError()
      Returns true if the response is an error response