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 Assume command pushes some proposition onto the assumption stack of the session. The
009 * proposition is assumed to be true, and is not proved. This command will not block.
010 */
011public class CmdAssume implements Cmd {
012  public final String proposition;
013
014  public CmdAssume(String proposition) {
015    this.proposition = proposition.trim();
016    SimpUtil.assert_well_formed(proposition);
017  }
018
019  /** For documentation, read the class overview. */
020  @Override
021  public void apply(final @GuardedBy("<self>") Session s) {
022
023    synchronized (s) {
024      // send out the (BG_PUSH proposition)
025      s.sendLine("(BG_PUSH " + proposition + ")");
026      if (Session.dkconfig_verbose_progress > 1) {
027        System.out.print("<");
028        System.out.flush();
029      }
030
031      // there is no output from Simplify
032    }
033  }
034
035  @SideEffectFree
036  @Override
037  public String toString(@GuardSatisfied CmdAssume this) {
038    return "CmdAssume: " + proposition;
039  }
040}