package org.batfish.bddreachability.transition;

import static com.google.common.base.Preconditions.checkArgument;

import java.util.HashSet;
import java.util.Set;
import net.sf.javabdd.BDD;

/** A transition that erases a variable and then constrains it to have a new value. */
public final class EraseAndSet implements Transition {
  private final BDD _eraseVars;
  private final BDD _setValue;

  private static void vars(BDD bdd, Set<Integer> varSet) {
    if (bdd.isZero() || bdd.isOne()) {
      return;
    }
    varSet.add(bdd.var());
    vars(bdd.high(), varSet);
    vars(bdd.low(), varSet);
  }

  private static Set<Integer> vars(BDD bdd) {
    Set<Integer> varSet = new HashSet<>();
    vars(bdd, varSet);
    return varSet;
  }

  EraseAndSet(BDD eraseVars, BDD setValue) {
    Set<Integer> vars = vars(eraseVars);
    checkArgument(!vars.isEmpty(), "No variables to erase");

    checkArgument(!setValue.isOne(), "Value is one (always true). Use Identity instead");

    /* Require that the erased variables include the set variables. We consider it an error to
     * set a variable that wasn't erased. If we want to set a variable that wasn't erased, use a
     * different transition class.
     */
    checkArgument(vars.containsAll(vars(setValue)));

    _eraseVars = eraseVars;
    _setValue = setValue;
  }

  @Override
  public BDD transitForward(BDD bdd) {
    return bdd.exist(_eraseVars).and(_setValue);
  }

  @Override
  public BDD transitBackward(BDD bdd) {
    return bdd.and(_setValue).exist(_eraseVars);
  }
}

@@ -113,56 +113,8 @@
 t;%0A%0A
-import java.util.HashSet;%0Aimport java.util.Set;%0A
 impo
@@ -349,469 +349,111 @@
 %0A%0A  
-private static void vars(BDD bdd, Set%3CInteger%3E varSet) %7B%0A    if (bdd.isZero() %7C%7C bdd.isOne()) %7B%0A      return;%0A    %7D%0A    varSet.add(bdd.var());%0A    vars(bdd.high(), varSet);%0A    vars(bdd.low(), varSet);%0A  %7D%0A%0A  private static Set%3CInteger%3E vars(BDD bdd) %7B%0A    Set%3CInteger%3E varSet = new HashSet%3C%3E();%0A    vars(bdd, varSet);%0A    return varSet;%0A  %7D%0A%0A  EraseAndSet(BDD eraseVars, BDD setValue) %7B%0A    Set%3CInteger%3E vars = vars(eraseVars);%0A    checkArgument(!vars.isEmpty(
+EraseAndSet(BDD eraseVars, BDD setValue) %7B%0A    checkArgument((!eraseVars.isOne() && !eraseVars.isZero()
 ), %22
@@ -826,40 +826,83 @@
 ent(
-vars.containsAll(vars(setValue))
+setValue.exist(eraseVars).isOne(), %22Erasing the value should result in one%22
 );%0A%0A

simplify (#3926)