Package com.microsoft.z3

Class Lambda<R extends Sort>

java.lang.Object

com.microsoft.z3.Z3Object

com.microsoft.z3.AST

com.microsoft.z3.Expr<ArraySort<D,R>>

com.microsoft.z3.ArrayExpr<Sort,R>

com.microsoft.z3.Lambda<R>

All Implemented Interfaces:

Comparable<AST>

public class Lambda<R extends Sort>
extends ArrayExpr<Sort,R>

Lambda expressions.

Method Summary

Modifier and Type	Method	Description
Expr<R>	getBody()	The body of the quantifier.
Symbol[]	getBoundVariableNames()	The symbols for the bound variables.
Sort[]	getBoundVariableSorts()	The sorts of the bound variables.
int	getNumBound()	The number of bound variables.
static <R extends Sort> Lambda<R>	of(Context ctx, Expr<?>[] bound, Expr<R> body)
static <R extends Sort> Lambda<R>	of(Context ctx, Sort[] sorts, Symbol[] names, Expr<R> body)
Lambda<R>	translate(Context ctx)	Translates (copies) the quantifier to the Context ctx.

Methods inherited from class com.microsoft.z3.Expr

distillSort, getArgs, getBoolValue, getFuncDecl, getIndex, getNumArgs, getSort, getString, isAdd, isAlgebraicNumber, isAnd, isArithmeticNumeral, isArray, isArrayMap, isAsArray, isBool, isBV, isBVAdd, isBVAND, isBVBitOne, isBVBitZero, isBVCarry, isBVComp, isBVConcat, isBVExtract, isBVMul, isBVNAND, isBVNOR, isBVNOT, isBVNumeral, isBVOR, isBVReduceAND, isBVReduceOR, isBVRepeat, isBVRotateLeft, isBVRotateLeftExtended, isBVRotateRight, isBVRotateRightExtended, isBVSDiv, isBVSGE, isBVSGT, isBVShiftLeft, isBVShiftRightArithmetic, isBVShiftRightLogical, isBVSignExtension, isBVSLE, isBVSLT, isBVSMod, isBVSRem, isBVSub, isBVToInt, isBVUDiv, isBVUGE, isBVUGT, isBVULE, isBVULT, isBVUMinus, isBVURem, isBVXNOR, isBVXOR, isBVXOR3, isBVZeroExtension, isConcat, isConst, isConstantArray, isDefaultArray, isDistinct, isDiv, isEmptyRelation, isEq, isFalse, isFiniteDomain, isFiniteDomainLT, isGE, isGT, isIDiv, isIff, isImplies, isInt, isIntNum, isIntToBV, isIntToReal, isIsEmptyRelation, isITE, isLabel, isLabelLit, isLE, isLT, isModulus, isMul, isNot, isNumeral, isOEQ, isOr, isProofAndElimination, isProofApplyDef, isProofAsserted, isProofCommutativity, isProofDefAxiom, isProofDefIntro, isProofDER, isProofDistributivity, isProofElimUnusedVars, isProofGoal, isProofHypothesis, isProofIFFFalse, isProofIFFOEQ, isProofIFFTrue, isProofLemma, isProofModusPonens, isProofModusPonensOEQ, isProofMonotonicity, isProofNNFNeg, isProofNNFPos, isProofOrElimination, isProofPullQuant, isProofPushQuant, isProofQuantInst, isProofQuantIntro, isProofReflexivity, isProofRewrite, isProofRewriteStar, isProofSkolemize, isProofSymmetry, isProofTheoryLemma, isProofTransitivity, isProofTransitivityStar, isProofTrue, isProofUnitResolution, isRatNum, isReal, isRealIsInt, isRealToInt, isRelation, isRelationalJoin, isRelationClone, isRelationComplement, isRelationFilter, isRelationNegationFilter, isRelationProject, isRelationRename, isRelationSelect, isRelationStore, isRelationUnion, isRelationWiden, isRemainder, isSelect, isSetComplement, isSetDifference, isSetIntersect, isSetSubset, isSetUnion, isStore, isString, isSub, isTrue, isUMinus, isWellSorted, isXor, simplify, simplify, substitute, substitute, substituteVars, toString, update

Methods inherited from class com.microsoft.z3.AST

compareTo, equals, getASTKind, getId, getSExpr, hashCode, isApp, isExpr, isFuncDecl, isQuantifier, isSort, isVar

Methods inherited from class com.microsoft.z3.Z3Object

arrayLength, arrayToNative

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Method Details

getNumBound

public int getNumBound()

The number of bound variables.

getBoundVariableNames

public Symbol[] getBoundVariableNames()

The symbols for the bound variables.

Throws:

Z3Exception

getBoundVariableSorts

public Sort[] getBoundVariableSorts()

The sorts of the bound variables.

Throws:

Z3Exception

getBody

public Expr<R> getBody()

The body of the quantifier.

Throws:

Z3Exception

translate

public Lambda<R> translate(Context ctx)

Translates (copies) the quantifier to the Context ctx.

Overrides:

translate in class Expr<ArraySort<Sort,R extends Sort>>

Parameters:

ctx - A context

Returns:

A copy of the quantifier which is associated with ctx

Throws:

Z3Exception - on error

of

public static <R extends Sort> Lambda<R> of(Context ctx,
 Sort[] sorts,
 Symbol[] names,
 Expr<R> body)

of

public static <R extends Sort> Lambda<R> of(Context ctx,
 Expr<?>[] bound,
 Expr<R> body)

Parameters:

ctx - Context to create the lambda on.

bound - Bound variables.

body - Body of the lambda expression.