class CommunityMatchExprToBDD implements CommunityMatchExprVisitor<BDD, Arg> {

  @Override
  public BDD visitCommunityNot(CommunityNot communityNot, Arg arg) {
    BDD toBeNegated = communityNot.getExpr().accept(this, arg);
    // to negate a predicate on a single community, we diff it from a predicate representing
    // any community. simply negating toBeNegated is not sufficient because it would allow a model
    // where all atomic predicates are false, which doesn't correspond to any concrete communities.
    return arg.getBDDRoute().anyCommunity().diffWith(toBeNegated);
  }

}