001package daikon.inv;
002
003import java.util.ArrayList;
004import java.util.List;
005import java.util.StringTokenizer;
006import org.checkerframework.checker.nullness.qual.Nullable;
007import org.checkerframework.dataflow.qual.Pure;
008
009/**
010 * Container class for holding all info needed to describe an Invariant. If any field is null, that
011 * field is a wildcard, so one instance of InvariantInfo may describe multiple Invariants in that
012 * way.
013 */
014public class InvariantInfo {
015
016  private String ppt;
017
018  // vars is maintained as "var1,var2,.." sorted in ascending lexicographical order
019  /** If null, treated as a wildcard. */
020  private final @Nullable String vars;
021
022  /** If null, treated as a wildcard. */
023  private @Nullable String className;
024
025  //   private InvariantInfo() {
026  //     // Make the default constructor private, this should never be called
027  //   }
028
029  /* // It's ok if vars isn't given in sorted order, we'll sort it here */
030  public InvariantInfo(String ppt, @Nullable String vars, @Nullable String className) {
031    this.ppt = ppt;
032    this.className = className;
033    /* if (vars != null) {
034    // Sort the vars into ascending order
035    StringTokenizer st = new StringTokenizer(vars, ",");
036    ArrayList temp = new ArrayList();
037    while (st.hasMoreTokens()) {
038      temp.add(st.nextToken());
039    }
040    Collections.sort(temp);
041    String vars_result = "";
042    for (int i = 0; i < temp.size(); i++) {
043      vars_result += temp.get(i) + ",";
044    }
045    this.vars = vars_result;
046    }*/
047    this.vars = vars;
048  }
049
050  public String ppt() {
051    return this.ppt;
052  }
053
054  @Pure
055  public @Nullable String className() {
056    return this.className;
057  }
058
059  public @Nullable String vars() {
060    return this.vars;
061  }
062
063  /**
064   * Returns a list of Strings of all permutations of the vars, or null if vars == null.
065   *
066   * <p>e.g., if vars is "var1,var2,var3", this method will return ["var1,var2,var3",
067   * "var1,var3,var2", "var2,var1,var3"... etc.]
068   *
069   * @return a list of Strings of all permutations of the vars, or null if vars == null
070   */
071  public @Nullable List<String> var_permutations() {
072    if (vars == null) {
073      return null;
074    }
075
076    // We know there can be at most 3 vars so it's not worth writing
077    // a complicated routine that generates all permutations
078    StringTokenizer st = new StringTokenizer(vars, ",");
079    assert st.countTokens() <= 3;
080    ArrayList<String> result = new ArrayList<>(3);
081    if (st.countTokens() == 1) {
082      result.add(vars);
083      return result;
084    } else if (st.countTokens() == 2) {
085      result.add(vars);
086      String var1 = st.nextToken();
087      String var2 = st.nextToken();
088      result.add(var2 + "," + var1);
089      return result;
090    } else {
091      // st.countTokens() == 3
092      String var1 = st.nextToken();
093      String var2 = st.nextToken();
094      String var3 = st.nextToken();
095      result.add(var1 + "," + var2 + "," + var3);
096      result.add(var1 + "," + var3 + "," + var2);
097      result.add(var2 + "," + var1 + "," + var3);
098      result.add(var2 + "," + var3 + "," + var1);
099      result.add(var3 + "," + var1 + "," + var2);
100      result.add(var3 + "," + var2 + "," + var1);
101      return result;
102    }
103  }
104}