001package daikon.simplify;
002
003import org.checkerframework.checker.lock.qual.GuardSatisfied;
004import org.checkerframework.checker.lock.qual.GuardedBy;
005import org.checkerframework.dataflow.qual.SideEffectFree;
006
007/**
008 * An UndoAssume command removes an assumption from the assumption stack of the given session. The
009 * command will not block.
010 */
011public class CmdUndoAssume implements Cmd {
012  public static CmdUndoAssume single = new CmdUndoAssume();
013
014  /** For documentation, read the class overview. */
015  @Override
016  public void apply(final @GuardedBy("<self>") Session s) {
017
018    synchronized (s) {
019      // send out the (BG_POP)
020      s.sendLine("(BG_POP)");
021      if (Session.dkconfig_verbose_progress > 1) {
022        System.out.print(">");
023        System.out.flush();
024      }
025
026      // there is no output from Simplify
027    }
028  }
029
030  @SideEffectFree
031  @Override
032  public String toString(@GuardSatisfied CmdUndoAssume this) {
033    return "CmdUndoAssume";
034  }
035}