001    package daikon.inv;
002    
003    import daikon.*;
004    
005    /**
006     * A class used for holding a DiscardCode and a string
007     * that contains more detailed information about why an Invariant
008     * was discarded, as well as the classname and what would be returned
009     * by the Invariant's format() method.
010     */
011    public final class DiscardInfo {
012    
013      /**
014       * The DiscardCode describing this DiscardInfo.  It should never be null;
015       * if an invariant isn't being discarded, use null as its DiscardInfo.
016       */
017      private DiscardCode discardCode;
018    
019      /** The detailed reason for discard */
020      private String discardString;
021    
022      /**
023       * The String that would have resulted from calling format() on the
024       * Invariant being discarded.  This does not have to be maintained
025       * if the Invariant isn't discarded.
026       */
027      private String discardFormat;
028    
029      /** Invariant for which the DiscardInfo applies **/
030      public Invariant inv;
031    
032      // Rarely used, so no need to precompute. -MDE
033      // /**
034      //  * The className of the Invariant being discarded
035      //  */
036      // private String className;
037    
038      // public DiscardInfo(String className, String discardFormat, DiscardCode discardCode, String discardString) {
039      //   this.discardCode = discardCode;
040      //   this.discardString = discardString;
041      //   this.discardFormat = discardFormat;
042      //   this.className = className;
043      // }
044    
045      public DiscardInfo(Invariant inv, DiscardCode discardCode, String discardString) {
046        assert inv.ppt != null;
047        // this(inv.getClass().getName(), inv.format(), discardCode, discardString);
048        this.discardCode = discardCode;
049        this.discardString = discardString;
050        this.discardFormat = inv.format();
051        // this.className = inv.getClass().getName();
052        this.inv = inv;
053        inv.log (discardString);
054      }
055    
056      public String discardFormat() {
057        return this.discardFormat;
058      }
059    
060      public DiscardCode discardCode() {
061        return this.discardCode;
062      }
063    
064      public String discardString() {
065        return this.discardString;
066      }
067    
068      public String className() {
069        return this.inv.getClass().getName();
070      }
071    
072      public String format() {
073        return (discardFormat + Global.lineSep
074                + discardCode + Global.lineSep
075                + discardString);
076      }
077    
078      /**
079       * Adds the specified string as an additional reason
080       */
081      public void add_implied (String reason) {
082        discardString += " and " + reason;
083      }
084    
085      /**
086       * Adds an equality string to the discardString for each variable in
087       * in vis which is different from the leader
088       */
089      public void add_implied_vis (VarInfo[] vis) {
090        for (int i = 0; i < vis.length; i++) {
091          if (inv.ppt.var_infos[i] != vis[i])
092            discardString += " and " + inv.ppt.var_infos[i] + "==" + vis[i];
093        }
094      }
095    
096    
097    }