FiniteDomainNum< R > Class Template Reference

Inheritance diagram for FiniteDomainNum< R >:

Public Member Functions
int	getInt ()
long	getInt64 ()
BigInteger	getBigInteger ()
String	toString ()
Public Member Functions inherited from Expr< FiniteDomainSort< 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< FiniteDomainSort< R > >
	Expr (Context ctx, long obj)

Detailed Description

Finite-domain Numerals

Definition at line 25 of file FiniteDomainNum.java.

Member Function Documentation

getBigInteger()

BigInteger getBigInteger ( )

inline

Retrieve the BigInteger value.

Definition at line 60 of file FiniteDomainNum.java.

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

getInt()

int getInt ( )

inline

Retrieve the int value.

Definition at line 36 of file FiniteDomainNum.java.

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

getInt64()

long getInt64 ( )

inline

Retrieve the 64-bit int value.

Definition at line 48 of file FiniteDomainNum.java.

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

toString()

String toString ( )

inline

Returns a string representation of the numeral.

Definition at line 69 of file FiniteDomainNum.java.

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

Referenced by FiniteDomainNum< R >.getBigInteger().