Z3 |

Static Public Member Functions
ArithExpr Class Reference

Arithmetic expressions (int/real) More...

Inheritance diagram for ArithExpr:

## Static Public Member Functions
static ArithExpr | operator/ (ArithExpr a, ArithExpr b)
| Operator overloading for arithmetical division operator (over reals) More...
static ArithExpr | operator/ (ArithExpr a, int b)
| Operator overloading for arithmetical operator More...
static ArithExpr | operator/ (ArithExpr a, double b)
| Operator overloading for arithmetical operator More...
static ArithExpr | operator/ (int a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static ArithExpr | operator/ (double a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static ArithExpr | operator- (ArithExpr a)
| Operator overloading for arithmetical operator More...
static ArithExpr | operator- (ArithExpr a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static ArithExpr | operator- (ArithExpr a, int b)
| Operator overloading for arithmetical operator More...
static ArithExpr | operator- (ArithExpr a, double b)
| Operator overloading for arithmetical operator More...
static ArithExpr | operator- (int a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static ArithExpr | operator- (double a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static ArithExpr | operator+ (ArithExpr a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static ArithExpr | operator+ (ArithExpr a, int b)
| Operator overloading for arithmetical operator More...
static ArithExpr | operator+ (ArithExpr a, double b)
| Operator overloading for arithmetical operator More...
static ArithExpr | operator+ (int a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static ArithExpr | operator+ (double a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static ArithExpr | operator* (ArithExpr a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static ArithExpr | operator* (ArithExpr a, int b)
| Operator overloading for arithmetical operator More...
static ArithExpr | operator* (ArithExpr a, double b)
| Operator overloading for arithmetical operator More...
static ArithExpr | operator* (int a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static ArithExpr | operator* (double a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator<= (ArithExpr a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator<= (ArithExpr a, int b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator<= (ArithExpr a, double b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator<= (int a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator<= (double a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator< (ArithExpr a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator< (ArithExpr a, int b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator< (ArithExpr a, double b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator< (int a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator< (double a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator> (ArithExpr a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator> (ArithExpr a, int b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator> (ArithExpr a, double b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator> (int a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator> (double a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator>= (ArithExpr a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator>= (ArithExpr a, int b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator>= (ArithExpr a, double b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator>= (int a, ArithExpr b)
| Operator overloading for arithmetical operator More...
static BoolExpr | operator>= (double a, ArithExpr b)
| Operator overloading for arithmetical operator 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...

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

## Detailed Description

Arithmetic expressions (int/real)

Definition at line 31 of file ArithExpr.cs.

## Member Function Documentation

## ◆ operator*() [1/5]

static ArithExpr operator* | ( | ArithExpr | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 97 of file ArithExpr.cs.

97{ return a.Context.MkMul(a, b); }

## ◆ operator*() [2/5]

static ArithExpr operator* | ( | ArithExpr | a,
|  | double | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 103 of file ArithExpr.cs.

103{ return a * MkNum(a, b); }

## ◆ operator*() [3/5]

static ArithExpr operator* | ( | ArithExpr | a,
|  | int | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 100 of file ArithExpr.cs.

100{ return a * MkNum(a, b); }

## ◆ operator*() [4/5]

static ArithExpr operator* | ( | double | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 109 of file ArithExpr.cs.

109{ return MkNum(b, a) * b; }

## ◆ operator*() [5/5]

static ArithExpr operator* | ( | int | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 106 of file ArithExpr.cs.

106{ return MkNum(b, a) * b; }

## ◆ operator+() [1/5]

static ArithExpr operator+ | ( | ArithExpr | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 82 of file ArithExpr.cs.

82{ return a.Context.MkAdd(a, b); }

## ◆ operator+() [2/5]

static ArithExpr operator+ | ( | ArithExpr | a,
|  | double | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 88 of file ArithExpr.cs.

88{ return a + MkNum(a, b); }

## ◆ operator+() [3/5]

static ArithExpr operator+ | ( | ArithExpr | a,
|  | int | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 85 of file ArithExpr.cs.

85{ return a + MkNum(a, b); }

## ◆ operator+() [4/5]

static ArithExpr operator+ | ( | double | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 94 of file ArithExpr.cs.

94{ return MkNum(b, a) + b; }

## ◆ operator+() [5/5]

static ArithExpr operator+ | ( | int | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 91 of file ArithExpr.cs.

91{ return MkNum(b, a) + b; }

## ◆ operator-() [1/6]

static ArithExpr operator- | ( | ArithExpr | a | ) |
| inline static

Operator overloading for arithmetical operator

Definition at line 64 of file ArithExpr.cs.

64{ return a.Context.MkUnaryMinus(a); }

## ◆ operator-() [2/6]

static ArithExpr operator- | ( | ArithExpr | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 67 of file ArithExpr.cs.

67{ return a.Context.MkSub(a, b); }

## ◆ operator-() [3/6]

static ArithExpr operator- | ( | ArithExpr | a,
|  | double | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 73 of file ArithExpr.cs.

73{ return a - MkNum(a, b); }

## ◆ operator-() [4/6]

static ArithExpr operator- | ( | ArithExpr | a,
|  | int | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 70 of file ArithExpr.cs.

70{ return a - MkNum(a, b); }

## ◆ operator-() [5/6]

static ArithExpr operator- | ( | double | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 79 of file ArithExpr.cs.

79{ return MkNum(b, a) - b; }

## ◆ operator-() [6/6]

static ArithExpr operator- | ( | int | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 76 of file ArithExpr.cs.

76{ return MkNum(b, a) - b; }

## ◆ operator/() [1/5]

static ArithExpr operator/ | ( | ArithExpr | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical division operator (over reals)

Definition at line 49 of file ArithExpr.cs.

49{ return a.Context.MkDiv(a, b); }

## ◆ operator/() [2/5]

static ArithExpr operator/ | ( | ArithExpr | a,
|  | double | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 55 of file ArithExpr.cs.

55{ return a / MkNum(a, b); }

## ◆ operator/() [3/5]

static ArithExpr operator/ | ( | ArithExpr | a,
|  | int | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 52 of file ArithExpr.cs.

52{ return a / MkNum(a, b); }

## ◆ operator/() [4/5]

static ArithExpr operator/ | ( | double | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 61 of file ArithExpr.cs.

61{ return MkNum(b, a) / b; }

## ◆ operator/() [5/5]

static ArithExpr operator/ | ( | int | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 58 of file ArithExpr.cs.

58{ return MkNum(b, a) / b; }

## ◆ operator<() [1/5]

static BoolExpr operator< | ( | ArithExpr | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 127 of file ArithExpr.cs.

127{ return a.Context.MkLt(a, b); }

## ◆ operator<() [2/5]

static BoolExpr operator< | ( | ArithExpr | a,
|  | double | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 133 of file ArithExpr.cs.

133{ return a < MkNum(a, b); }

## ◆ operator<() [3/5]

static BoolExpr operator< | ( | ArithExpr | a,
|  | int | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 130 of file ArithExpr.cs.

130{ return a < MkNum(a, b); }

## ◆ operator<() [4/5]

static BoolExpr operator< | ( | double | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 139 of file ArithExpr.cs.

139{ return MkNum(b, a) < b; }

## ◆ operator<() [5/5]

static BoolExpr operator< | ( | int | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 136 of file ArithExpr.cs.

136{ return MkNum(b, a) < b; }

## ◆ operator<=() [1/5]

static BoolExpr operator<= | ( | ArithExpr | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 112 of file ArithExpr.cs.

112{ return a.Context.MkLe(a, b); }

## ◆ operator<=() [2/5]

static BoolExpr operator<= | ( | ArithExpr | a,
|  | double | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 118 of file ArithExpr.cs.

118{ return a <= MkNum(a, b); }

## ◆ operator<=() [3/5]

static BoolExpr operator<= | ( | ArithExpr | a,
|  | int | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 115 of file ArithExpr.cs.

115{ return a <= MkNum(a, b); }

## ◆ operator<=() [4/5]

static BoolExpr operator<= | ( | double | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 124 of file ArithExpr.cs.

124{ return MkNum(b, a) <= b; }

## ◆ operator<=() [5/5]

static BoolExpr operator<= | ( | int | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 121 of file ArithExpr.cs.

121{ return MkNum(b, a) <= b; }

## ◆ operator>() [1/5]

static BoolExpr operator> | ( | ArithExpr | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 142 of file ArithExpr.cs.

142{ return a.Context.MkGt(a, b); }

## ◆ operator>() [2/5]

static BoolExpr operator> | ( | ArithExpr | a,
|  | double | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 148 of file ArithExpr.cs.

148{ return a > MkNum(a, b); }

## ◆ operator>() [3/5]

static BoolExpr operator> | ( | ArithExpr | a,
|  | int | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 145 of file ArithExpr.cs.

145{ return a > MkNum(a, b); }

## ◆ operator>() [4/5]

static BoolExpr operator> | ( | double | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 154 of file ArithExpr.cs.

154{ return MkNum(b, a) > b; }

## ◆ operator>() [5/5]

static BoolExpr operator> | ( | int | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 151 of file ArithExpr.cs.

151{ return MkNum(b, a) > b; }

## ◆ operator>=() [1/5]

static BoolExpr operator>= | ( | ArithExpr | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 157 of file ArithExpr.cs.

157{ return a.Context.MkGe(a, b); }

## ◆ operator>=() [2/5]

static BoolExpr operator>= | ( | ArithExpr | a,
|  | double | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 163 of file ArithExpr.cs.

163{ return a >= MkNum(a, b); }

## ◆ operator>=() [3/5]

static BoolExpr operator>= | ( | ArithExpr | a,
|  | int | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 160 of file ArithExpr.cs.

160{ return a >= MkNum(a, b); }

## ◆ operator>=() [4/5]

static BoolExpr operator>= | ( | double | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 169 of file ArithExpr.cs.

169{ return MkNum(b, a) >= b; }

## ◆ operator>=() [5/5]

static BoolExpr operator>= | ( | int | a,
|  | ArithExpr | b
| ) |  |
| inline static

Operator overloading for arithmetical operator

Definition at line 166 of file ArithExpr.cs.

166{ return MkNum(b, a) >= b; }