IntNum Class Reference

Inheritance diagram for IntNum:

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

Additional Inherited Members
Protected Member Functions inherited from IntExpr
	IntExpr (Context ctx) throws Z3Exception
Protected Member Functions inherited from ArithExpr
	ArithExpr (Context ctx)
Protected Member Functions inherited from Expr
	Expr (Context ctx)
	Expr (Context ctx, long obj) throws Z3Exception
Protected Member Functions inherited from Z3Object
void	finalize () throws Z3Exception

Detailed Description

Integer Numerals

Definition at line 25 of file IntNum.java.

Member Function Documentation

BigInteger getBigInteger ( ) throws Z3Exception

inline

Retrieve the BigInteger value.

Definition at line 58 of file IntNum.java.

    {
        return new BigInteger(this.toString());
    }

int getInt ( ) throws Z3Exception

inline

Retrieve the int value.

Definition at line 36 of file IntNum.java.

    {
        Native.IntPtr res = new Native.IntPtr();
        if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true)
            throw new Z3Exception("Numeral is not an int");
        return res.value;
    }

long getInt64 ( ) throws Z3Exception

inline

Retrieve the 64-bit int value.

Definition at line 47 of file IntNum.java.

    {
        Native.LongPtr res = new Native.LongPtr();
        if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
            throw new Z3Exception("Numeral is not an int64");
        return res.value;
    }

String toString ( )

inline

Returns a string representation of the numeral.

Definition at line 66 of file IntNum.java.

Referenced by RatNum.getBigIntDenominator(), IntNum.getBigInteger(), and RatNum.getBigIntNumerator().

    {
        try
        {
            return Native.getNumeralString(getContext().nCtx(), getNativeObject());
        } catch (Z3Exception e)
        {
            return "Z3Exception: " + e.getMessage();
        }
    }