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

Method isDistinct

src/api/java/Expr.java:357–360  ·  view source on GitHub ↗

Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct). @throws Z3Exception on error @return a boolean

()

Source from the content-addressed store, hash-verified

355 * @return a boolean
356 **/
357 public boolean isDistinct()
358 {
359 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DISTINCT;
360 }
361
362 /**
363 * Indicates whether the term is a ternary if-then-else term

Callers

nothing calls this directly

Calls 3

getFuncDeclMethod · 0.95
getDeclKindMethod · 0.80
isAppMethod · 0.65

Tested by

no test coverage detected