Method notImplies

smt/expr.cpp:1716–1720

}

expr expr::notImplies(const expr &rhs) const {
  if (eq(rhs))
    return false;
  return *this && !rhs;
}

expr expr::ule(const expr &rhs) const {
  if (eq(rhs) || isZero() || rhs.isAllOnes())