Z3Object Class Reference

Inheritance diagram for Z3Object:

Static Public Member Functions
static long[]	arrayToNative (Z3Object[] a)
static int	arrayLength (Z3Object[] a)

Detailed Description

Internal base class for interfacing with native Z3 objects. Should not be used externally.

Definition at line 24 of file Z3Object.java.

Member Function Documentation

arrayLength()

static int arrayLength ( Z3Object[]  a )

inlinestatic

Definition at line 83 of file Z3Object.java.

    {
        return (a == null) ? 0 : a.length;
    }

Referenced by Context.mkMap(), Context.mkPropagateFunction(), Quantifier.of(), Lambda< R extends Sort >.of(), Context.parOr(), Context.parseSMTLIB2File(), Context.parseSMTLIB2String(), Fixedpoint.query(), Fixedpoint.setPredicateRepresentation(), and Fixedpoint.toString().

arrayToNative()

static long [] arrayToNative ( Z3Object[]  a )

inlinestatic

Definition at line 73 of file Z3Object.java.

    {
        if (a == null)
            return null;
        long[] an = new long[a.length];
        for (int i = 0; i < a.length; i++)
            an[i] = (a[i] == null) ? 0 : a[i].getNativeObject();
        return an;
    }

Referenced by Context.AddRecDef(), Context.benchmarkToSMTString(), Optimize.Check(), Solver.check(), UserPropagatorBase.consequence(), Context.mkAdd(), Context.mkAnd(), Context.mkAtLeast(), Context.mkAtMost(), Context.mkConcat(), Context.mkDatatypeSorts(), Context.mkDistinct(), Context.mkIntersect(), Context.mkMap(), Context.mkMul(), Context.mkOr(), Context.mkPattern(), Context.mkPBEq(), Context.mkPBGe(), Context.mkPBLe(), Context.mkPropagateFunction(), Context.mkSelect(), Context.mkSetIntersection(), Context.mkSetUnion(), Context.mkStore(), Context.mkSub(), Context.mkUnion(), Quantifier.of(), Lambda< R extends Sort >.of(), Context.parOr(), Context.parseSMTLIB2File(), Context.parseSMTLIB2String(), Fixedpoint.query(), Fixedpoint.setPredicateRepresentation(), Expr< R extends Sort >.substitute(), Expr< R extends Sort >.substituteVars(), Fixedpoint.toString(), and Expr< R extends Sort >.update().