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

Method isRelation

src/api/java/Expr.java:1894–1900  ·  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

1892 * @return a boolean
1893 **/
1894 public boolean isRelation()
1895 {
1896 return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
1897 .getSortKind(getContext().nCtx(),
1898 Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_RELATION_SORT
1899 .toInt());
1900 }
1901
1902 /**
1903 * Indicates whether the term is an relation store

Callers

nothing calls this directly

Calls 7

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

Tested by

no test coverage detected