Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Public Member Functions | Properties
BitVecNum Class Reference

Bit-vector numerals More...

+ Inheritance diagram for BitVecNum:

Public Member Functions

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

Properties

UInt64 UInt64 [get]
 Retrieve the 64-bit unsigned integer value.
 
int Int [get]
 Retrieve the int value.
 
Int64 Int64 [get]
 Retrieve the 64-bit int value.
 
uint UInt [get]
 Retrieve the int value.
 
BigInteger BigInteger [get]
 Retrieve the BigInteger value.
 
- Properties inherited from BitVecExpr
uint SortSize [get]
 The size of the sort of a bit-vector term.
 
- 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.
 
- Properties inherited from AST
uint Id [get]
 A unique identifier for the AST (unique among all ASTs).
 
Z3_ast_kind ASTKind [get]
 The kind of the AST.
 
bool IsExpr [get]
 Indicates whether the AST is an Expr
 
bool IsVar [get]
 Indicates whether the AST is a BoundVariable
 
bool IsQuantifier [get]
 Indicates whether the AST is a Quantifier
 
bool IsSort [get]
 Indicates whether the AST is a Sort
 
bool IsFuncDecl [get]
 Indicates whether the AST is a FunctionDeclaration
 

Additional Inherited Members

- 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.
 
- Protected Member Functions inherited from BitVecExpr
 BitVecExpr (Context ctx)
 Constructor for BitVecExpr
 

Detailed Description

Bit-vector numerals

Definition at line 207 of file Numeral.cs.

Member Function Documentation

override string ToString ( )
inline

Returns a string representation of the numeral.

Definition at line 281 of file Numeral.cs.

{
return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
}

Property Documentation

BigInteger BigInteger
get

Retrieve the BigInteger value.

Definition at line 270 of file Numeral.cs.

int Int
get

Retrieve the int value.

Definition at line 227 of file Numeral.cs.

Int64 Int64
get

Retrieve the 64-bit int value.

Definition at line 241 of file Numeral.cs.

uint UInt
get

Retrieve the int value.

Definition at line 255 of file Numeral.cs.

UInt64 UInt64
get

Retrieve the 64-bit unsigned integer value.

Definition at line 213 of file Numeral.cs.