001package daikon.simplify;
002
003/** Utility functions for the simplify package. */
004public class SimpUtil {
005  private SimpUtil() {
006    throw new Error("do not instantiate");
007  }
008
009  public static void assert_well_formed(String s) {
010    boolean assert_enabled = false;
011    assert (assert_enabled = true);
012    if (!assert_enabled) {
013      return;
014    }
015
016    // Unfortunately, most of the tests here aren't sensible if the
017    // string can contain quoted strings (like |))|). To do this
018    // right, the paren counter would also have to be smarter about
019    // details like the rules for | delimiting strings, and how it can
020    // be escaped.
021
022    assert s != null;
023    // XXX not with strings
024    //     if (s.indexOf("((") != -1)
025    //       throw new Error("'((' may not appear, '" + s + "'");
026    assert s.length() >= 4 : "too short, '" + s + "'";
027    if (s.charAt(0) != '(') {
028      throw new Error("starts with lparen, '" + s + "'");
029    }
030    if (s.charAt(s.length() - 1) != ')') {
031      throw new Error("ends with rparen, '" + s + "'");
032    }
033
034    @SuppressWarnings("UnusedVariable")
035    int paren = 0;
036    char[] cs = s.toCharArray();
037    for (int i = 0; i < cs.length; i++) {
038      char c = cs[i];
039      if (c == '(') {
040        paren++;
041      } else if (c == ')') {
042        // XXX not with strings
043        //         if (paren <= 0)
044        //           assert paren > 0 : // "too deep at char " + i + " in '" + s + "'";
045        paren--;
046        // This check is only sensible for some callers; it needs a flag.
047        //         if (paren == 0 && i < cs.length -1)
048        //           throw new Error("multiple SEXPs in " + s);
049      }
050    }
051    // XXX not with strings
052    //     if (paren != 0)
053    //       assert paren == 0 : "unbalanced parens in '" + s + "'";
054  }
055
056  /**
057   * Represent a Java long integer as an uninterpreted function applied to 6 moderately sized
058   * integers, to work around Simplify's numeric limitations. The first integer is a sign, and the
059   * rest are 13-bit (base 8192) limbs in order from most to least significant.
060   */
061  public static String formatInteger(long i) {
062    int sign;
063    int[] limbs = new int[5]; // limbs[0] is most significant
064    if (i == 0) {
065      sign = limbs[0] = limbs[1] = limbs[2] = limbs[3] = limbs[4] = 0;
066    } else if (i == Long.MIN_VALUE) {
067      sign = -1;
068      limbs[0] = 2048;
069      limbs[1] = limbs[2] = limbs[3] = limbs[4] = 0;
070    } else {
071      sign = 1;
072      if (i < 0) {
073        sign = -1;
074        i = -i;
075      }
076      for (int j = 4; j >= 0; j--) {
077        limbs[j] = (int) (i % 8192);
078        i /= 8192;
079      }
080    }
081    return "(|long-int| "
082        + sign
083        + " "
084        + limbs[0]
085        + " "
086        + limbs[1]
087        + " "
088        + limbs[2]
089        + " "
090        + limbs[3]
091        + " "
092        + limbs[4]
093        + ")";
094  }
095}