Z3
Public Member Functions | Static Public Member Functions
Lambda Class Reference
+ Inheritance diagram for Lambda:

Public Member Functions

int getNumBound ()
 
Symbol[] getBoundVariableNames ()
 
Sort[] getBoundVariableSorts ()
 
Expr getBody ()
 
Lambda translate (Context ctx)
 
- Public Member Functions inherited from Expr
Expr simplify ()
 
Expr simplify (Params p)
 
FuncDecl getFuncDecl ()
 
Z3_lbool getBoolValue ()
 
int getNumArgs ()
 
Expr[] getArgs ()
 
Expr update (Expr[] args)
 
Expr substitute (Expr[] from, Expr[] to)
 
Expr substitute (Expr from, Expr to)
 
Expr substituteVars (Expr[] to)
 
String toString ()
 
boolean isNumeral ()
 
boolean isWellSorted ()
 
Sort getSort ()
 
boolean isConst ()
 
boolean isIntNum ()
 
boolean isRatNum ()
 
boolean isAlgebraicNumber ()
 
boolean isBool ()
 
boolean isTrue ()
 
boolean isFalse ()
 
boolean isEq ()
 
boolean isDistinct ()
 
boolean isITE ()
 
boolean isAnd ()
 
boolean isOr ()
 
boolean isIff ()
 
boolean isXor ()
 
boolean isNot ()
 
boolean isImplies ()
 
boolean isInt ()
 
boolean isReal ()
 
boolean isArithmeticNumeral ()
 
boolean isLE ()
 
boolean isGE ()
 
boolean isLT ()
 
boolean isGT ()
 
boolean isAdd ()
 
boolean isSub ()
 
boolean isUMinus ()
 
boolean isMul ()
 
boolean isDiv ()
 
boolean isIDiv ()
 
boolean isRemainder ()
 
boolean isModulus ()
 
boolean isIntToReal ()
 
boolean isRealToInt ()
 
boolean isRealIsInt ()
 
boolean isArray ()
 
boolean isStore ()
 
boolean isSelect ()
 
boolean isConstantArray ()
 
boolean isDefaultArray ()
 
boolean isArrayMap ()
 
boolean isAsArray ()
 
boolean isSetUnion ()
 
boolean isSetIntersect ()
 
boolean isSetDifference ()
 
boolean isSetComplement ()
 
boolean isSetSubset ()
 
boolean isBV ()
 
boolean isBVNumeral ()
 
boolean isBVBitOne ()
 
boolean isBVBitZero ()
 
boolean isBVUMinus ()
 
boolean isBVAdd ()
 
boolean isBVSub ()
 
boolean isBVMul ()
 
boolean isBVSDiv ()
 
boolean isBVUDiv ()
 
boolean isBVSRem ()
 
boolean isBVURem ()
 
boolean isBVSMod ()
 
boolean isBVULE ()
 
boolean isBVSLE ()
 
boolean isBVUGE ()
 
boolean isBVSGE ()
 
boolean isBVULT ()
 
boolean isBVSLT ()
 
boolean isBVUGT ()
 
boolean isBVSGT ()
 
boolean isBVAND ()
 
boolean isBVOR ()
 
boolean isBVNOT ()
 
boolean isBVXOR ()
 
boolean isBVNAND ()
 
boolean isBVNOR ()
 
boolean isBVXNOR ()
 
boolean isBVConcat ()
 
boolean isBVSignExtension ()
 
boolean isBVZeroExtension ()
 
boolean isBVExtract ()
 
boolean isBVRepeat ()
 
boolean isBVReduceOR ()
 
boolean isBVReduceAND ()
 
boolean isBVComp ()
 
boolean isBVShiftLeft ()
 
boolean isBVShiftRightLogical ()
 
boolean isBVShiftRightArithmetic ()
 
boolean isBVRotateLeft ()
 
boolean isBVRotateRight ()
 
boolean isBVRotateLeftExtended ()
 
boolean isBVRotateRightExtended ()
 
boolean isIntToBV ()
 
boolean isBVToInt ()
 
boolean isBVCarry ()
 
boolean isBVXOR3 ()
 
boolean isLabel ()
 
boolean isLabelLit ()
 
boolean isString ()
 
String getString ()
 
boolean isConcat ()
 
boolean isOEQ ()
 
boolean isProofTrue ()
 
boolean isProofAsserted ()
 
boolean isProofGoal ()
 
boolean isProofModusPonens ()
 
boolean isProofReflexivity ()
 
boolean isProofSymmetry ()
 
boolean isProofTransitivity ()
 
boolean isProofTransitivityStar ()
 
boolean isProofMonotonicity ()
 
boolean isProofQuantIntro ()
 
boolean isProofDistributivity ()
 
boolean isProofAndElimination ()
 
boolean isProofOrElimination ()
 
boolean isProofRewrite ()
 
boolean isProofRewriteStar ()
 
boolean isProofPullQuant ()
 
boolean isProofPushQuant ()
 
boolean isProofElimUnusedVars ()
 
boolean isProofDER ()
 
boolean isProofQuantInst ()
 
boolean isProofHypothesis ()
 
boolean isProofLemma ()
 
boolean isProofUnitResolution ()
 
boolean isProofIFFTrue ()
 
boolean isProofIFFFalse ()
 
boolean isProofCommutativity ()
 
boolean isProofDefAxiom ()
 
boolean isProofDefIntro ()
 
boolean isProofApplyDef ()
 
boolean isProofIFFOEQ ()
 
boolean isProofNNFPos ()
 
boolean isProofNNFNeg ()
 
boolean isProofSkolemize ()
 
boolean isProofModusPonensOEQ ()
 
boolean isProofTheoryLemma ()
 
boolean isRelation ()
 
boolean isRelationStore ()
 
boolean isEmptyRelation ()
 
boolean isIsEmptyRelation ()
 
boolean isRelationalJoin ()
 
boolean isRelationUnion ()
 
boolean isRelationWiden ()
 
boolean isRelationProject ()
 
boolean isRelationFilter ()
 
boolean isRelationNegationFilter ()
 
boolean isRelationRename ()
 
boolean isRelationComplement ()
 
boolean isRelationSelect ()
 
boolean isRelationClone ()
 
boolean isFiniteDomain ()
 
boolean isFiniteDomainLT ()
 
int getIndex ()
 
- Public Member Functions inherited from AST
boolean equals (Object o)
 
int compareTo (AST other)
 
int hashCode ()
 
int getId ()
 
Z3_ast_kind getASTKind ()
 
boolean isExpr ()
 
boolean isApp ()
 
boolean isVar ()
 
boolean isQuantifier ()
 
boolean isSort ()
 
boolean isFuncDecl ()
 
String getSExpr ()
 

Static Public Member Functions

static Lambda of (Context ctx, Sort[] sorts, Symbol[] names, Expr body)
 
static Lambda of (Context ctx, Expr[] bound, Expr body)
 
- Static Public Member Functions inherited from Z3Object
static long[] arrayToNative (Z3Object[] a)
 
static int arrayLength (Z3Object[] a)
 

Additional Inherited Members

- Protected Member Functions inherited from Expr
 Expr (Context ctx, long obj)
 

Detailed Description

Lambda expressions.

Definition at line 27 of file Lambda.java.

Member Function Documentation

◆ getBody()

Expr getBody ( )
inline

The body of the quantifier.

Exceptions
Z3Exception

Definition at line 73 of file Lambda.java.

74  {
75  return Expr.create(getContext(), Native.getQuantifierBody(getContext()
76  .nCtx(), getNativeObject()));
77  }

◆ getBoundVariableNames()

Symbol [] getBoundVariableNames ( )
inline

The symbols for the bound variables.

Exceptions
Z3Exception

Definition at line 43 of file Lambda.java.

44  {
45  int n = getNumBound();
46  Symbol[] res = new Symbol[n];
47  for (int i = 0; i < n; i++)
48  res[i] = Symbol.create(getContext(), Native.getQuantifierBoundName(
49  getContext().nCtx(), getNativeObject(), i));
50  return res;
51  }

◆ getBoundVariableSorts()

Sort [] getBoundVariableSorts ( )
inline

The sorts of the bound variables.

Exceptions
Z3Exception

Definition at line 58 of file Lambda.java.

59  {
60  int n = getNumBound();
61  Sort[] res = new Sort[n];
62  for (int i = 0; i < n; i++)
63  res[i] = Sort.create(getContext(), Native.getQuantifierBoundSort(
64  getContext().nCtx(), getNativeObject(), i));
65  return res;
66  }

◆ getNumBound()

int getNumBound ( )
inline

The number of bound variables.

Definition at line 33 of file Lambda.java.

34  {
35  return Native.getQuantifierNumBound(getContext().nCtx(), getNativeObject());
36  }

Referenced by Lambda.getBoundVariableNames(), and Lambda.getBoundVariableSorts().

◆ of() [1/2]

static Lambda of ( Context  ctx,
Expr[]  bound,
Expr  body 
)
inlinestatic
Parameters
ctxContext to create the lambda on.
boundBound variables.
bodyBody of the lambda expression.

Definition at line 118 of file Lambda.java.

118  {
119  ctx.checkContextMatch(body);
120 
121 
122  long nativeObject = Native.mkLambdaConst(ctx.nCtx(),
123  AST.arrayLength(bound), AST.arrayToNative(bound),
124  body.getNativeObject());
125  return new Lambda(ctx, nativeObject);
126  }

◆ of() [2/2]

static Lambda of ( Context  ctx,
Sort[]  sorts,
Symbol[]  names,
Expr  body 
)
inlinestatic

Definition at line 94 of file Lambda.java.

95  {
96  ctx.checkContextMatch(sorts);
97  ctx.checkContextMatch(names);
98  ctx.checkContextMatch(body);
99 
100  if (sorts.length != names.length)
101  throw new Z3Exception("Number of sorts does not match number of names");
102 
103 
104  long nativeObject = Native.mkLambda(ctx.nCtx(),
105  AST.arrayLength(sorts), AST.arrayToNative(sorts),
106  Symbol.arrayToNative(names),
107  body.getNativeObject());
108 
109  return new Lambda(ctx, nativeObject);
110  }

Referenced by Context.mkLambda().

◆ translate()

Lambda translate ( Context  ctx)
inline

Translates (copies) the quantifier to the Context

ctx

.

Parameters
ctxA context
Returns
A copy of the quantifier which is associated with
ctx
Exceptions
Z3Exceptionon error

Reimplemented from Expr.

Definition at line 88 of file Lambda.java.

89  {
90  return (Lambda) super.translate(ctx);
91  }

Referenced by Lambda.translate().

com.microsoft.z3.Expr.Expr
Expr(Context ctx, long obj)
Definition: Expr.java:2096
com.microsoft.z3.Lambda.getNumBound
int getNumBound()
Definition: Lambda.java:33