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

Implement most of the important matlab -> smtlib generation code. 

The system can now generate SMT-LIB code from the parsed Matlab code.  It doesn't
deal with tables (yet), but that is next.  Also use the MatlabParser tests to
verify the generated SMT-LIB code.

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

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

+24 −4
Original line number Diff line number Diff line
@@ -23,17 +23,21 @@ package ca.mcmaster.cas.matlab2smt; 
public class SMTLIBGenerator implements CheckerGenerator {

    @Override

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

        return null;  //To change body of implemented methods use File | Settings | File Templates.

        return "(not " + expression + ")";  //To change body of implemented methods use File | Settings | File Templates.

    }



    @Override

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

        return null;  //To change body of implemented methods use File | Settings | File Templates.

        return "(" + SMTLIBGenerator.GetBinaryOperationSymbolFor(op) + " " + lhsExp + " " + rhsExp + ")";

    }



    @Override

    public String GenerateLiterlaValue(String value, VariableType requestedType) {

        return null;  //To change body of implemented methods use File | Settings | File Templates.

        if (requestedType instanceof RealVariableType || requestedType instanceof MatlabLiteral.LiteralNumberType) {

            return value;

        } else {

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

        }

    }



    @Override
@@ -41,7 +45,7 @@ public class SMTLIBGenerator implements CheckerGenerator { 
        return "(declare-fun " + var.name() + " () " + GenerateVariableType(var.type()) + ")";

    }



    public String GenerateVariableType(VariableType type) {

    public static String GenerateVariableType(VariableType type) {

        if (type instanceof RealVariableType) {

            return "Real";

        } else if (type instanceof BooleanVariableType) {
@@ -50,4 +54,20 @@ public class SMTLIBGenerator implements CheckerGenerator { 
            throw new IllegalArgumentException("SMT-LIB Doesn't handle this variable type (Class: " + type.getClass().getName() + ")");

        }

    }



    private static String GetBinaryOperationSymbolFor(MatlabBinaryOperation op) {

        switch (op) {

            case Addition:

                return "+";

            case Multiplication:

                return "*";

            case GreaterThen:

                return ">";

            case Equals:

                return "=";

            case BooleanAnd:

                return "and";

        }

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

    }

}

Matlab2SMT/src/test/java/ca/mcmaster/cas/matlab2smt/test/MatlabParserTest.java

+42 −10
Original line number Diff line number Diff line
@@ -11,6 +11,7 @@ import ca.mcmaster.cas.matlab2smt.MatlabExpression; 
import ca.mcmaster.cas.matlab2smt.MatlabLiteral;

import ca.mcmaster.cas.matlab2smt.MatlabParser;

import ca.mcmaster.cas.matlab2smt.RealVariableType;

import ca.mcmaster.cas.matlab2smt.SMTLIBGenerator;

import ca.mcmaster.cas.matlab2smt.Variable;

import ca.mcmaster.cas.matlab2smt.VariableParser;

import org.junit.Test;
@@ -31,6 +32,9 @@ public class MatlabParserTest { 
        MatlabExpression expr = parser.getRootExpression();

        

        assertSame(MatlabLiteral.class, expr.getClass());

        CheckerGenerator generator = new CVC3Generator();

        assertEquals("5", expr.getCheckerOutput(generator, new RealVariableType()));

        generator = new SMTLIBGenerator();

        assertEquals("5", expr.getCheckerOutput(generator, new RealVariableType()));

    }
@@ -41,6 +45,9 @@ public class MatlabParserTest { 
        

        assertSame(Variable.class, expr.getClass());

        assertEquals(new RealVariableType(), expr.type());

        CheckerGenerator generator = new CVC3Generator();

        assertEquals("a", expr.getCheckerOutput(generator, expr.type()));

        generator = new SMTLIBGenerator();

        assertEquals("a", expr.getCheckerOutput(generator, expr.type()));

    }
@@ -50,7 +57,10 @@ public class MatlabParserTest { 
        MatlabExpression expr = parser.getRootExpression();

        

        assertEquals(new MatlabLiteral(null).type(), expr.type());

        CheckerGenerator generator = new CVC3Generator();

        assertEquals("(4 + 5)", expr.getCheckerOutput(generator, expr.type()));

        generator = new SMTLIBGenerator();

        assertEquals("(+ 4 5)", expr.getCheckerOutput(generator, expr.type()));

    }

    

    @Test
@@ -59,7 +69,10 @@ public class MatlabParserTest { 
        MatlabExpression expr = parser.getRootExpression();

        

        assertEquals(new MatlabLiteral(null).type(), expr.type());

        CheckerGenerator generator = new CVC3Generator();

        assertEquals("(4 * 5)", expr.getCheckerOutput(generator, expr.type()));

        generator = new SMTLIBGenerator();

        assertEquals("(* 4 5)", expr.getCheckerOutput(generator, expr.type()));

    }

    

    @Test
@@ -68,7 +81,10 @@ public class MatlabParserTest { 
        MatlabExpression expr = parser.getRootExpression();



        assertEquals(new MatlabLiteral(null).type(), expr.type());

        CheckerGenerator generator = new CVC3Generator();

        assertEquals("(NOT 0)", expr.getCheckerOutput(generator, expr.type()));

        generator = new SMTLIBGenerator();

        assertEquals("(not 0)", expr.getCheckerOutput(generator, expr.type()));

    }



    @Test
@@ -77,7 +93,10 @@ public class MatlabParserTest { 
        MatlabExpression expr = parser.getRootExpression();

        

        assertEquals(new MatlabLiteral(null).type(), expr.type());

        CheckerGenerator generator = new CVC3Generator();

        assertEquals("((4 + 5) + 6)", expr.getCheckerOutput(generator, expr.type()));

        generator = new SMTLIBGenerator();

        assertEquals("(+ (+ 4 5) 6)", expr.getCheckerOutput(generator, expr.type()));

    }

    

    @Test
@@ -86,7 +105,10 @@ public class MatlabParserTest { 
        MatlabExpression expr = parser.getRootExpression();

        

        assertEquals(new MatlabLiteral(null).type(), expr.type());

        CheckerGenerator generator = new CVC3Generator();

        assertEquals("((4 * 5) + 6)", expr.getCheckerOutput(generator, expr.type()));

        generator = new SMTLIBGenerator();

        assertEquals("(+ (* 4 5) 6)", expr.getCheckerOutput(generator, expr.type()));

    }

    

    @Test
@@ -95,22 +117,27 @@ public class MatlabParserTest { 
        MatlabExpression expr = parser.getRootExpression();

        

        assertEquals(new MatlabLiteral(null).type(), expr.type());

        CheckerGenerator generator = new CVC3Generator();

        assertEquals("(4 + (5 * 6))", expr.getCheckerOutput(generator, expr.type()));

        generator = new SMTLIBGenerator();

        assertEquals("(+ 4 (* 5 6))", expr.getCheckerOutput(generator, expr.type()));

    }

    

    @Test

    public void testInsanseExpressionsWithLiterals() {

        MatlabParser parser = new MatlabParser(null, "4*5+6*7\n");

        MatlabExpression expr = parser.getRootExpression();

        MatlabParser parser2 = new MatlabParser(null, "4+5+6*7*8\n");



        assertEquals(new MatlabLiteral(null).type(), expr.type());

        assertEquals("((4 * 5) + (6 * 7))", expr.getCheckerOutput(generator, expr.type()));

        CheckerGenerator cvc3generator = new CVC3Generator();

        CheckerGenerator smtlibgenerator = new SMTLIBGenerator();



        parser = new MatlabParser(null, "4+5+6*7*8\n");

        expr = parser.getRootExpression();

        assertEquals(new MatlabLiteral(null).type(), parser.getRootExpression().type());

        assertEquals("((4 * 5) + (6 * 7))", parser.getRootExpression().getCheckerOutput(cvc3generator, parser2.getRootExpression().type()));

        assertEquals("(+ (* 4 5) (* 6 7))", parser.getRootExpression().getCheckerOutput(smtlibgenerator, parser2.getRootExpression().type()));

        

        assertEquals(new MatlabLiteral(null).type(), expr.type());

        assertEquals("((4 + 5) + ((6 * 7) * 8))", expr.getCheckerOutput(generator, expr.type()));

        assertEquals(new MatlabLiteral(null).type(), parser2.getRootExpression().type());

        assertEquals("((4 + 5) + ((6 * 7) * 8))", parser2.getRootExpression().getCheckerOutput(cvc3generator, parser2.getRootExpression().type()));

        assertEquals("(+ (+ 4 5) (* (* 6 7) 8))", parser2.getRootExpression().getCheckerOutput(smtlibgenerator, parser2.getRootExpression().type()));

    }

    

    @Test
@@ -119,7 +146,10 @@ public class MatlabParserTest { 
        MatlabExpression expr = parser.getRootExpression();

        

        assertEquals(new BooleanVariableType(), expr.type());

        CheckerGenerator generator = new CVC3Generator();

        assertEquals("(5 > 5)", expr.getCheckerOutput(generator, expr.type()));

        generator = new SMTLIBGenerator();

        assertEquals("(> 5 5)", expr.getCheckerOutput(generator, expr.type()));

    }



    @Test
@@ -128,7 +158,9 @@ public class MatlabParserTest { 
        MatlabExpression expr = parser.getRootExpression();



        assertEquals(new BooleanVariableType(), expr.type());

        CheckerGenerator generator = new CVC3Generator();

        assertEquals("(((z = 1) AND (x = 0)) AND (y = 2))", expr.getCheckerOutput(generator, expr.type()));

        generator = new SMTLIBGenerator();

        assertEquals("(and (and (= z 1) (= x 0)) (= y 2))", expr.getCheckerOutput(generator, expr.type()));

    }

    CheckerGenerator generator = new CVC3Generator();

}