Static Public Member Functions | |
static long[] | arrayToNative (Z3Object[] a) |
static int | arrayLength (Z3Object[] a) |
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition at line 24 of file Z3Object.java.
|
inlinestatic |
Definition at line 83 of file Z3Object.java.
Referenced by Lambda< R extends Sort >.of(), Quantifier.of(), Context.parOr(), Context.parseSMTLIB2File(), Context.parseSMTLIB2String(), Fixedpoint.query(), Fixedpoint.setPredicateRepresentation(), and Fixedpoint.toString().
|
inlinestatic |
Definition at line 73 of file Z3Object.java.
Referenced by Context.benchmarkToSMTString(), Optimize.Check(), Solver.check(), Context.mkAnd(), Context.mkAtLeast(), Context.mkAtMost(), Context.mkDatatypeSorts(), Context.mkOr(), Context.mkPattern(), Context.mkPBEq(), Context.mkPBGe(), Context.mkPBLe(), Lambda< R extends Sort >.of(), Quantifier.of(), Context.parOr(), Context.parseSMTLIB2File(), Context.parseSMTLIB2String(), Fixedpoint.query(), Fixedpoint.setPredicateRepresentation(), Expr< SeqSort< R > >.substitute(), Expr< SeqSort< R > >.substituteVars(), Fixedpoint.toString(), and Expr< SeqSort< R > >.update().