Start work on a SAL Code Generator.

/*

 * Copyright (C) 2014 Matthew Dawson <matthew@mjdsystems.ca>

 *

 * Redistribution and use in source and binary forms, with or without

 * modification, are permitted provided that the following conditions are

 * met:

 *

 *     * Redistributions of source code must retain the above copyright

 *       notice, this list of conditions and the following disclaimer.

 *     * Redistributions in binary form must reproduce the above copyright

 *       notice, this list of conditions and the following disclaimer in

 *       the documentation and/or other materials provided with the distribution

 *     * Neither the name of the McMaster Centre for Software Certification nor the names

 *       of its contributors may be used to endorse or promote products derived

 *       from this software without specific prior written permission.

 *

 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"

 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE

 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE

 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE

 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR

 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF

 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS

 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN

 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)

 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE

 * POSSIBILITY OF SUCH DAMAGE.

 */

package ca.mcscert.jtet.expression;

/**

 * @author Matthew Dawson <matthew@mjdsystems.ca>

 */

public class SALGenerator implements CheckerGenerator {

    private static String GetInfixSymbolFor(BinaryOperation op) {

        switch (op) {

            case Addition:

                return "+";

            case Minus:

                return "-";

            case Multiplication:

                return "*";

            case Division:

                return "/";

            case Exponentiation:

                return "^";

            case GreaterThen:

                return ">";

            case GreaterThenEqual:

                return ">=";

            case LessThen:

                return "<";

            case LessThenEqual:

                return "<=";

            case Equals:

                return "=";

            case NotEquals:

                return "/=";

            case BooleanAnd:

                return "AND";

            case BooleanOr:

                return "OR";

            case Implies:

                return "=>";

        }

        throw new RuntimeException("Should never happen!");

    }

    @Override

    public String GenerateBinaryOperation(BinaryOperation op, String lhsExp, String rhsExp, VariableType usedType) {

        return "(" + lhsExp + " " + GetInfixSymbolFor(op) + " " + rhsExp + ")";

    }

    private static String GetUnaryOperationSymbolFor(UnaryOperation op) {

        switch (op) {

            case Negation:

                return "NOT";

            case Minus:

                return "-";

        }

        throw new RuntimeException("Should never happen!  Asked for unhandled op: " + op + "!");

    }

    @Override

    public String GenerateUnaryOperation(UnaryOperation op, String expression, VariableType usedType) {

        return "(" + GetUnaryOperationSymbolFor(op) + " " + expression + ")";

    }

    @Override

    public String GenerateVariablesDeclaration(VariableCollection variableCollection) {

        throw new UnsupportedOperationException();

    }

    @Override

    public String GenerateLiterlaValue(String value, VariableType requestedType) {

        if (requestedType instanceof RealVariableType) {

            return value;

        } else {

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

        }

    }

}

                        "((((x * 5) = (1 / (- 4))) OR (((x > (8 + 3)) AND (9 < (x - 2))) OR ((x >= 12) OR ((NOT (34 <= (- x))) OR (5 > 4))))) => (x /= 5))",

                        "(((BVMULT(8,x,0bin00010100) = BVSDIV(0bin00000100,BVUMINUS(0bin00010000))) OR ((BVSGT(x,BVPLUS(8,0bin00100000,0bin00001100)) AND BVSLT(0bin00100100,BVSUB(x,0bin00001000))) OR (BVSGE(x,0bin00110000) OR ((NOT BVSLE(0bin10001000,BVUMINUS(x))) OR (5 > 4))))) => (x /= 0bin00010100))",

                        "(((BVMULT(8,x,0bin00010100) = BVUDIV(0bin00000100,BVUMINUS(0bin00010000))) OR ((BVGT(x,BVPLUS(8,0bin00100000,0bin00001100)) AND BVLT(0bin00100100,BVSUB(x,0bin00001000))) OR (BVGE(x,0bin00110000) OR ((NOT BVLE(0bin10001000,BVUMINUS(x))) OR (5 > 4))))) => (x /= 0bin00010100))"

                },

                {new SALGenerator(),

                        "((((x * 5) = (1 / (- 4))) OR (((x > (8 + 3)) AND (9 < (x - 2))) OR ((x >= 12) OR ((NOT (34 <= (- x))) OR (5 > 4))))) => (x /= 5))",

                        null,

                        null

                }

        });

    }