Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/App.java

+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+import java.util.logging.Level;
+import java.util.logging.Logger;
+import org.antlr.v4.runtime.misc.TestRig;
+
+/**
+ * Hello world!
+ *
+ */
+public class App 
+{
+    public static void main( String[] args )
+    {
+        String[] args2 = {"ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParser", "expression", "-tree"};
+        try {
+            TestRig.main(args2);
+        } catch (Exception ex) {
+            Logger.getLogger(App.class.getName()).log(Level.SEVERE, null, ex);
+        }
+        System.out.println( "Hello World!" );
+    }
+
+    public int test(Object p) {
+        return 5;
+    }
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/BinaryOperation.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+import java.util.Arrays;
+import java.util.Collection;
+
+/**
+ *
+ * @author matthew
+ */
+public enum BinaryOperation {
+
+    Addition,
+    Minus,
+    Multiplication,
+    Division,
+    Exponentiation,
+
+    GreaterThen,
+    GreaterThenEqual,
+    LessThen,
+    LessThenEqual,
+    Equals,
+    NotEquals,
+
+    Implies,
+    BooleanAnd,
+    BooleanOr;
+
+    Collection<VariableTypeMarker> getInputTypeForOutput(VariableTypeMarker outputType) {
+        // Boolean inputs only work with a boolean input!
+        if (this == BooleanAnd || this == BooleanOr || this == Implies || this == GreaterThen || this == GreaterThenEqual ||
+                this == LessThen || this == LessThenEqual || this == Equals || this == NotEquals) {
+            if (!outputType.equals(new BooleanVariableType())) {
+                throw new IllegalArgumentException("Boolean operators and comparisons require a boolean output type!");
+            }
+        }
+
+        // Comparisions produce boolean outputs!
+        switch(this) {
+            case GreaterThen:
+            case GreaterThenEqual:
+            case LessThen:
+            case LessThenEqual:
+            case Equals:
+            case NotEquals:
+                return Arrays.asList(new VariableTypeMarker[]{new RealVariableType(), new FixedPointVariableType.Marker()});
+        }
+        return Arrays.asList(new VariableTypeMarker[]{outputType});
+    }
+
+    public VariableType getOutputForInput(VariableType inputType) {
+        // Boolean inputs only work with a boolean input!
+        if (this == BooleanAnd || this == BooleanOr || this == Implies) {
+            if (!inputType.equals(new BooleanVariableType())) {
+                throw new IllegalArgumentException("Boolean operators require a boolean input type!");
+            }
+        }
+
+        // Comparisions produce boolean outputs!
+        switch(this) {
+            case GreaterThen:
+            case GreaterThenEqual:
+            case LessThen:
+            case LessThenEqual:
+            case Equals:
+            case NotEquals:
+                return new BooleanVariableType();
+        }
+        return inputType;
+    }
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/BooleanVariableType.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+/**
+ *
+ * @author matthew
+ */
+public class BooleanVariableType extends VariableType {
+
+    @Override
+    public boolean equals(Object other) {
+        return other instanceof BooleanVariableType;
+    }
+
+    @Override
+    public int hashCode() {
+        return 0;
+    }
+
+    @Override
+    public boolean canCastToType(VariableType type) {
+        return false;
+    }
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/CVC3Generator.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+import java.math.BigDecimal;
+import java.math.BigInteger;
+import java.util.Map;
+
+import org.apache.commons.lang3.StringUtils;
+
+/**
+ *
+ * @author matthew
+ */
+final public class CVC3Generator implements CheckerGenerator{
+
+    // For operations that don't have specific signed/unsigned representations, use this function.
+    private static String GetIndifferentFixedPointFunctionFor(BinaryOperation op) {
+        switch (op) {
+            case Addition:
+                return "BVPLUS(";
+            case Minus:
+                return "BVSUB(";
+            case Multiplication:
+                return "BVMULT(";
+        }
+        throw new IllegalArgumentException("Operation " + op + " doesn't have a fixed point function!");
+    }
+
+    private static String GetSignedFixedPointFunctionFor(BinaryOperation op) {
+        switch (op) {
+            case Division:
+                return "BVSDIV(";
+            case GreaterThen:
+                return "BVSGT(";
+            case GreaterThenEqual:
+                return "BVSGE(";
+            case LessThen:
+                return "BVSLT(";
+            case LessThenEqual:
+                return "BVSLE(";
+        }
+        return GetIndifferentFixedPointFunctionFor(op);
+    }
+
+    private static String GetUnsignedFixedPointFunctionFor(BinaryOperation op) {
+        switch (op) {
+            case Division:
+                return "BVUDIV(";
+            case GreaterThen:
+                return "BVGT(";
+            case GreaterThenEqual:
+                return "BVGE(";
+            case LessThen:
+                return "BVLT(";
+            case LessThenEqual:
+                return "BVLE(";
+        }
+        return GetIndifferentFixedPointFunctionFor(op);
+    }
+
+    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!");
+    }
+
+    protected static String ConvertToOutputOp(BinaryOperation op, VariableType type) {
+        switch (OpTypeForVariableType(op, type)) {
+            case Function:
+                String func = GetSignedFixedPointFunctionFor(op);
+                if (!((FixedPointVariableType) type).isSigned()) {
+                    func = GetUnsignedFixedPointFunctionFor(op);
+                }
+                if (op == BinaryOperation.Addition || op == BinaryOperation.Multiplication) {
+                    FixedPointVariableType typeF = (FixedPointVariableType) type;
+                    return func + typeF.digits() + ",";
+                } else {
+                    return func;
+                }
+            case CenterOp:
+                return GetInfixSymbolFor(op);
+            default:
+                throw new IllegalStateException("CVC3 Operation type asked for that doesn't exist!");
+        }
+    }
+
+    private static OperationType OpTypeForVariableType(BinaryOperation op, VariableType type) {
+        if (type instanceof FixedPointVariableType && op != BinaryOperation.Equals && op != BinaryOperation.NotEquals) {
+            if (op == BinaryOperation.Exponentiation) {
+                throw new IllegalArgumentException("Cannot generate exponential functions in fixed point!");
+            }
+            return OperationType.Function;
+        } else {
+            return OperationType.CenterOp;
+        }
+    }
+
+    @Override
+    public String GenerateBinaryOperation(BinaryOperation op, String lhsExp, String rhsExp, VariableType usedType) {
+        switch (CVC3Generator.OpTypeForVariableType(op, usedType)) {
+            case CenterOp:
+                return "(" + lhsExp + " " + CVC3Generator.ConvertToOutputOp(op, usedType) + " " + rhsExp + ")";
+            case Function:
+                return CVC3Generator.ConvertToOutputOp(op, usedType) + lhsExp + "," + rhsExp + ")";
+            default:
+                throw new IllegalStateException("Cannot output expression operation for requested operation type.");
+        }
+    }
+
+    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) {
+        switch (CVC3Generator.OpTypeForVariableType(op, usedType)) {
+            case PrefixOp:
+                return "(" + CVC3Generator.ConvertToOutputOp(op, usedType) + " " + expression + ")";
+            case Function:
+                return CVC3Generator.ConvertToOutputOp(op, usedType) + "(" + expression + ")";
+            default:
+                throw new IllegalStateException("Cannot output expression operation for requested operation type.");
+        }
+    }
+
+    private static OperationType OpTypeForVariableType(UnaryOperation op, VariableType usedType) {
+        if (usedType instanceof FixedPointVariableType) {
+            return OperationType.Function;
+        }
+        return OperationType.PrefixOp;
+    }
+
+    private static String ConvertToOutputOp(UnaryOperation op, VariableType usedType) {
+        switch (op) {
+            case Negation:
+                return "NOT";
+            case Minus:
+                if (usedType instanceof FixedPointVariableType) {
+                    return "BVUMINUS";
+                } else {
+                    return "-";
+                }
+        }
+        throw new IllegalArgumentException("Unhandled operation: " + op);
+    }
+
+    public String GenerateVariableType(VariableType type) {
+        if (type instanceof RealVariableType) {
+            return "REAL";
+        } else if (type instanceof FixedPointVariableType) {
+            return "BITVECTOR(" + ((FixedPointVariableType) type).digits() + ")";
+        } else if (type instanceof BooleanVariableType) {
+            return "BOOLEAN";
+        } else {
+            throw new IllegalArgumentException("CVC3 Doesn't handle this variable type (Class: " + type.getClass().getName() + ")");
+        }
+    }
+
+    @Override
+    public String GenerateVariablesDeclaration(VariableCollection variableCollection) {
+        Map<String, Variable> vars = variableCollection.getVariables();
+
+        StringBuilder ret = new StringBuilder();
+        // First generate all the variables.
+        for(Variable var : vars.values()) {
+            ret.append(var.name())
+               .append(":")
+               .append(GenerateVariableType(var.type()))
+               .append(";\n");
+        }
+
+        // Then generate the variable predicates.  This ensures any dependent variables are declared.
+        for(Variable var : vars.values()) {
+            if (var.type().subtypePredicate() != null) {
+                ret.append("ASSERT ")
+                   .append(var.type().subtypePredicate().getCheckerOutput(this, new BooleanVariableType()))
+                   .append(";\n");
+            }
+        }
+
+        return ret.toString();
+    }
+
+    @Override
+    public String GenerateLiterlaValue(String value, VariableType requestedType) {
+        if (requestedType instanceof RealVariableType) {
+            if (value.contains(".")) {
+                String[] fraction = value.split("\\.");
+
+                String res = "(";
+                res += StringUtils.join(fraction, "");
+                res += "/1" + StringUtils.repeat('0', fraction[1].length()) + ")";
+
+                return res;
+            } else {
+                return value;
+            }
+        } else if (requestedType instanceof FixedPointVariableType) {
+            FixedPointVariableType type = (FixedPointVariableType) requestedType;
+            BigDecimal decimal = new BigDecimal(value);
+            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';
+            }
+
+            if (intOut.signum() < 0) {
+                return "0bin" + StringUtils.repeat('1', type.digits() - bits.length()) + bits;
+            } else {
+                return "0bin" + StringUtils.repeat('0', type.digits() - bits.length()) + bits;
+            }
+        } else {
+            throw new IllegalArgumentException("Can't cast literal to that type!");
+        }
+    }
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/CheckerGenerator.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+import java.util.Map;
+
+/**
+ *
+ * @author matthew
+ */
+public interface CheckerGenerator {
+    public String GenerateUnaryOperation(UnaryOperation op, String expression, VariableType usedType);
+    public String GenerateBinaryOperation(BinaryOperation op, String lhsExp, String rhsExp, VariableType usedType);
+    public String GenerateLiterlaValue(String value, VariableType requestedType);
+    public String GenerateVariablesDeclaration(VariableCollection vars);
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/Expression.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+/**
+ *
+ * @author matthew
+ */
+public interface Expression {
+
+    /* This methods returns an actual variable type for the requested input type.  If due to the setup of the system,
+    *  this is not possible, then this function should return null.
+    */
+    VariableType actualOutputTypeForRequestedOutput(VariableTypeMarker requestedType);
+
+    String getCheckerOutput(CheckerGenerator generator, VariableType requestedType);
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/ExpressionBinaryOperation.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+import java.util.Collection;
+
+/**
+ *
+ * @author matthew
+ */
+public final class ExpressionBinaryOperation implements Expression, ExpressionWithSubExpression {
+
+    public ExpressionBinaryOperation(Expression lhs, BinaryOperation op, Expression rhs) {
+        m_lhs = lhs;
+        m_rhs = rhs;
+        m_op = op;
+    }
+
+    public void setLHS(Expression expr) {
+        m_lhs = expr;
+    }
+
+    public void setRHS(Expression expr) {
+        m_rhs = expr;
+    }
+
+    private VariableType getInputTypeForOutput(VariableTypeMarker requestedType) {
+        Collection<VariableTypeMarker> allowedInputTypes = m_op.getInputTypeForOutput(requestedType);
+        for(VariableTypeMarker allowedType : allowedInputTypes) {
+            VariableType inputType = m_lhs.actualOutputTypeForRequestedOutput(allowedType);
+            if(inputType != null &&
+                    m_rhs.actualOutputTypeForRequestedOutput(inputType) != null) {
+                return inputType;
+            }
+            inputType = m_rhs.actualOutputTypeForRequestedOutput(allowedType);
+            if(inputType != null &&
+                    m_lhs.actualOutputTypeForRequestedOutput(inputType) != null) {
+                return inputType;
+            }
+        }
+        return null;
+    }
+
+    @Override
+    public VariableType actualOutputTypeForRequestedOutput(VariableTypeMarker requestedType) {
+        VariableType inputType = getInputTypeForOutput(requestedType);
+        if (inputType != null) {
+            return m_op.getOutputForInput(inputType);
+        }
+        return null;
+    }
+
+    @Override
+    public String getCheckerOutput(CheckerGenerator generator, VariableType requestedType) {
+        VariableType inputType = getInputTypeForOutput(requestedType);
+        if (inputType == null) {
+            throw new IllegalArgumentException("Requested output type is not valid for the expression's output type (" + requestedType.getClass().getSimpleName() + "!");
+        }
+
+        String lhsExp = m_lhs.getCheckerOutput(generator, inputType);
+        String rhsExp = m_rhs.getCheckerOutput(generator, inputType);
+
+        return generator.GenerateBinaryOperation(m_op, lhsExp, rhsExp, inputType);
+    }
+
+    @Override
+    public Expression getSubExpression() {
+        return m_rhs;
+    }
+
+    @Override
+    public void setSubExpression(Expression subExpression) {
+        m_rhs = subExpression;
+    }
+
+    @Override
+    public String toString() {
+        return "(" + m_lhs.toString() + " " + m_op.toString() + " " + m_rhs.toString() + ")";
+    }
+
+    private Expression m_lhs, m_rhs;
+    private BinaryOperation m_op;
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/ExpressionUnaryOperation.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+/**
+ *
+ * @author matthew
+ */
+public final class ExpressionUnaryOperation implements Expression, ExpressionWithSubExpression {
+
+    public ExpressionUnaryOperation(UnaryOperation op, Expression rhs) {
+        m_expr = rhs;
+        m_op = op;
+    }
+
+    void setExpression(Expression expr) {
+        m_expr = expr;
+    }
+
+    @Override
+    public VariableType actualOutputTypeForRequestedOutput(VariableTypeMarker requestedType) {
+        return m_expr.actualOutputTypeForRequestedOutput(requestedType);
+    }
+
+    @Override
+    public String getCheckerOutput(CheckerGenerator generator, VariableType requestedType) {
+        if (actualOutputTypeForRequestedOutput(requestedType) == null) {
+            throw new IllegalArgumentException("Can generate output for requested type!");
+        }
+
+        String expression = m_expr.getCheckerOutput(generator, requestedType);
+
+        return generator.GenerateUnaryOperation(m_op, expression, requestedType);
+    }
+
+    @Override
+    public Expression getSubExpression() {
+        return m_expr;
+    }
+
+    @Override
+    public void setSubExpression(Expression subExpression) {
+        m_expr = subExpression;
+    }
+
+    @Override
+    public String toString() {
+        return "( " + m_op + " " + m_expr + ")";
+    }
+
+    private Expression m_expr;
+    private UnaryOperation m_op;
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/ExpressionValue.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+/** This interface means the expression is a value with no further expansion possible.
+ * This is just a marker to mean an expression is only a value.
+ *
+ * @author matthew
+ */
+public interface ExpressionValue extends Expression {
+    
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/ExpressionWithSubExpression.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+/**
+ *
+ * @author matthew
+ */
+public interface ExpressionWithSubExpression {
+    public Expression getSubExpression();
+    public void setSubExpression(Expression subExpression);
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/FixedPointVariableType.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+/**
+ *
+ * @author matthew
+ */
+final public class FixedPointVariableType extends VariableType {
+
+    public FixedPointVariableType(boolean signed, int digits, int fractionPart) {
+        m_isSigned = signed;
+        m_digits = digits;
+        m_fractionPart = fractionPart;
+    }
+
+    public boolean isSigned() {
+        return m_isSigned;
+    }
+
+    public int digits() {
+        return m_digits;
+    }
+
+    public int fractionPart() {
+        return m_fractionPart;
+    }
+
+    @Override
+    public boolean canCastToType(VariableType type) {
+        return false;
+    }
+
+    @Override
+    public boolean equals(Object othero) {
+        if (!(othero instanceof FixedPointVariableType)) {
+            return false;
+        } else {
+            FixedPointVariableType other = (FixedPointVariableType) othero;
+            if (other.m_isSigned == m_isSigned
+                    && other.m_digits == m_digits
+                    && other.m_fractionPart == m_fractionPart) {
+                return true;
+            } else {
+                return false;
+            }
+        }
+    }
+
+    @Override
+    public int hashCode() {
+        int hash = 0;
+        hash += (this.m_isSigned ? 1 : 0);
+        hash = 2 * hash + this.m_fractionPart;
+        hash = 83 * hash + this.m_digits;
+        return hash;
+    }
+
+    private final int m_fractionPart;
+    private final int m_digits;
+    private final boolean m_isSigned;
+
+    public static class Marker implements VariableTypeMarker {
+        @Override
+        public boolean isMarkerFor(VariableType m_type) {
+            return m_type instanceof FixedPointVariableType;
+        }
+    }
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/Literal.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+/**
+ *
+ * @author matthew
+ */
+public final class Literal implements Expression, ExpressionValue {
+
+    public Literal(String value) {
+        m_value = value;
+    }
+
+    @Override
+    public VariableType actualOutputTypeForRequestedOutput(VariableTypeMarker requestedType) {
+        if (requestedType instanceof RealVariableType ||
+                requestedType instanceof FixedPointVariableType) {
+            return (VariableType)requestedType;
+        }
+        return null;
+    }
+
+    @Override
+    public String getCheckerOutput(CheckerGenerator generator, VariableType requestedType) {
+        return generator.GenerateLiterlaValue(m_value, requestedType);
+    }
+
+    @Override
+    public String toString() {
+        return m_value;
+    }
+
+    final String m_value;
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/OperationType.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+/**
+ *
+ * @author matthew
+ */
+public enum OperationType {
+    CenterOp,
+    PrefixOp,
+    PostfixOp,
+    Function;
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/RealVariableType.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+/**
+ *
+ * @author matthew
+ */
+public final class RealVariableType extends VariableType {
+    @Override
+    public boolean equals(Object other) {
+        return other instanceof RealVariableType;
+    }
+
+    @Override
+    public int hashCode() {
+        return 0;
+    }
+
+    @Override
+    public boolean canCastToType(VariableType type) {
+        return false;
+    }
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/SMTLIBGenerator.java

+/*
+ * Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+import java.util.Map;
+
+/**
+ *
+ * @author Matthew Dawson <matthew@mjdsystems.ca>
+ */
+public class SMTLIBGenerator implements CheckerGenerator {
+    @Override
+    public String GenerateUnaryOperation(UnaryOperation op, String expression, VariableType usedType) {
+        return "(" + SMTLIBGenerator.GetUnaryOperationSymbolFor(op) + " " + expression + ")";  //To change body of implemented methods use File | Settings | File Templates.
+    }
+
+    @Override
+    public String GenerateBinaryOperation(BinaryOperation op, String lhsExp, String rhsExp, VariableType usedType) {
+        return "(" + SMTLIBGenerator.GetBinaryOperationSymbolFor(op) + " " + lhsExp + " " + rhsExp + ")";
+    }
+
+    @Override
+    public String GenerateLiterlaValue(String value, VariableType requestedType) {
+        if (requestedType instanceof RealVariableType) {
+            if (value.contains(".")) {
+                return value;
+            } else {
+                return value + ".0";
+            }
+        } else {
+            throw new IllegalArgumentException("Can't cast literal to that type!");
+        }
+    }
+
+    @Override
+    public String GenerateVariablesDeclaration(VariableCollection variableCollection) {
+        Map<String, Variable> vars = variableCollection.getVariables();
+
+        StringBuilder ret = new StringBuilder();
+        // First generate all the variables.
+        for (Variable var : vars.values()) {
+            ret.append("(declare-fun ")
+               .append(var.name())
+               .append(" () ")
+               .append(GenerateVariableType(var.type()))
+               .append(")\n");
+        }
+
+        // Then generate the variable predicates.  This ensures any dependent variables are declared.
+        for(Variable var : vars.values()) {
+            if (var.type().subtypePredicate() != null) {
+                ret.append("(assert ")
+                        .append(var.type().subtypePredicate().getCheckerOutput(this, new BooleanVariableType()))
+                        .append(")\n");
+            }
+        }
+        return ret.toString();
+    }
+
+    public static String GenerateVariableType(VariableType type) {
+        if (type instanceof RealVariableType) {
+            return "Real";
+        } else if (type instanceof BooleanVariableType) {
+            return "Bool";
+        } else {
+            throw new IllegalArgumentException("SMT-LIB Doesn't handle this variable type (Class: " + type.getClass().getName() + ")");
+        }
+    }
+
+    private static String GetBinaryOperationSymbolFor(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 "distinct";
+            case BooleanAnd:
+                return "and";
+            case BooleanOr:
+                return "or";
+            case Implies:
+                return "=>";
+        }
+        throw new RuntimeException("Should never happen!  Asked for unhandled op: " + op + "!");
+    }
+
+    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 + "!");
+    }
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/UnaryOperation.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+/**
+ *
+ * @author matthew
+ */
+public enum UnaryOperation {
+
+    Minus,
+    Negation;
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/Variable.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+/**
+ *
+ * @author matthew
+ */
+public class Variable implements Expression, ExpressionValue {
+    public Variable(String name, VariableType type) {
+        m_name = name;
+        m_type = type;
+    }
+
+    public String name() {
+        return m_name;
+    }
+
+    public VariableType type() {
+        return m_type;
+    }
+
+    @Override
+    public VariableType actualOutputTypeForRequestedOutput(VariableTypeMarker requestedType) {
+        if (requestedType.isMarkerFor(m_type)) {
+            return m_type;
+        }
+        return null;
+    }
+
+    private String m_name;
+    private VariableType m_type;
+
+    @Override
+    public String getCheckerOutput(CheckerGenerator generator, VariableType requestedType) {
+        if (!type().equals(requestedType)) {
+            throw new IllegalArgumentException("Requested output type is not the expression's output type!");
+        }
+        return m_name;
+    }
+
+    @Override
+    public String toString() {
+        return m_name;
+    }
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/VariableCollection.java

+/*
+ * Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+import java.util.Map;
+
+/**
+ * @author Matthew Dawson <matthew@mjdsystems.ca>
+ */
+final public class VariableCollection {
+    public VariableCollection(Map<String, Variable> variables) {
+        m_variables = variables;
+    }
+
+    public Map<String, Variable> getVariablesAndEnumeratedValues() {
+        return m_variables;
+    }
+
+    public Map<String, Variable> getVariables() {
+        return m_variables;
+    }
+
+    private final Map<String,Variable> m_variables;
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/VariableType.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+/**
+ *
+ * @author matthew
+ */
+public abstract class VariableType implements VariableTypeMarker {
+    /**
+     * Marks whether the type can be cast to this type.  Certain values may be
+     * castable to a different type.  If possible, this method will mark it as
+     * such.
+     * @param type The type this variable type should cast to.
+     * @return True if this type can act like the other type.  False otherwise.
+     */
+    abstract public boolean canCastToType(VariableType type);
+
+    /* By default, all types are their own markers.  Thus by default implement isMarkerFor to represent that.  Override
+     * if further behaviour is necessary.
+     */
+     @Override
+    public boolean isMarkerFor(VariableType m_type) {
+        return this.equals(m_type);
+    }
+
+    public Expression subtypePredicate() {
+        return m_subtypePredicate;
+    }
+
+    public void setSubtypePredicate(Expression subtypePredicate) {
+        m_subtypePredicate = subtypePredicate;
+    }
+
+    private Expression m_subtypePredicate;
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/VariableTypeMarker.java

+/*
+ * Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+/**
+ * @author Matthew Dawson <matthew@mjdsystems.ca>
+ */
+interface VariableTypeMarker {
+    boolean isMarkerFor(VariableType m_type);
+}