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

Method isImplies

src/api/java/Expr.java:428–431  ·  view source on GitHub ↗

Indicates whether the term is an implication @throws Z3Exception on error @return a boolean

()

Source from the content-addressed store, hash-verified

426 * @return a boolean
427 **/
428 public boolean isImplies()
429 {
430 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IMPLIES;
431 }
432
433 /**
434 * Indicates whether the term is of integer sort.

Callers

nothing calls this directly

Calls 3

getFuncDeclMethod · 0.95
getDeclKindMethod · 0.80
isAppMethod · 0.65

Tested by

no test coverage detected