class CommunitySetMatchExprToBDD implements CommunitySetMatchExprVisitor<BDD, CommunitySetMatchExprToBDD.Arg> {

  @Override
  public BDD visitHasCommunity(HasCommunity hasCommunity, Arg arg) {
    BDD matchExprBDD = hasCommunity.getExpr().accept(new CommunityMatchExprToBDD(), arg);
    /**
     * the above BDD applies to a single community so we can't treat it as a BDD for a community
     * set, or else its constraints could be satisfied by multiple communities in the set that each
     * satisfy some of the constraints. therefore, we instead return the largest disjunction of
     * atomic predicates that satisfies the BDD. hence any community set that satisfies this
     * disjunction must contain at least one community that satisfies our original BDD.
     */
    BDD[] aps = arg.getBDDRoute().getCommunityAtomicPredicates();
    /**
     * first figure out which atomic predicates satisfy matchExprBDD. when considering each atomic
     * predicate, we use the exactlyOneAP helper function to include the fact that all other atomic
     * predicates will be false, which must be the case since atomic predicates are disjoint.
     * otherwise, we would not be able to show that ap1 satisfies the community constraint (ap1 /\
     * !ap2), for example.
     */
    IntStream disjuncts =
        IntStream.range(0, aps.length).filter(i -> !exactlyOneAP(aps, i).diffSat(matchExprBDD));
    /**
     * now return a disjunction of all of the satisfying atomic predicates. here we do NOT use the
     * exactlyOneAP function, because we are returning a BDD for a community set, which can satisfy
     * multiple atomic predicates due to multiple elements of the set.
     */
    return BDDRoute.factory.orAll(disjuncts.mapToObj(i -> aps[i]).collect(Collectors.toList()));
  }

}