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

Add then add support for prefix unary operations. 

Now add the actual prefix unary operation support.  For now, just deal with
negation (~), and cheat the code gen appropriately.  But for the future,
things are ready for use.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10469 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent e3ee7bc2

Matlab2SMT/src/main/java/ca/mcmaster/cas/matlab2smt/CVC3Generator.java

+8 −0
Original line number Diff line number Diff line
@@ -96,6 +96,14 @@ final public class CVC3Generator implements CheckerGenerator{ 
        }

    }



    @Override

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

        if (op != MatlabUnaryOperation.Negation) {

            throw new RuntimeException("Stubbed function just became inadequate!");

        }

        return "(NOT " + expression + ")";

    }



    @Override

    public String GenerateVariableType(VariableType type) {

        if (type instanceof RealVariableType) {

Matlab2SMT/src/main/java/ca/mcmaster/cas/matlab2smt/CheckerGenerator.java

+1 −0
Original line number Diff line number Diff line
@@ -9,6 +9,7 @@ package ca.mcmaster.cas.matlab2smt; 
 * @author matthew

 */

public interface CheckerGenerator {

    public String GenerateUnaryOperation(MatlabUnaryOperation op, String expression, VariableType usedType);

    public String GenerateBinaryOperation(MatlabBinaryOperation op, String lhsExp, String rhsExp, VariableType usedType);

    public String GenerateLiterlaValue(String value, VariableType requestedType);

    public String GenerateVariableDecleration(Variable var);

Matlab2SMT/src/main/java/ca/mcmaster/cas/matlab2smt/MatlabExpressionUnaryOperation.java

0 → 100644
+49 −0
Original line number Diff line number Diff line 
/*

 * To change this template, choose Tools | Templates

 * and open the template in the editor.

 */

package ca.mcmaster.cas.matlab2smt;



/**

 *

 * @author matthew

 */

final class MatlabExpressionUnaryOperation implements MatlabExpression, MatlabExpressionWithSubExpression {



    MatlabExpressionUnaryOperation(MatlabUnaryOperation op, MatlabExpression rhs) {

        m_expr = rhs;

        m_op = op;

    }



    void setExpression(MatlabExpression expr) {

        m_expr = expr;

    }



    @Override

    public VariableType type() {

        return m_expr.type();

    }



    @Override

    public String getCheckerOutput(CheckerGenerator generator, VariableType requestedType) {

        VariableType usedType = type();

        assert usedType.equals(requestedType);



        String expression = m_expr.getCheckerOutput(generator, usedType);



        return generator.GenerateUnaryOperation(m_op, expression, usedType);

    }



    @Override

    public MatlabExpression getSubExpression() {

        return m_expr;

    }



    @Override

    public void setSubExpression(MatlabExpression subExpression) {

        m_expr = subExpression;

    }



    MatlabExpression m_expr;

    MatlabUnaryOperation m_op;

}

Matlab2SMT/src/main/java/ca/mcmaster/cas/matlab2smt/MatlabParser.java

+26 −0
Original line number Diff line number Diff line
@@ -22,6 +22,7 @@ import ca.mcmaster.cas.matlab2smt.MatlabParserParser.E10Context; 
import ca.mcmaster.cas.matlab2smt.MatlabParserParser.E11Context;

import ca.mcmaster.cas.matlab2smt.MatlabParserParser.Literal_numberContext;

import ca.mcmaster.cas.matlab2smt.MatlabParserParser.Id_plus_indexersContext;

import ca.mcmaster.cas.matlab2smt.MatlabParserParser.Prefix_operatorContext;

import java.util.ArrayDeque;

import java.util.Deque;

import org.antlr.v4.runtime.ANTLRInputStream;
@@ -97,6 +98,20 @@ final public class MatlabParser implements MatlabExpressionWithSubExpression { 
        }

    }



    private void addPrefixUnaryOperation(MatlabExpressionUnaryOperation op) {

        System.out.println("" + m_level + " " + m_opStack.peekFirst().level);

        /* Unlike Binary operations, unary operations just always insert

         * themselves into the operation stack exactly where they appear.

         * The whole left hand side handling never happens, since there is no

         * left hand side.  So just put it in place.

         *

         * Also, an unary operation is allowed to deal with a null root expression,

         * since it doesn't use it!

         */

        m_opStack.peekFirst().op.setSubExpression(op);

        m_opStack.addFirst(new ExpressionStackContainer(m_level, op));

    }



    @Override

    public MatlabExpression getSubExpression() {

        return m_rootExpression;
@@ -297,6 +312,17 @@ final public class MatlabParser implements MatlabExpressionWithSubExpression { 
            System.out.println(ctx.getText());

        }



        @Override

        public void enterPrefix_operator(Prefix_operatorContext ctx) {

            addPrefixUnaryOperation(new MatlabExpressionUnaryOperation(MatlabUnaryOperation.getOpForSymbol(ctx.getText()), null));

        }



        @Override

        public void exitPrefix_operator(Prefix_operatorContext ctx) {

            System.out.print("prefix ");

            System.out.println(ctx.getText());

        }



        @Override

        public void enterLiteral_number(Literal_numberContext ctx) {

            addExpressionValue(new MatlabLiteral(ctx.getText()));

Matlab2SMT/src/main/java/ca/mcmaster/cas/matlab2smt/MatlabUnaryOperation.java

0 → 100644
+22 −0
Original line number Diff line number Diff line 
/*

 * To change this template, choose Tools | Templates

 * and open the template in the editor.

 */

package ca.mcmaster.cas.matlab2smt;



/**

 *

 * @author matthew

 */

public enum MatlabUnaryOperation {



    Negation;



    static MatlabUnaryOperation getOpForSymbol(String text) {

        if (text.equals("~")) {

            return Negation;

        } else {

            throw new IllegalArgumentException("No such unary matlab operation defined (" + text + ")!");

        }

    }

}