Package com.microsoft.z3

Class FiniteDomainNum<R>

java.lang.Object

com.microsoft.z3.Z3Object

com.microsoft.z3.AST

com.microsoft.z3.Expr<FiniteDomainSort<R>>

com.microsoft.z3.FiniteDomainExpr<R>

com.microsoft.z3.FiniteDomainNum<R>

All Implemented Interfaces:

Comparable<AST>

public class FiniteDomainNum<R>
extends FiniteDomainExpr<R>

Finite-domain Numerals

Method Summary

Modifier and Type	Method	Description
BigInteger	getBigInteger()	Retrieve the BigInteger value.
int	getInt()	Retrieve the int value.
long	getInt64()	Retrieve the 64-bit int value.
String	toString()	Returns a string representation of the numeral.

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, 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

getInt

public int getInt()

Retrieve the int value.

getInt64

public long getInt64()

Retrieve the 64-bit int value.

getBigInteger

public BigInteger getBigInteger()

Retrieve the BigInteger value.

toString

public String toString()

Returns a string representation of the numeral.

Overrides:

toString in class Expr<FiniteDomainSort<R>>