DatatypeExpr Class Reference

Datatype expressions More...

Inheritance diagram for DatatypeExpr:

## Additional Inherited Members | |

Public Member Functions inherited from Expr | |

Expr | Simplify (Params p=null) |

Returns a simplified version of the expression. More... | |

Expr | Arg (uint i) |

The i'th argument of the expression. More... | |

void | Update (Expr[] args) |

Update the arguments of the expression using the arguments args The number of new arguments should coincide with the current number of arguments. More... | |

Expr | Substitute (Expr[] from, Expr[] to) |

Substitute every occurrence of `from[i]` in the expression with `to[i]` , for `i` smaller than `num_exprs` . More... | |

Expr | Substitute (Expr from, Expr to) |

Substitute every occurrence of `from` in the expression with `to` . More... | |

Expr | SubstituteVars (Expr[] to) |

Substitute the free variables in the expression with the expressions in to More... | |

new Expr | Translate (Context ctx) |

Translates (copies) the term to the Context ctx . More... | |

Expr | Dup () |

Create a duplicate of expression. This feature is to allow extending the life-time of expressions that were passed down as arguments by the user propagator callbacks. By default the life-time of arguments to callbacks is within the callback only. More... | |

override string | ToString () |

Returns a string representation of the expression. More... | |

Public Member Functions inherited from AST | |

override bool | Equals (object o) |

Object comparison. More... | |

virtual int | CompareTo (object other) |

Object Comparison. More... | |

override int | GetHashCode () |

The AST's hash code. More... | |

AST | Translate (Context ctx) |

Translates (copies) the AST to the Context ctx . More... | |

override string | ToString () |

A string representation of the AST. More... | |

string | SExpr () |

A string representation of the AST in s-expression notation. More... | |

Public Member Functions inherited from Z3Object | |

void | Dispose () |

Disposes of the underlying native Z3 object. More... | |

Static Public Member Functions inherited from AST | |

static bool | operator== (AST a, AST b) |

Comparison operator. More... | |

static bool | operator!= (AST a, AST b) |

Comparison operator. More... | |

Protected Member Functions inherited from Expr | |

Expr (Context ctx, IntPtr obj) | |

Constructor for Expr More... | |

Properties inherited from Expr | |

FuncDecl | FuncDecl` [get]` |

The function declaration of the function that is applied in this expression. More... | |

Z3_lbool | BoolValue` [get]` |

Indicates whether the expression is the true or false expression or something else (Z3_L_UNDEF). More... | |

uint | NumArgs` [get]` |

The number of arguments of the expression. More... | |

Expr[] | Args` [get]` |

The arguments of the expression. More... | |

bool | IsNumeral` [get]` |

Indicates whether the term is a numeral More... | |

bool | IsWellSorted` [get]` |

Indicates whether the term is well-sorted. More... | |

Sort | Sort` [get]` |

The Sort of the term. More... | |

bool | IsConst` [get]` |

Indicates whether the term represents a constant. More... | |

bool | IsIntNum` [get]` |

Indicates whether the term is an integer numeral. More... | |

bool | IsRatNum` [get]` |

Indicates whether the term is a real numeral. More... | |

bool | IsAlgebraicNumber` [get]` |

Indicates whether the term is an algebraic number More... | |

bool | IsBool` [get]` |

Indicates whether the term has Boolean sort. More... | |

bool | IsTrue` [get]` |

Indicates whether the term is the constant true. More... | |

bool | IsFalse` [get]` |

Indicates whether the term is the constant false. More... | |

bool | IsEq` [get]` |

Indicates whether the term is an equality predicate. More... | |

bool | IsDistinct` [get]` |

Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct). More... | |

bool | IsITE` [get]` |

Indicates whether the term is a ternary if-then-else term More... | |

bool | IsAnd` [get]` |

Indicates whether the term is an n-ary conjunction More... | |

bool | IsOr` [get]` |

Indicates whether the term is an n-ary disjunction More... | |

bool | IsIff` [get]` |

Indicates whether the term is an if-and-only-if (Boolean equivalence, binary) More... | |

bool | IsXor` [get]` |

Indicates whether the term is an exclusive or More... | |

bool | IsNot` [get]` |

Indicates whether the term is a negation More... | |

bool | IsImplies` [get]` |

Indicates whether the term is an implication More... | |

bool | IsAtMost` [get]` |

Indicates whether the term is at-most More... | |

uint | AtMostBound` [get]` |

Retrieve bound of at-most More... | |

bool | IsAtLeast` [get]` |

Indicates whether the term is at-least More... | |

uint | AtLeastBound` [get]` |

Retrieve bound of at-least More... | |

bool | IsPbEq` [get]` |

Indicates whether the term is pbeq More... | |

bool | IsPbLe` [get]` |

Indicates whether the term is pble More... | |

bool | IsPbGe` [get]` |

Indicates whether the term is pbge More... | |

bool | IsInt` [get]` |

Indicates whether the term is of integer sort. More... | |

bool | IsReal` [get]` |

Indicates whether the term is of sort real. More... | |

bool | IsArithmeticNumeral` [get]` |

Indicates whether the term is an arithmetic numeral. More... | |

bool | IsLE` [get]` |

Indicates whether the term is a less-than-or-equal More... | |

bool | IsGE` [get]` |

Indicates whether the term is a greater-than-or-equal More... | |

bool | IsLT` [get]` |

Indicates whether the term is a less-than More... | |

bool | IsGT` [get]` |

Indicates whether the term is a greater-than More... | |

bool | IsAdd` [get]` |

Indicates whether the term is addition (binary) More... | |

bool | IsSub` [get]` |

Indicates whether the term is subtraction (binary) More... | |

bool | IsUMinus` [get]` |

Indicates whether the term is a unary minus More... | |

bool | IsMul` [get]` |

Indicates whether the term is multiplication (binary) More... | |

bool | IsDiv` [get]` |

Indicates whether the term is division (binary) More... | |

bool | IsIDiv` [get]` |

Indicates whether the term is integer division (binary) More... | |

bool | IsRemainder` [get]` |

Indicates whether the term is remainder (binary) More... | |

bool | IsModulus` [get]` |

Indicates whether the term is modulus (binary) More... | |

bool | IsIntToReal` [get]` |

Indicates whether the term is a coercion of integer to real (unary) More... | |

bool | IsRealToInt` [get]` |

Indicates whether the term is a coercion of real to integer (unary) More... | |

bool | IsRealIsInt` [get]` |

Indicates whether the term is a check that tests whether a real is integral (unary) More... | |

bool | IsArray` [get]` |

Indicates whether the term is of an array sort. More... | |

bool | IsStore` [get]` |

Indicates whether the term is an array store. More... | |

bool | IsSelect` [get]` |

Indicates whether the term is an array select. More... | |

bool | IsConstantArray` [get]` |

Indicates whether the term is a constant array. More... | |

bool | IsDefaultArray` [get]` |

Indicates whether the term is a default array. More... | |

bool | IsArrayMap` [get]` |

Indicates whether the term is an array map. More... | |

bool | IsAsArray` [get]` |

Indicates whether the term is an as-array term. More... | |

bool | IsSetUnion` [get]` |

Indicates whether the term is set union More... | |

bool | IsSetIntersect` [get]` |

Indicates whether the term is set intersection More... | |

bool | IsSetDifference` [get]` |

Indicates whether the term is set difference More... | |

bool | IsSetComplement` [get]` |

Indicates whether the term is set complement More... | |

bool | IsSetSubset` [get]` |

Indicates whether the term is set subset More... | |

bool | IsBV` [get]` |

Indicates whether the terms is of bit-vector sort. More... | |

bool | IsBVNumeral` [get]` |

Indicates whether the term is a bit-vector numeral More... | |

bool | IsBVBitOne` [get]` |

Indicates whether the term is a one-bit bit-vector with value one More... | |

bool | IsBVBitZero` [get]` |

Indicates whether the term is a one-bit bit-vector with value zero More... | |

bool | IsBVUMinus` [get]` |

Indicates whether the term is a bit-vector unary minus More... | |

bool | IsBVAdd` [get]` |

Indicates whether the term is a bit-vector addition (binary) More... | |

bool | IsBVSub` [get]` |

Indicates whether the term is a bit-vector subtraction (binary) More... | |

bool | IsBVMul` [get]` |

Indicates whether the term is a bit-vector multiplication (binary) More... | |

bool | IsBVSDiv` [get]` |

Indicates whether the term is a bit-vector signed division (binary) More... | |

bool | IsBVUDiv` [get]` |

Indicates whether the term is a bit-vector unsigned division (binary) More... | |

bool | IsBVSRem` [get]` |

Indicates whether the term is a bit-vector signed remainder (binary) More... | |

bool | IsBVURem` [get]` |

Indicates whether the term is a bit-vector unsigned remainder (binary) More... | |

bool | IsBVSMod` [get]` |

Indicates whether the term is a bit-vector signed modulus More... | |

bool | IsBVULE` [get]` |

Indicates whether the term is an unsigned bit-vector less-than-or-equal More... | |

bool | IsBVSLE` [get]` |

Indicates whether the term is a signed bit-vector less-than-or-equal More... | |

bool | IsBVUGE` [get]` |

Indicates whether the term is an unsigned bit-vector greater-than-or-equal More... | |

bool | IsBVSGE` [get]` |

Indicates whether the term is a signed bit-vector greater-than-or-equal More... | |

bool | IsBVULT` [get]` |

Indicates whether the term is an unsigned bit-vector less-than More... | |

bool | IsBVSLT` [get]` |

Indicates whether the term is a signed bit-vector less-than More... | |

bool | IsBVUGT` [get]` |

Indicates whether the term is an unsigned bit-vector greater-than More... | |

bool | IsBVSGT` [get]` |

Indicates whether the term is a signed bit-vector greater-than More... | |

bool | IsBVAND` [get]` |

Indicates whether the term is a bit-wise AND More... | |

bool | IsBVOR` [get]` |

Indicates whether the term is a bit-wise OR More... | |

bool | IsBVNOT` [get]` |

Indicates whether the term is a bit-wise NOT More... | |

bool | IsBVXOR` [get]` |

Indicates whether the term is a bit-wise XOR More... | |

bool | IsBVNAND` [get]` |

Indicates whether the term is a bit-wise NAND More... | |

bool | IsBVNOR` [get]` |

Indicates whether the term is a bit-wise NOR More... | |

bool | IsBVXNOR` [get]` |

Indicates whether the term is a bit-wise XNOR More... | |

bool | IsBVConcat` [get]` |

Indicates whether the term is a bit-vector concatenation (binary) More... | |

bool | IsBVSignExtension` [get]` |

Indicates whether the term is a bit-vector sign extension More... | |

bool | IsBVZeroExtension` [get]` |

Indicates whether the term is a bit-vector zero extension More... | |

bool | IsBVExtract` [get]` |

Indicates whether the term is a bit-vector extraction More... | |

bool | IsBVRepeat` [get]` |

Indicates whether the term is a bit-vector repetition More... | |

bool | IsBVReduceOR` [get]` |

Indicates whether the term is a bit-vector reduce OR More... | |

bool | IsBVReduceAND` [get]` |

Indicates whether the term is a bit-vector reduce AND More... | |

bool | IsBVComp` [get]` |

Indicates whether the term is a bit-vector comparison More... | |

bool | IsBVShiftLeft` [get]` |

Indicates whether the term is a bit-vector shift left More... | |

bool | IsBVShiftRightLogical` [get]` |

Indicates whether the term is a bit-vector logical shift right More... | |

bool | IsBVShiftRightArithmetic` [get]` |

Indicates whether the term is a bit-vector arithmetic shift left More... | |

bool | IsBVRotateLeft` [get]` |

Indicates whether the term is a bit-vector rotate left More... | |

bool | IsBVRotateRight` [get]` |

Indicates whether the term is a bit-vector rotate right More... | |

bool | IsBVRotateLeftExtended` [get]` |

Indicates whether the term is a bit-vector rotate left (extended) More... | |

bool | IsBVRotateRightExtended` [get]` |

Indicates whether the term is a bit-vector rotate right (extended) More... | |

bool | IsIntToBV` [get]` |

Indicates whether the term is a coercion from integer to bit-vector More... | |

bool | IsBVToInt` [get]` |

Indicates whether the term is a coercion from bit-vector to integer More... | |

bool | IsBVCarry` [get]` |

Indicates whether the term is a bit-vector carry More... | |

bool | IsBVXOR3` [get]` |

Indicates whether the term is a bit-vector ternary XOR More... | |

bool | IsLabel` [get]` |

Indicates whether the term is a label (used by the Boogie Verification condition generator). More... | |

bool | IsLabelLit` [get]` |

Indicates whether the term is a label literal (used by the Boogie Verification condition generator). More... | |

bool | IsString` [get]` |

Check whether expression is a string constant. More... | |

string | String` [get]` |

Retrieve string corresponding to string constant. More... | |

bool | IsConcat` [get]` |

Check whether expression is a concatenation. More... | |

bool | IsPrefix` [get]` |

Check whether expression is a prefix. More... | |

bool | IsSuffix` [get]` |

Check whether expression is a suffix. More... | |

bool | IsContains` [get]` |

Check whether expression is a contains. More... | |

bool | IsExtract` [get]` |

Check whether expression is an extract. More... | |

bool | IsReplace` [get]` |

Check whether expression is a replace. More... | |

bool | IsAt` [get]` |

Check whether expression is an at. More... | |

bool | IsLength` [get]` |

Check whether expression is a sequence length. More... | |

bool | IsIndex` [get]` |

Check whether expression is a sequence index. More... | |

bool | IsOEQ` [get]` |

Indicates whether the term is a binary equivalence modulo namings. More... | |

bool | IsProofTrue` [get]` |

Indicates whether the term is a Proof for the expression 'true'. More... | |

bool | IsProofAsserted` [get]` |

Indicates whether the term is a proof for a fact asserted by the user. More... | |

bool | IsProofGoal` [get]` |

Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user. More... | |

bool | IsProofModusPonens` [get]` |

Indicates whether the term is proof via modus ponens More... | |

bool | IsProofReflexivity` [get]` |

Indicates whether the term is a proof for (R t t), where R is a reflexive relation. More... | |

bool | IsProofSymmetry` [get]` |

Indicates whether the term is proof by symmetricity of a relation More... | |

bool | IsProofTransitivity` [get]` |

Indicates whether the term is a proof by transitivity of a relation More... | |

bool | IsProofTransitivityStar` [get]` |

Indicates whether the term is a proof by condensed transitivity of a relation More... | |

bool | IsProofMonotonicity` [get]` |

Indicates whether the term is a monotonicity proof object. More... | |

bool | IsProofQuantIntro` [get]` |

Indicates whether the term is a quant-intro proof More... | |

bool | IsProofDistributivity` [get]` |

Indicates whether the term is a distributivity proof object. More... | |

bool | IsProofAndElimination` [get]` |

Indicates whether the term is a proof by elimination of AND More... | |

bool | IsProofOrElimination` [get]` |

Indicates whether the term is a proof by elimination of not-or More... | |

bool | IsProofRewrite` [get]` |

Indicates whether the term is a proof by rewriting More... | |

bool | IsProofRewriteStar` [get]` |

Indicates whether the term is a proof by rewriting More... | |

bool | IsProofPullQuant` [get]` |

Indicates whether the term is a proof for pulling quantifiers out. More... | |

bool | IsProofPushQuant` [get]` |

Indicates whether the term is a proof for pushing quantifiers in. More... | |

bool | IsProofElimUnusedVars` [get]` |

Indicates whether the term is a proof for elimination of unused variables. More... | |

bool | IsProofDER` [get]` |

Indicates whether the term is a proof for destructive equality resolution More... | |

bool | IsProofQuantInst` [get]` |

Indicates whether the term is a proof for quantifier instantiation More... | |

bool | IsProofHypothesis` [get]` |

Indicates whether the term is a hypothesis marker. More... | |

bool | IsProofLemma` [get]` |

Indicates whether the term is a proof by lemma More... | |

bool | IsProofUnitResolution` [get]` |

Indicates whether the term is a proof by unit resolution More... | |

bool | IsProofIFFTrue` [get]` |

Indicates whether the term is a proof by iff-true More... | |

bool | IsProofIFFFalse` [get]` |

Indicates whether the term is a proof by iff-false More... | |

bool | IsProofCommutativity` [get]` |

Indicates whether the term is a proof by commutativity More... | |

bool | IsProofDefAxiom` [get]` |

Indicates whether the term is a proof for Tseitin-like axioms More... | |

bool | IsProofDefIntro` [get]` |

Indicates whether the term is a proof for introduction of a name More... | |

bool | IsProofApplyDef` [get]` |

Indicates whether the term is a proof for application of a definition More... | |

bool | IsProofIFFOEQ` [get]` |

Indicates whether the term is a proof iff-oeq More... | |

bool | IsProofNNFPos` [get]` |

Indicates whether the term is a proof for a positive NNF step More... | |

bool | IsProofNNFNeg` [get]` |

Indicates whether the term is a proof for a negative NNF step More... | |

bool | IsProofSkolemize` [get]` |

Indicates whether the term is a proof for a Skolemization step More... | |

bool | IsProofModusPonensOEQ` [get]` |

Indicates whether the term is a proof by modus ponens for equi-satisfiability. More... | |

bool | IsProofTheoryLemma` [get]` |

Indicates whether the term is a proof for theory lemma More... | |

bool | IsRelation` [get]` |

Indicates whether the term is of relation sort. More... | |

bool | IsRelationStore` [get]` |

Indicates whether the term is an relation store More... | |

bool | IsEmptyRelation` [get]` |

Indicates whether the term is an empty relation More... | |

bool | IsIsEmptyRelation` [get]` |

Indicates whether the term is a test for the emptiness of a relation More... | |

bool | IsRelationalJoin` [get]` |

Indicates whether the term is a relational join More... | |

bool | IsRelationUnion` [get]` |

Indicates whether the term is the union or convex hull of two relations. More... | |

bool | IsRelationWiden` [get]` |

Indicates whether the term is the widening of two relations More... | |

bool | IsRelationProject` [get]` |

Indicates whether the term is a projection of columns (provided as numbers in the parameters). More... | |

bool | IsRelationFilter` [get]` |

Indicates whether the term is a relation filter More... | |

bool | IsRelationNegationFilter` [get]` |

Indicates whether the term is an intersection of a relation with the negation of another. More... | |

bool | IsRelationRename` [get]` |

Indicates whether the term is the renaming of a column in a relation More... | |

bool | IsRelationComplement` [get]` |

Indicates whether the term is the complement of a relation More... | |

bool | IsRelationSelect` [get]` |

Indicates whether the term is a relational select More... | |

bool | IsRelationClone` [get]` |

Indicates whether the term is a relational clone (copy) More... | |

bool | IsFiniteDomain` [get]` |

Indicates whether the term is of an array sort. More... | |

bool | IsFiniteDomainLT` [get]` |

Indicates whether the term is a less than predicate over a finite domain. More... | |

bool | IsFP` [get]` |

Indicates whether the terms is of floating-point sort. More... | |

bool | IsFPRM` [get]` |

Indicates whether the terms is of floating-point rounding mode sort. More... | |

bool | IsFPNumeral` [get]` |

Indicates whether the term is a floating-point numeral More... | |

bool | IsFPRMNumeral` [get]` |

Indicates whether the term is a floating-point rounding mode numeral More... | |

bool | IsFPRMRoundNearestTiesToEven` [get]` |

Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven More... | |

bool | IsFPRMRoundNearestTiesToAway` [get]` |

Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway More... | |

bool | IsFPRMRoundTowardNegative` [get]` |

Indicates whether the term is the floating-point rounding numeral roundTowardNegative More... | |

bool | IsFPRMRoundTowardPositive` [get]` |

Indicates whether the term is the floating-point rounding numeral roundTowardPositive More... | |

bool | IsFPRMRoundTowardZero` [get]` |

Indicates whether the term is the floating-point rounding numeral roundTowardZero More... | |

bool | IsFPRMExprRNE` [get]` |

Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven More... | |

bool | IsFPRMExprRNA` [get]` |

Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway More... | |

bool | IsFPRMExprRTN` [get]` |

Indicates whether the term is the floating-point rounding numeral roundTowardNegative More... | |

bool | IsFPRMExprRTP` [get]` |

Indicates whether the term is the floating-point rounding numeral roundTowardPositive More... | |

bool | IsFPRMExprRTZ` [get]` |

Indicates whether the term is the floating-point rounding numeral roundTowardZero More... | |

bool | IsFPRMExpr` [get]` |

Indicates whether the term is a floating-point rounding mode numeral More... | |

bool | IsFPPlusInfinity` [get]` |

Indicates whether the term is a floating-point +oo More... | |

bool | IsFPMinusInfinity` [get]` |

Indicates whether the term is a floating-point -oo More... | |

bool | IsFPNaN` [get]` |

Indicates whether the term is a floating-point NaN More... | |

bool | IsFPPlusZero` [get]` |

bool | IsFPMinusZero` [get]` |

Indicates whether the term is a floating-point -zero More... | |

bool | IsFPAdd` [get]` |

Indicates whether the term is a floating-point addition term More... | |

bool | IsFPSub` [get]` |

Indicates whether the term is a floating-point subtraction term More... | |

bool | IsFPNeg` [get]` |

Indicates whether the term is a floating-point negation term More... | |

bool | IsFPMul` [get]` |

Indicates whether the term is a floating-point multiplication term More... | |

bool | IsFPDiv` [get]` |

Indicates whether the term is a floating-point division term More... | |

bool | IsFPRem` [get]` |

Indicates whether the term is a floating-point remainder term More... | |

bool | IsFPAbs` [get]` |

Indicates whether the term is a floating-point term absolute value term More... | |

bool | IsFPMin` [get]` |

Indicates whether the term is a floating-point minimum term More... | |

bool | IsFPMax` [get]` |

Indicates whether the term is a floating-point maximum term More... | |

bool | IsFPFMA` [get]` |

Indicates whether the term is a floating-point fused multiply-add term More... | |

bool | IsFPSqrt` [get]` |

Indicates whether the term is a floating-point square root term More... | |

bool | IsFPRoundToIntegral` [get]` |

Indicates whether the term is a floating-point roundToIntegral term More... | |

bool | IsFPEq` [get]` |

Indicates whether the term is a floating-point equality term More... | |

bool | IsFPLt` [get]` |

Indicates whether the term is a floating-point less-than term More... | |

bool | IsFPGt` [get]` |

Indicates whether the term is a floating-point greater-than term More... | |

bool | IsFPLe` [get]` |

Indicates whether the term is a floating-point less-than or equal term More... | |

bool | IsFPGe` [get]` |

Indicates whether the term is a floating-point greater-than or equal term More... | |

bool | IsFPisNaN` [get]` |

Indicates whether the term is a floating-point isNaN predicate term More... | |

bool | IsFPisInf` [get]` |

Indicates whether the term is a floating-point isInf predicate term More... | |

bool | IsFPisZero` [get]` |

Indicates whether the term is a floating-point isZero predicate term More... | |

bool | IsFPisNormal` [get]` |

Indicates whether the term is a floating-point isNormal term More... | |

bool | IsFPisSubnormal` [get]` |

Indicates whether the term is a floating-point isSubnormal predicate term More... | |

bool | IsFPisNegative` [get]` |

Indicates whether the term is a floating-point isNegative predicate term More... | |

bool | IsFPisPositive` [get]` |

Indicates whether the term is a floating-point isPositive predicate term More... | |

bool | IsFPFP` [get]` |

Indicates whether the term is a floating-point constructor term More... | |

bool | IsFPToFp` [get]` |

Indicates whether the term is a floating-point conversion term More... | |

bool | IsFPToFpUnsigned` [get]` |

Indicates whether the term is a floating-point conversion from unsigned bit-vector term More... | |

bool | IsFPToUBV` [get]` |

Indicates whether the term is a floating-point conversion to unsigned bit-vector term More... | |

bool | IsFPToSBV` [get]` |

Indicates whether the term is a floating-point conversion to signed bit-vector term More... | |

bool | IsFPToReal` [get]` |

Indicates whether the term is a floating-point conversion to real term More... | |

bool | IsFPToIEEEBV` [get]` |

Indicates whether the term is a floating-point conversion to IEEE-754 bit-vector term More... | |

uint | Index` [get]` |

The de-Bruijn index of a bound variable. More... | |

Properties inherited from AST | |

uint | Id` [get]` |

A unique identifier for the AST (unique among all ASTs). More... | |

Z3_ast_kind | ASTKind` [get]` |

The kind of the AST. More... | |

bool | IsExpr` [get]` |

Indicates whether the AST is an Expr More... | |

bool | IsApp` [get]` |

Indicates whether the AST is an application More... | |

bool | IsVar` [get]` |

Indicates whether the AST is a BoundVariable More... | |

bool | IsQuantifier` [get]` |

Indicates whether the AST is a Quantifier More... | |

bool | IsSort` [get]` |

Indicates whether the AST is a Sort More... | |

bool | IsFuncDecl` [get]` |

Indicates whether the AST is a FunctionDeclaration More... | |

Properties inherited from Z3Object | |

Context | Context` [get]` |

Access Context object More... | |

Datatype expressions

Definition at line 31 of file DatatypeExpr.cs.

Generated on Sat Jan 14 2023 14:44:09 for Z3 by 1.9.1