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}