AlgebraicNum Class Reference

Inheritance diagram for AlgebraicNum:

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

Additional Inherited Members
Protected Member Functions inherited from Expr< R >
	Expr (Context ctx, long obj)

Detailed Description

Algebraic numbers

Definition at line 23 of file AlgebraicNum.java.

Member Function Documentation

toDecimal()

String toDecimal ( int  precision )

inline

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

precision 

decimal places.

Parameters

precision

precision

Returns

String

Exceptions

Z3Exception

on error

Definition at line 66 of file AlgebraicNum.java.

    {
 
        return Native.getNumeralDecimalString(getContext().nCtx(), getNativeObject(),
                precision);
    }

toLower()

RatNum toLower ( int  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

precision

Returns

A numeral Expr of sort Real

Exceptions

Z3Exception

on error

Definition at line 52 of file AlgebraicNum.java.

    {
 
        return new RatNum(getContext(), Native.getAlgebraicNumberLower(getContext()
                .nCtx(), getNativeObject(), precision));
    }

toUpper()

RatNum toUpper ( int  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

precision

the precision of the result

Returns

A numeral Expr of sort Real

Exceptions

Z3Exception

on error

Definition at line 35 of file AlgebraicNum.java.

    {
 
        return new RatNum(getContext(), Native.getAlgebraicNumberUpper(getContext()
                .nCtx(), getNativeObject(), precision));
    }