Commit a3858ef6 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Move CVC3's fixed point literal generator to use a StringBuilder. 

CVC3's fixed point literal generator used a ton of string appending to do its
work in a loop.  This could grow expensive easily, thus move to a StringBuilder.
parent d5bbdd7f

src/main/java/ca/mcscert/jtet/cvc3generator/CVC3ExpressionGenerator.java

+10 −7
Original line number Diff line number Diff line
@@ -205,17 +205,20 @@ final public class CVC3ExpressionGenerator implements ExpressionGenerator { 
            decimal = decimal.multiply(BigDecimal.valueOf(1 << type.fractionPart()));

            BigInteger intOut = decimal.toBigIntegerExact();



            //This gets the two's compliment representation.  Ugly for loop, but best I could find.

            String bits = "";

            for (int i = intOut.bitLength() - 1; i >= 0; --i) {

                bits += (intOut.testBit(i)) ? '1' : '0';

            }

            final StringBuilder output = new StringBuilder(type.digits());

            output.append("0bin");



            if (intOut.signum() < 0) {

                return "0bin" + StringUtils.repeat('1', type.digits() - bits.length()) + bits;

                output.append(StringUtils.repeat('1', type.digits() - intOut.bitLength()));

            } else {

                return "0bin" + StringUtils.repeat('0', type.digits() - bits.length()) + bits;

                output.append(StringUtils.repeat('0', type.digits() - intOut.bitLength()));

            }



            //This gets the two's compliment representation.  Ugly for loop, but best I could find.

            for (int i = intOut.bitLength() - 1; i >= 0; --i) {

                output.append((intOut.testBit(i)) ? '1' : '0');

            }

            return output.toString();

        } else {

            throw new IllegalArgumentException("Can't cast literal to that type!");

        }