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(), 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.benchmarkToSMTString(), Optimize.Check(), Solver.check(), 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.mkSetIntersection(), Context.mkSetUnion(), 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().