MCPcopy Create free account
hub / github.com/Z3Prover/z3 / isArray

Method isArray

src/api/java/Expr.java:619–624  ·  view source on GitHub ↗

Indicates whether the term is of an array sort. @throws Z3Exception on error @return a boolean

()

Source from the content-addressed store, hash-verified

617 * @return a boolean
618 **/
619 public boolean isArray()
620 {
621 return (Native.isApp(getContext().nCtx(), getNativeObject()) && Z3_sort_kind
622 .fromInt(Native.getSortKind(getContext().nCtx(),
623 Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_ARRAY_SORT);
624 }
625
626 /**
627 * Indicates whether the term is an array store.

Callers

nothing calls this directly

Calls 7

nCtxMethod · 0.80
getContextMethod · 0.80
getNativeObjectMethod · 0.80
fromIntMethod · 0.80
getSortKindMethod · 0.80
isAppMethod · 0.65
getSortMethod · 0.65

Tested by

no test coverage detected