|
Z3
|
|
|
Z3
|
|
Finite-domain expressions More...
Inheritance diagram for FiniteDomainExpr: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... | |
Finite-domain expressions
Definition at line 27 of file FiniteDomainExpr.cs.
1.9.1
