Commit 34e99ffe authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Add in support for generating CVC3 from matlab tree. 

CVC3 output is possible from matlab tree.  It's not perfect yet, but it is somewhere.


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

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

0 → 100644
+15 −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

 */

interface MatlabExpression {

    VariableType type();

    

    String getCVC3Output();

}

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

0 → 100644
+37 −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 MatlabExpressionOperation implements MatlabExpression {

    MatlabExpressionOperation(MatlabExpression lhs, MatlabOperation op, MatlabExpression rhs) {

        m_lhs = lhs;

        m_rhs = rhs;

        m_op = op;

    }



    @Override

    public VariableType type() {

        VariableType lhs_type = m_lhs.type();

        VariableType rhs_type = m_rhs.type();

        

        if(lhs_type.equals(rhs_type)) {

            return lhs_type;

        } else {

            throw new IllegalStateException("Incompatible types are used together!");

        }

    }



    @Override

    public String getCVC3Output() {

        return "(" + m_lhs.getCVC3Output() + " " + m_op.convertToCVC3Op() + " " + m_rhs.getCVC3Output() + ")";

    }

    

    MatlabExpression m_lhs, m_rhs;

    MatlabOperation m_op;

}

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

0 → 100644
+23 −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

 */

enum MatlabOperation {

    Addition("+");



    MatlabOperation(String CVC3Version){

        m_CVC3Version = CVC3Version;

    }

    

    String convertToCVC3Op(){

        return m_CVC3Version;

    }

    

    String m_CVC3Version;

}

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

0 → 100644
+23 −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 class MatlabParser {

    MatlabParser(VariableParser variableListing, String matlabCode) {

        parseMatlabCode(matlabCode);

    }

    

    private void parseMatlabCode(String matlabCode) {

        

    }

    

    MatlabExpression getRootExpression() {

        return null;

    }

}

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

+7 −1
Original line number Diff line number Diff line
@@ -8,7 +8,7 @@ package ca.mcmaster.cas.matlab2smt; 
 *

 * @author matthew

 */

public class Variable {

public class Variable implements MatlabExpression {

    protected Variable(String name, VariableType type) {

        m_name = name;

        m_type = type;
@@ -18,10 +18,16 @@ public class Variable { 
        return m_name;

    }

    

    @Override

    public VariableType type() {

        return m_type;

    }

    

    private String m_name;

    private VariableType m_type;



    @Override

    public String getCVC3Output() {

        return m_name;

    }

}