Package org.smtlib

Interface IExpr.ILambda

All Superinterfaces:

IAttributeValue, IExpr, INode, IPos.IPosable, IResponse

All Known Implementing Classes:

SMTExpr.Lambda

Enclosing interface:

IExpr

public static interface IExpr.ILambda
extends IExpr

This interface represents an SMT-LIB lambda expression: (lambda (sorted_var+) term). Lambda is only available as of SMT-LIB version 2.7 and later ("2.7ff") -- it was added to the <term> grammar as part of the optional HO-Core theory (see SMT/logics/HO-Core.smt2), the same way the non-standard par-polymorphic declare-fun extension documents its own version/scope restrictions elsewhere. jSMTLIB has no general runtime mechanism that would reject this node under an older configured version merely for existing; TypeChecker.visit(ILambda) does check the configured SMT-LIB version explicitly, the same way it already does for IExpr.IMatch. A lambda's own sort is the function/array sort mapping its parameters' sorts to its body's sort -- see TypeChecker.visit(ILambda) for exactly how (and under what conditions) that result sort is computed, using the SMT-LIB 2.7 (-> sort+ sort) function-sort constructor that HO-Core also declares.

Nested Class Summary

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

IExpr.IAsIdentifier, IExpr.IAttribute<TT extends IAttributeValue>, IExpr.IAttributedExpr, IExpr.IBinaryLiteral, IExpr.IBinding, IExpr.IConstructor, IExpr.IDecimal, IExpr.IDeclaration, IExpr.IError, IExpr.IExists, IExpr.IFactory, IExpr.IFcnExpr, IExpr.IForall, IExpr.IFunctionDeclaration, IExpr.IHexLiteral, IExpr.IIdentifier, IExpr.IIndex, IExpr.IKeyword, IExpr.ILambda, IExpr.ILet, IExpr.ILiteral, IExpr.IMatch, IExpr.IMatchCase, IExpr.INumeral, IExpr.IParameterizedIdentifier, IExpr.IPattern, IExpr.IPatternTerms, IExpr.IQualifiedIdentifier, IExpr.ISelector, IExpr.ISortDeclaration, IExpr.IStringLiteral, IExpr.ISymbol

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
IExpr	expr()
List<IExpr.IDeclaration>	parameters()

Methods inherited from interface org.smtlib.IAttributeValue

isOK

Methods inherited from interface org.smtlib.IExpr

isError, setSort, sort

Methods inherited from interface org.smtlib.INode

accept

Methods inherited from interface org.smtlib.IPos.IPosable

pos, setPos

Method Details

parameters

List<IExpr.IDeclaration> parameters()

expr

IExpr expr()