
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 wellsorted. 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 nary distinct predicate (every argument is mutually distinct). More...


bool  IsITE [get] 
 Indicates whether the term is a ternary ifthenelse term More...


bool  IsAnd [get] 
 Indicates whether the term is an nary conjunction More...


bool  IsOr [get] 
 Indicates whether the term is an nary disjunction More...


bool  IsIff [get] 
 Indicates whether the term is an ifandonlyif (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  IsInterpolant [get] 
 Indicates whether the term is marked for interpolation. 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 lessthanorequal More...


bool  IsGE [get] 
 Indicates whether the term is a greaterthanorequal More...


bool  IsLT [get] 
 Indicates whether the term is a lessthan More...


bool  IsGT [get] 
 Indicates whether the term is a greaterthan 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 asarray 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 bitvector sort. More...


bool  IsBVNumeral [get] 
 Indicates whether the term is a bitvector numeral More...


bool  IsBVBitOne [get] 
 Indicates whether the term is a onebit bitvector with value one More...


bool  IsBVBitZero [get] 
 Indicates whether the term is a onebit bitvector with value zero More...


bool  IsBVUMinus [get] 
 Indicates whether the term is a bitvector unary minus More...


bool  IsBVAdd [get] 
 Indicates whether the term is a bitvector addition (binary) More...


bool  IsBVSub [get] 
 Indicates whether the term is a bitvector subtraction (binary) More...


bool  IsBVMul [get] 
 Indicates whether the term is a bitvector multiplication (binary) More...


bool  IsBVSDiv [get] 
 Indicates whether the term is a bitvector signed division (binary) More...


bool  IsBVUDiv [get] 
 Indicates whether the term is a bitvector unsigned division (binary) More...


bool  IsBVSRem [get] 
 Indicates whether the term is a bitvector signed remainder (binary) More...


bool  IsBVURem [get] 
 Indicates whether the term is a bitvector unsigned remainder (binary) More...


bool  IsBVSMod [get] 
 Indicates whether the term is a bitvector signed modulus More...


bool  IsBVULE [get] 
 Indicates whether the term is an unsigned bitvector lessthanorequal More...


bool  IsBVSLE [get] 
 Indicates whether the term is a signed bitvector lessthanorequal More...


bool  IsBVUGE [get] 
 Indicates whether the term is an unsigned bitvector greaterthanorequal More...


bool  IsBVSGE [get] 
 Indicates whether the term is a signed bitvector greaterthanorequal More...


bool  IsBVULT [get] 
 Indicates whether the term is an unsigned bitvector lessthan More...


bool  IsBVSLT [get] 
 Indicates whether the term is a signed bitvector lessthan More...


bool  IsBVUGT [get] 
 Indicates whether the term is an unsigned bitvector greaterthan More...


bool  IsBVSGT [get] 
 Indicates whether the term is a signed bitvector greaterthan More...


bool  IsBVAND [get] 
 Indicates whether the term is a bitwise AND More...


bool  IsBVOR [get] 
 Indicates whether the term is a bitwise OR More...


bool  IsBVNOT [get] 
 Indicates whether the term is a bitwise NOT More...


bool  IsBVXOR [get] 
 Indicates whether the term is a bitwise XOR More...


bool  IsBVNAND [get] 
 Indicates whether the term is a bitwise NAND More...


bool  IsBVNOR [get] 
 Indicates whether the term is a bitwise NOR More...


bool  IsBVXNOR [get] 
 Indicates whether the term is a bitwise XNOR More...


bool  IsBVConcat [get] 
 Indicates whether the term is a bitvector concatenation (binary) More...


bool  IsBVSignExtension [get] 
 Indicates whether the term is a bitvector sign extension More...


bool  IsBVZeroExtension [get] 
 Indicates whether the term is a bitvector zero extension More...


bool  IsBVExtract [get] 
 Indicates whether the term is a bitvector extraction More...


bool  IsBVRepeat [get] 
 Indicates whether the term is a bitvector repetition More...


bool  IsBVReduceOR [get] 
 Indicates whether the term is a bitvector reduce OR More...


bool  IsBVReduceAND [get] 
 Indicates whether the term is a bitvector reduce AND More...


bool  IsBVComp [get] 
 Indicates whether the term is a bitvector comparison More...


bool  IsBVShiftLeft [get] 
 Indicates whether the term is a bitvector shift left More...


bool  IsBVShiftRightLogical [get] 
 Indicates whether the term is a bitvector logical shift right More...


bool  IsBVShiftRightArithmetic [get] 
 Indicates whether the term is a bitvector arithmetic shift left More...


bool  IsBVRotateLeft [get] 
 Indicates whether the term is a bitvector rotate left More...


bool  IsBVRotateRight [get] 
 Indicates whether the term is a bitvector rotate right More...


bool  IsBVRotateLeftExtended [get] 
 Indicates whether the term is a bitvector rotate left (extended) More...


bool  IsBVRotateRightExtended [get] 
 Indicates whether the term is a bitvector rotate right (extended) More...


bool  IsIntToBV [get] 
 Indicates whether the term is a coercion from integer to bitvector More...


bool  IsBVToInt [get] 
 Indicates whether the term is a coercion from bitvector to integer More...


bool  IsBVCarry [get] 
 Indicates whether the term is a bitvector carry More...


bool  IsBVXOR3 [get] 
 Indicates whether the term is a bitvector 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  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 quantintro 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 eliminiation of notor 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  IsProofPullQuantStar [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 hypthesis 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 ifftrue More...


bool  IsProofIFFFalse [get] 
 Indicates whether the term is a proof by ifffalse 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 Tseitinlike 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 iffoeq 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  IsProofNNFStar [get] 
 Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form. More...


bool  IsProofCNFStar [get] 
 Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form. 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 equisatisfiability. More...


bool  IsProofTheoryLemma [get] 
 Indicates whether the term is a proof for theory lemma More...


bool  IsRelation [get] 
 Indicates whether the term is of an array 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...


uint  Index [get] 
 The deBurijn index of a bound variable. More...


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...

