Commit 161060a0 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Start implementing the SMTLIBGenerator for matlab syntax. 

Start with the SMTLIBGenerator class.  To start with, deal with variable
definitions!

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

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

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

 * 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.matlab2smt;



/**

 *

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

 */

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.

    }



    @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.

    }



    @Override

    public String GenerateLiterlaValue(String value, VariableType requestedType) {

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

    }



    @Override

    public String GenerateVariableDecleration(Variable var) {

        return "(declare-fun " + var.name() + " () " + GenerateVariableType(var.type()) + ")";

    }



    public 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() + ")");

        }

    }

}

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

+5 −1
Original line number Diff line number Diff line
@@ -22,12 +22,16 @@ public class VariableTest { 
        VariableType type = new RealVariableType();

        

        Variable var = new Variable(name, type);

        CheckerGenerator generator = new CVC3Generator();

        

        assertSame(name, var.name());

        assertSame(type, var.type());

        assertEquals(name, var.getCheckerOutput(null, new RealVariableType()));



        CheckerGenerator generator = new CVC3Generator();

        assertEquals(name+":REAL;", generator.GenerateVariableDecleration(var));



        generator = new SMTLIBGenerator();

        assertEquals("(declare-fun " +name+ " () Real)", generator.GenerateVariableDecleration(var));

    }



    // Verify handling of invalid type to getCheckerOutput

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

+15 −3
Original line number Diff line number Diff line
@@ -6,8 +6,8 @@ package ca.mcmaster.cas.matlab2smt.test; 


import ca.mcmaster.cas.matlab2smt.BooleanVariableType;

import ca.mcmaster.cas.matlab2smt.CVC3Generator;

import ca.mcmaster.cas.matlab2smt.CheckerGenerator;

import ca.mcmaster.cas.matlab2smt.RealVariableType;

import ca.mcmaster.cas.matlab2smt.SMTLIBGenerator;

import org.junit.After;

import org.junit.AfterClass;

import org.junit.Before;
@@ -29,6 +29,7 @@ public class BooleanVariableTypeTest { 
     */

    @Test

    public void testGetCVC3Definition() {

        CVC3Generator generator = new CVC3Generator();

        String variableName = "test_variable";

        BooleanVariableType instance = new BooleanVariableType();

        String expResult = "BOOLEAN";
@@ -36,6 +37,19 @@ public class BooleanVariableTypeTest { 
        assertEquals(expResult, result);

    }



    /**

     * Test of SMT-LIB generation of boolean type.

     */

    @Test

    public void testGetSMTLIBDefinition() {

        SMTLIBGenerator generator = new SMTLIBGenerator();

        String variableName = "test_variable";

        BooleanVariableType instance = new BooleanVariableType();

        String expResult = "Bool";

        String result = generator.GenerateVariableType(instance);

        assertEquals(expResult, result);

    }



    /**

     * Test of equals method, of class RealVariableType.

     */
@@ -66,6 +80,4 @@ public class BooleanVariableTypeTest { 
        assertFalse(instance.canCastToType(new RealVariableType()));

        assertFalse(instance.canCastToType(new BooleanVariableType()));

    }



    CVC3Generator generator = new CVC3Generator();

}

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

+14 −0
Original line number Diff line number Diff line
@@ -7,6 +7,7 @@ package ca.mcmaster.cas.matlab2smt.test; 
import ca.mcmaster.cas.matlab2smt.BooleanVariableType;

import ca.mcmaster.cas.matlab2smt.CVC3Generator;

import ca.mcmaster.cas.matlab2smt.RealVariableType;

import ca.mcmaster.cas.matlab2smt.SMTLIBGenerator;

import org.junit.After;

import org.junit.AfterClass;

import org.junit.Before;
@@ -36,6 +37,19 @@ public class RealVariableTypeTest { 
        assertEquals(expResult, result);

    }



    /**

     * Test SMTLIB generates the correct type.

     */

    @Test

    public void testGetSMTLIBDefinition() {

        SMTLIBGenerator generator = new SMTLIBGenerator();

        String variableName = "test_variable";

        RealVariableType instance = new RealVariableType();

        String expResult = "Real";

        String result = generator.GenerateVariableType(instance);

        assertEquals(expResult, result);

    }



    /**

     * Test of equals method, of class RealVariableType.

     */