|
Z3
|
|
|
Z3
|
|
Boolean expressions More...
Inheritance diagram for BoolExpr:Static Public Member Functions | |
| static BoolExpr | operator| (BoolExpr a, BoolExpr b) |
| Disjunction of Boolean expressions More... | |
| static BoolExpr | operator& (BoolExpr a, BoolExpr b) |
| Conjunction of Boolean expressions More... | |
| static BoolExpr | operator^ (BoolExpr a, BoolExpr b) |
| Xor of Boolean expressions More... | |
| static BoolExpr | operator! (BoolExpr a) |
| Negation 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... | |
| 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... | |
| 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... | |
Boolean expressions
Definition at line 31 of file BoolExpr.cs.
Conjunction of Boolean expressions
Definition at line 43 of file BoolExpr.cs.
Xor of Boolean expressions
Definition at line 46 of file BoolExpr.cs.
Disjunction of Boolean expressions
Definition at line 40 of file BoolExpr.cs.
1.9.1
