Package com.microsoft.z3

Class AlgebraicNum

java.lang.Object

com.microsoft.z3.Z3Object

com.microsoft.z3.AST

com.microsoft.z3.Expr<R>

com.microsoft.z3.ArithExpr

com.microsoft.z3.AlgebraicNum

All Implemented Interfaces:

Comparable

public class AlgebraicNum
extends ArithExpr

Algebraic numbers

Method Summary

Modifier and Type	Method	Description
String	toDecimal(int precision)	Returns a string representation in decimal notation.
RatNum	toLower(int precision)	Return a lower bound for the given real algebraic number.
RatNum	toUpper(int precision)	Return a upper bound for a given real algebraic number.

Methods inherited from class com.microsoft.z3.Expr

distillSort, getArgs, getBoolValue, getFuncDecl, getIndex, getNumArgs, getSort, getString, isAdd, isAlgebraicNumber, isAnd, isArithmeticNumeral, isArray, isArrayMap, isAsArray, isBool, isBV, isBVAdd, isBVAND, isBVBitOne, isBVBitZero, isBVCarry, isBVComp, isBVConcat, isBVExtract, isBVMul, isBVNAND, isBVNOR, isBVNOT, isBVNumeral, isBVOR, isBVReduceAND, isBVReduceOR, isBVRepeat, isBVRotateLeft, isBVRotateLeftExtended, isBVRotateRight, isBVRotateRightExtended, isBVSDiv, isBVSGE, isBVSGT, isBVShiftLeft, isBVShiftRightArithmetic, isBVShiftRightLogical, isBVSignExtension, isBVSLE, isBVSLT, isBVSMod, isBVSRem, isBVSub, isBVToInt, isBVUDiv, isBVUGE, isBVUGT, isBVULE, isBVULT, isBVUMinus, isBVURem, isBVXNOR, isBVXOR, isBVXOR3, isBVZeroExtension, isConcat, isConst, isConstantArray, isDefaultArray, isDistinct, isDiv, isEmptyRelation, isEq, isFalse, isFiniteDomain, isFiniteDomainLT, isGE, isGT, isIDiv, isIff, isImplies, isInt, isIntNum, isIntToBV, isIntToReal, isIsEmptyRelation, isITE, isLabel, isLabelLit, isLE, isLT, isModulus, isMul, isNot, isNumeral, isOEQ, isOr, isProofAndElimination, isProofApplyDef, isProofAsserted, isProofCommutativity, isProofDefAxiom, isProofDefIntro, isProofDER, isProofDistributivity, isProofElimUnusedVars, isProofGoal, isProofHypothesis, isProofIFFFalse, isProofIFFOEQ, isProofIFFTrue, isProofLemma, isProofModusPonens, isProofModusPonensOEQ, isProofMonotonicity, isProofNNFNeg, isProofNNFPos, isProofOrElimination, isProofPullQuant, isProofPushQuant, isProofQuantInst, isProofQuantIntro, isProofReflexivity, isProofRewrite, isProofRewriteStar, isProofSkolemize, isProofSymmetry, isProofTheoryLemma, isProofTransitivity, isProofTransitivityStar, isProofTrue, isProofUnitResolution, isRatNum, isReal, isRealIsInt, isRealToInt, isRelation, isRelationalJoin, isRelationClone, isRelationComplement, isRelationFilter, isRelationNegationFilter, isRelationProject, isRelationRename, isRelationSelect, isRelationStore, isRelationUnion, isRelationWiden, isRemainder, isSelect, isSetComplement, isSetDifference, isSetIntersect, isSetSubset, isSetUnion, isStore, isString, isSub, isTrue, isUMinus, isWellSorted, isXor, simplify, simplify, substitute, substitute, substituteVars, toString, translate, update

Methods inherited from class com.microsoft.z3.AST

compareTo, equals, getASTKind, getId, getSExpr, hashCode, isApp, isExpr, isFuncDecl, isQuantifier, isSort, isVar

Methods inherited from class com.microsoft.z3.Z3Object

arrayLength, arrayToNative

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Method Details

toUpper

public RatNum toUpper(int precision)

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

Parameters:

precision - the precision of the result

Returns:

A numeral Expr of sort Real

Throws:

Z3Exception - on error

See Also:

• Expr.isAlgebraicNumber()

toLower

public RatNum toLower(int precision)

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

Parameters:

precision - precision

Returns:

A numeral Expr of sort Real

Throws:

Z3Exception - on error

See Also:

• Expr.isAlgebraicNumber()

toDecimal

public String toDecimal(int precision)

Returns a string representation in decimal notation. Remarks: The result has at most precision decimal places.

Parameters:

precision - precision

Returns:

String

Throws:

Z3Exception - on error