Z3 |

Static Public Member Functions
Z3Object Class Referenceabstract
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 | ) |
| inline static

Definition at line 83 of file Z3Object.java.

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

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 | ) |
| inline static

Definition at line 73 of file Z3Object.java.

74 {
75 if (a == null)
76 return null;
77 long[] an = new long[a.length];
78 for (int i = 0; i < a.length; i++)
79 an[i] = (a[i] == null) ? 0 : a[i].getNativeObject();
80 return an;
81 }

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().