All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages

ArrayExpr Class Reference

Array expressions More...

Inheritance diagram for ArrayExpr:

## Protected Member Functions | |

ArrayExpr (Context ctx) | |

Constructor for ArrayExpr | |

Protected Member Functions inherited from Expr | |

Expr (Context ctx) | |

Constructor for Expr | |

Expr (Context ctx, IntPtr obj) | |

Constructor for Expr | |

## Additional Inherited Members | |

Public Member Functions inherited from Expr | |

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 Public Member Functions inherited from AST | |

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

Comparison operator. | |

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

Comparison operator. | |

Properties inherited from Expr | |

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

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 n-ary distinct predicate (every argument is mutually distinct). | |

bool | IsITE` [get]` |

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

bool | IsAnd` [get]` |

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

bool | IsOr` [get]` |

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

bool | IsIff` [get]` |

Indicates whether the term is an if-and-only-if (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 less-than-or-equal | |

bool | IsGE` [get]` |

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

bool | IsLT` [get]` |

Indicates whether the term is a less-than | |

bool | IsGT` [get]` |

Indicates whether the term is a greater-than | |

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 as-array 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 bit-vector sort. | |

bool | IsBVNumeral` [get]` |

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

bool | IsBVBitOne` [get]` |

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

bool | IsBVBitZero` [get]` |

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

bool | IsBVUMinus` [get]` |

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

bool | IsBVAdd` [get]` |

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

bool | IsBVSub` [get]` |

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

bool | IsBVMul` [get]` |

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

bool | IsBVSDiv` [get]` |

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

bool | IsBVUDiv` [get]` |

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

bool | IsBVSRem` [get]` |

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

bool | IsBVURem` [get]` |

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

bool | IsBVSMod` [get]` |

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

bool | IsBVULE` [get]` |

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

bool | IsBVSLE` [get]` |

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

bool | IsBVUGE` [get]` |

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

bool | IsBVSGE` [get]` |

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

bool | IsBVULT` [get]` |

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

bool | IsBVSLT` [get]` |

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

bool | IsBVUGT` [get]` |

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

bool | IsBVSGT` [get]` |

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

bool | IsBVAND` [get]` |

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

bool | IsBVOR` [get]` |

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

bool | IsBVNOT` [get]` |

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

bool | IsBVXOR` [get]` |

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

bool | IsBVNAND` [get]` |

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

bool | IsBVNOR` [get]` |

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

bool | IsBVXNOR` [get]` |

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

bool | IsBVConcat` [get]` |

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

bool | IsBVSignExtension` [get]` |

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

bool | IsBVZeroExtension` [get]` |

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

bool | IsBVExtract` [get]` |

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

bool | IsBVRepeat` [get]` |

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

bool | IsBVReduceOR` [get]` |

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

bool | IsBVReduceAND` [get]` |

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

bool | IsBVComp` [get]` |

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

bool | IsBVShiftLeft` [get]` |

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

bool | IsBVShiftRightLogical` [get]` |

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

bool | IsBVShiftRightArithmetic` [get]` |

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

bool | IsBVRotateLeft` [get]` |

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

bool | IsBVRotateRight` [get]` |

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

bool | IsBVRotateLeftExtended` [get]` |

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

bool | IsBVRotateRightExtended` [get]` |

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

bool | IsIntToBV` [get]` |

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

bool | IsBVToInt` [get]` |

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

bool | IsBVCarry` [get]` |

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

bool | IsBVXOR3` [get]` |

Indicates whether the term is a bit-vector 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 quant-intro 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 not-or | |

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 iff-true | |

bool | IsProofIFFFalse` [get]` |

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

bool | IsProofCommutativity` [get]` |

Indicates whether the term is a proof by commutativity | |

bool | IsProofDefAxiom` [get]` |

Indicates whether the term is a proof for Tseitin-like 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 iff-oeq | |

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

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 de-Burijn index of a bound variable. | |

Generated on Thu Nov 22 2012 18:37:21 for Z3 by 1.8.2