Package org.smtlib

Interface IExpr

All Superinterfaces:

IAttributeValue, INode, IPos.IPosable, IResponse

All Known Subinterfaces:

IExpr.IAsIdentifier, 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.IQualifiedIdentifier, IExpr.IStringLiteral, IExpr.ISymbol

All Known Implementing Classes:

Pos.AbstractExpr, SMTExpr, SMTExpr.AsIdentifier, 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.StringLiteral, SMTExpr.Symbol

public interface IExpr
extends INode, IPos.IPosable, IAttributeValue

This interface represents the functionality for any class implementing an SMT-LIB term or formula

Nested Class Summary

Nested Classes

Modifier and Type	Interface	Description
static interface	IExpr.IAsIdentifier	This interface represents SMT-LIB identifiers that are sort qualifiers on function ids
static interface	IExpr.IAttribute<TT extends IAttributeValue>	This interface represents an SMT-LIB attribute-value pair; the value may be null (keyword-only attribute).
static interface	IExpr.IAttributedExpr	This interface represents an SMT-LIB expression with attributes.
static interface	IExpr.IBinaryLiteral	This interface represents SMT-LIB binary literals
static interface	IExpr.IBinding	This interface represents a binding of a parameter and an expression
static interface	IExpr.IConstructor	A constructor declaration within a datatype; pairs a constructor name with its selectors.
static interface	IExpr.IDecimal	This interface represents non-negative decimal numbers of arbitrary size (i.e.
static interface	IExpr.IDeclaration	This interface represents a declaration of a parameter and its sort
static interface	IExpr.IError	This interface represents an error, e.g.
static interface	IExpr.IExists	This interface represents an SMT-LIB quantified exists expression
static interface	IExpr.IFactory	The interface defining the factory type for producing objects of various subtypes of IExpr; the IPos argument is an optional argument giving information about the textual position of an expression.
static interface	IExpr.IFcnExpr	This interface represents SMT-LIB expressions that are a function identifier applied to one or more arguments.
static interface	IExpr.IForall	This interface represents an SMT-LIB quantified forall expression
static interface	IExpr.IFunctionDeclaration	A function declaration: a name, a parameter list (sorted variables), and a result sort; used in the header list of define-funs-rec.
static interface	IExpr.IHexLiteral	This interface represents SMT-LIB hex literals
static interface	IExpr.IIdentifier	This interface represents SMT-LIB identifiers (either ids or parameterized ids)
static interface	IExpr.IIndex	Marker interface for the index types in a parameterized identifier: INumeral and ISymbol, plus IHexLiteral, which the Strings theory's (_ char H) uses, and IBinaryLiteral, which no theory uses but which is parsed so that a solver reports it; each theory decides which kinds it accepts.
static interface	IExpr.IKeyword	This interface represents SMT-LIB attribute and infoflag names.
static interface	IExpr.ILambda	This interface represents an SMT-LIB lambda expression: (lambda (sorted_var+) term).
static interface	IExpr.ILet	This interface represents an SMT-LIB let-expression
static interface	IExpr.ILiteral	This interface represents all literal (explicit constant) expressions.
static interface	IExpr.IMatch	This interface represents an SMT-LIB 2.7 match expression.
static interface	IExpr.IMatchCase	This interface represents one case in a match expression: a pattern and its body.
static interface	IExpr.INumeral	This interface represents non-negative integers of arbitrary size.
static interface	IExpr.IParameterizedIdentifier	This interface represents SMT-LIB parameterized identifiers
static interface	IExpr.IPattern	This interface represents a match pattern: either a bare symbol (variable/nullary-constructor) or a constructor applied to zero or more variable symbols.
static interface	IExpr.IPatternTerms	This interface represents the value of a :pattern attribute: a list of terms (a multi-pattern), written in the concrete syntax as ( t1 ... tn ).
static interface	IExpr.IQualifiedIdentifier	This interface represents SMT-LIB identifiers for function ids (either ids or parameterized ids or as-type identifiers)
static interface	IExpr.ISelector	A selector declaration within a constructor; pairs a selector name with its result sort.
static interface	IExpr.ISortDeclaration	Pairs a sort name with its arity; used in declare-datatype and declare-datatypes.
static interface	IExpr.IStringLiteral	This interface represents SMT-LIB string literals
static interface	IExpr.ISymbol	This interface represents SMT-LIB ids; equal ids have equal (using .equals) values of value().

Nested classes/interfaces inherited from interface org.smtlib.IResponse

IResponse.IAssertionsResponse, IResponse.IAssignmentResponse, IResponse.IAttributeList, IResponse.IPair<T1,T2>, IResponse.IProofResponse, IResponse.IUnsatAssumptionsResponse, IResponse.IUnsatCoreResponse, IResponse.IValueResponse

Method Summary

Modifier and Type	Method	Description
default boolean	isError()	Returns true if the response is an error response
void	setSort(ISort sort)	Records the sort computed for this expression by the type checker.
ISort	sort()	The sort computed for this expression by the type checker, or null if not yet (or never) computed.

Methods inherited from interface org.smtlib.IAttributeValue

isOK

Methods inherited from interface org.smtlib.INode

accept

Methods inherited from interface org.smtlib.IPos.IPosable

pos, setPos

Method Details

isError

default boolean isError()

Description copied from interface: IResponse

Returns true if the response is an error response

Specified by:

isError in interface IAttributeValue

Specified by:

isError in interface IResponse

sort

ISort sort()

The sort computed for this expression by the type checker, or null if not yet (or never) computed.

setSort

void setSort(ISort sort)

Records the sort computed for this expression by the type checker.