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

Algebraic numbers More...

+ Inheritance diagram for AlgebraicNum:

Public Member Functions

RatNum ToUpper (uint precision)
 Return a upper bound for a given real algebraic number. The interval isolating the number is smaller than 1/10^precision .

See Also
Expr.IsAlgebraicNumber

 
RatNum ToLower (uint precision)
 Return a lower bound for the given real algebraic number. The interval isolating the number is smaller than 1/10^precision .

See Also
Expr.IsAlgebraicNumber

 
string ToDecimal (uint precision)
 Returns a string representation in decimal notation.
 

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 ArithExpr
 ArithExpr (Context ctx)
 Constructor for ArithExpr
 
- 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.
 

Detailed Description

Algebraic numbers

Definition at line 295 of file Numeral.cs.

Member Function Documentation

string ToDecimal ( uint  precision)
inline

Returns a string representation in decimal notation.

The result has at most precision decimal places.

Definition at line 329 of file Numeral.cs.

{
Contract.Ensures(Contract.Result<string>() != null);
return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision);
}
RatNum ToLower ( uint  precision)
inline

Return a lower bound for the given real algebraic number. The interval isolating the number is smaller than 1/10^precision .

See Also
Expr.IsAlgebraicNumber

Parameters
precision
Returns
A numeral Expr of sort Real

Definition at line 318 of file Numeral.cs.

{
Contract.Ensures(Contract.Result<RatNum>() != null);
return new RatNum(Context, Native.Z3_get_algebraic_number_lower(Context.nCtx, NativeObject, precision));
}
RatNum ToUpper ( uint  precision)
inline

Return a upper bound for a given real algebraic number. The interval isolating the number is smaller than 1/10^precision .

See Also
Expr.IsAlgebraicNumber

Parameters
precisionthe precision of the result
Returns
A numeral Expr of sort Real

Definition at line 304 of file Numeral.cs.

{
Contract.Ensures(Contract.Result<RatNum>() != null);
return new RatNum(Context, Native.Z3_get_algebraic_number_upper(Context.nCtx, NativeObject, precision));
}