
Expr  Simplify (Params p=null) 
 Returns a simplified version of the expression.


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.


Expr  Substitute (Expr[] from, Expr[] to) 
 Substitute every occurrence of from[i] in the expression with to[i] , for i smaller than num_exprs .


Expr  Substitute (Expr from, Expr to) 
 Substitute every occurrence of from in the expression with to .


Expr  SubstituteVars (Expr[] to) 
 Substitute the free variables in the expression with the expressions in to


new Expr  Translate (Context ctx) 
 Translates (copies) the term to the Context ctx .


override string  ToString () 
 Returns a string representation of the expression.


static bool  operator== (AST a, AST b) 
 Comparison operator.


static bool  operator!= (AST a, AST b) 
 Comparison operator.


FuncDecl  FuncDecl [get] 
 The function declaration of the function that is applied in this expression.


Z3_lbool  BoolValue [get] 
 Indicates whether the expression is the true or false expression or something else (Z3_L_UNDEF).


uint  NumArgs [get] 
 The number of arguments of the expression.


Expr[]  Args [get] 
 The arguments of the expression.


bool  IsNumeral [get] 
 Indicates whether the term is a numeral


bool  IsWellSorted [get] 
 Indicates whether the term is wellsorted.


Sort  Sort [get] 
 The Sort of the term.


bool  IsConst [get] 
 Indicates whether the term represents a constant.


bool  IsIntNum [get] 
 Indicates whether the term is an integer numeral.


bool  IsRatNum [get] 
 Indicates whether the term is a real numeral.


bool  IsAlgebraicNumber [get] 
 Indicates whether the term is an algebraic number


bool  IsBool [get] 
 Indicates whether the term has Boolean sort.


bool  IsTrue [get] 
 Indicates whether the term is the constant true.


bool  IsFalse [get] 
 Indicates whether the term is the constant false.


bool  IsEq [get] 
 Indicates whether the term is an equality predicate.


bool  IsDistinct [get] 
 Indicates whether the term is an nary distinct predicate (every argument is mutually distinct).


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


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


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


bool  IsIff [get] 
 Indicates whether the term is an ifandonlyif (Boolean equivalence, binary)


bool  IsXor [get] 
 Indicates whether the term is an exclusive or


bool  IsNot [get] 
 Indicates whether the term is a negation


bool  IsImplies [get] 
 Indicates whether the term is an implication


bool  IsInt [get] 
 Indicates whether the term is of integer sort.


bool  IsReal [get] 
 Indicates whether the term is of sort real.


bool  IsArithmeticNumeral [get] 
 Indicates whether the term is an arithmetic numeral.


bool  IsLE [get] 
 Indicates whether the term is a lessthanorequal


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


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


bool  IsGT [get] 
 Indicates whether the term is a greaterthan


bool  IsAdd [get] 
 Indicates whether the term is addition (binary)


bool  IsSub [get] 
 Indicates whether the term is subtraction (binary)


bool  IsUMinus [get] 
 Indicates whether the term is a unary minus


bool  IsMul [get] 
 Indicates whether the term is multiplication (binary)


bool  IsDiv [get] 
 Indicates whether the term is division (binary)


bool  IsIDiv [get] 
 Indicates whether the term is integer division (binary)


bool  IsRemainder [get] 
 Indicates whether the term is remainder (binary)


bool  IsModulus [get] 
 Indicates whether the term is modulus (binary)


bool  IsIntToReal [get] 
 Indicates whether the term is a coercion of integer to real (unary)


bool  IsRealToInt [get] 
 Indicates whether the term is a coercion of real to integer (unary)


bool  IsRealIsInt [get] 
 Indicates whether the term is a check that tests whether a real is integral (unary)


bool  IsArray [get] 
 Indicates whether the term is of an array sort.


bool  IsStore [get] 
 Indicates whether the term is an array store.


bool  IsSelect [get] 
 Indicates whether the term is an array select.


bool  IsConstantArray [get] 
 Indicates whether the term is a constant array.


bool  IsDefaultArray [get] 
 Indicates whether the term is a default array.


bool  IsArrayMap [get] 
 Indicates whether the term is an array map.


bool  IsAsArray [get] 
 Indicates whether the term is an asarray term.


bool  IsSetUnion [get] 
 Indicates whether the term is set union


bool  IsSetIntersect [get] 
 Indicates whether the term is set intersection


bool  IsSetDifference [get] 
 Indicates whether the term is set difference


bool  IsSetComplement [get] 
 Indicates whether the term is set complement


bool  IsSetSubset [get] 
 Indicates whether the term is set subset


bool  IsBV [get] 
 Indicates whether the terms is of bitvector sort.


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


bool  IsBVXOR3 [get] 
 Indicates whether the term is a bitvector ternary XOR


bool  IsLabel [get] 
 Indicates whether the term is a label (used by the Boogie Verification condition generator).


bool  IsLabelLit [get] 
 Indicates whether the term is a label literal (used by the Boogie Verification condition generator).


bool  IsOEQ [get] 
 Indicates whether the term is a binary equivalence modulo namings.


bool  IsProofTrue [get] 
 Indicates whether the term is a Proof for the expression 'true'.


bool  IsProofAsserted [get] 
 Indicates whether the term is a proof for a fact asserted by the user.


bool  IsProofGoal [get] 
 Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user.


bool  IsProofModusPonens [get] 
 Indicates whether the term is proof via modus ponens


bool  IsProofReflexivity [get] 
 Indicates whether the term is a proof for (R t t), where R is a reflexive relation.


bool  IsProofSymmetry [get] 
 Indicates whether the term is proof by symmetricity of a relation


bool  IsProofTransitivity [get] 
 Indicates whether the term is a proof by transitivity of a relation


bool  IsProofTransitivityStar [get] 
 Indicates whether the term is a proof by condensed transitivity of a relation


bool  IsProofMonotonicity [get] 
 Indicates whether the term is a monotonicity proof object.


bool  IsProofQuantIntro [get] 
 Indicates whether the term is a quantintro proof


bool  IsProofDistributivity [get] 
 Indicates whether the term is a distributivity proof object.


bool  IsProofAndElimination [get] 
 Indicates whether the term is a proof by elimination of AND


bool  IsProofOrElimination [get] 
 Indicates whether the term is a proof by eliminiation of notor


bool  IsProofRewrite [get] 
 Indicates whether the term is a proof by rewriting


bool  IsProofRewriteStar [get] 
 Indicates whether the term is a proof by rewriting


bool  IsProofPullQuant [get] 
 Indicates whether the term is a proof for pulling quantifiers out.


bool  IsProofPullQuantStar [get] 
 Indicates whether the term is a proof for pulling quantifiers out.


bool  IsProofPushQuant [get] 
 Indicates whether the term is a proof for pushing quantifiers in.


bool  IsProofElimUnusedVars [get] 
 Indicates whether the term is a proof for elimination of unused variables.


bool  IsProofDER [get] 
 Indicates whether the term is a proof for destructive equality resolution


bool  IsProofQuantInst [get] 
 Indicates whether the term is a proof for quantifier instantiation


bool  IsProofHypothesis [get] 
 Indicates whether the term is a hypthesis marker.


bool  IsProofLemma [get] 
 Indicates whether the term is a proof by lemma


bool  IsProofUnitResolution [get] 
 Indicates whether the term is a proof by unit resolution


bool  IsProofIFFTrue [get] 
 Indicates whether the term is a proof by ifftrue


bool  IsProofIFFFalse [get] 
 Indicates whether the term is a proof by ifffalse


bool  IsProofCommutativity [get] 
 Indicates whether the term is a proof by commutativity


bool  IsProofDefAxiom [get] 
 Indicates whether the term is a proof for Tseitinlike axioms


bool  IsProofDefIntro [get] 
 Indicates whether the term is a proof for introduction of a name


bool  IsProofApplyDef [get] 
 Indicates whether the term is a proof for application of a definition


bool  IsProofIFFOEQ [get] 
 Indicates whether the term is a proof iffoeq


bool  IsProofNNFPos [get] 
 Indicates whether the term is a proof for a positive NNF step


bool  IsProofNNFNeg [get] 
 Indicates whether the term is a proof for a negative NNF step


bool  IsProofNNFStar [get] 
 Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.


bool  IsProofCNFStar [get] 
 Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.


bool  IsProofSkolemize [get] 
 Indicates whether the term is a proof for a Skolemization step


bool  IsProofModusPonensOEQ [get] 
 Indicates whether the term is a proof by modus ponens for equisatisfiability.


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


bool  IsRelation [get] 
 Indicates whether the term is of an array sort.


bool  IsRelationStore [get] 
 Indicates whether the term is an relation store


bool  IsEmptyRelation [get] 
 Indicates whether the term is an empty relation


bool  IsIsEmptyRelation [get] 
 Indicates whether the term is a test for the emptiness of a relation


bool  IsRelationalJoin [get] 
 Indicates whether the term is a relational join


bool  IsRelationUnion [get] 
 Indicates whether the term is the union or convex hull of two relations.


bool  IsRelationWiden [get] 
 Indicates whether the term is the widening of two relations


bool  IsRelationProject [get] 
 Indicates whether the term is a projection of columns (provided as numbers in the parameters).


bool  IsRelationFilter [get] 
 Indicates whether the term is a relation filter


bool  IsRelationNegationFilter [get] 
 Indicates whether the term is an intersection of a relation with the negation of another.


bool  IsRelationRename [get] 
 Indicates whether the term is the renaming of a column in a relation


bool  IsRelationComplement [get] 
 Indicates whether the term is the complement of a relation


bool  IsRelationSelect [get] 
 Indicates whether the term is a relational select


bool  IsRelationClone [get] 
 Indicates whether the term is a relational clone (copy)


bool  IsFiniteDomain [get] 
 Indicates whether the term is of an array sort.


bool  IsFiniteDomainLT [get] 
 Indicates whether the term is a less than predicate over a finite domain.


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

