Commit 93fff796 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Implement other important math operators for SMTLIB. 

Implement other operators for SMTLIB.  Also implement a test for it.  The test
is parameterized, so CVC3 support is easy to add.  Due to the parameterization,
a newer version of JUnit is required, so bump the version in the pom.xml file.

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

Matlab2SMT/pom.xml

+1 −1
Original line number Diff line number Diff line
@@ -18,7 +18,7 @@ 
        <dependency>

            <groupId>junit</groupId>

            <artifactId>junit</artifactId>

            <version>4.10</version>

            <version>4.11</version>

            <scope>test</scope>

        </dependency>

        <dependency>

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

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

    @Override

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

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

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

    }



    @Override
@@ -63,15 +63,37 @@ public class SMTLIBGenerator implements CheckerGenerator { 
        switch (op) {

            case Addition:

                return "+";

            case Minus:

                return "-";

            case Multiplication:

                return "*";

            case Division:

                return "/";

            case GreaterThen:

                return ">";

            case GreaterThenEqual:

                return ">=";

            case LessThen:

                return "<";

            case LessThenEqual:

                return "<=";

            case Equals:

                return "=";

            case BooleanAnd:

                return "and";

            case BooleanOr:

                return "or";

        }

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

        throw new RuntimeException("Should never happen!  Asked for unhandled op: " + op + "!");

    }



    private static String GetUnaryOperationSymbolFor(MatlabUnaryOperation op) {

        switch (op) {

            case Negation:

                return "not";

            case Minus:

                return "-";

        }

        throw new RuntimeException("Should never happen!  Asked for unhandled op: " + op + "!");

    }

}

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

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



import org.junit.Test;

import org.junit.runner.RunWith;

import org.junit.runners.Parameterized;

import org.junit.runners.Parameterized.Parameter;

import org.junit.runners.Parameterized.Parameters;



import java.util.Arrays;

import java.util.Collection;



import static org.junit.Assert.*;



/**

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

 */

@RunWith(Parameterized.class)

public class GenericGeneratorTest {

    @Parameters

    public static Collection<Object[]> data() {

        return Arrays.asList(new Object[][]{

                {new SMTLIBGenerator(), "(or (or (or (= (* x 5.0) (/ 1.0 (- 4.0))) (and (> 4.0 (+ 8.0 3.0)) (< 9.0 (- 1.0 2.0)))) (>= 11.0 12.0)) (not (<= 34.0 (- 54.0))))"}

        });

    }



    static private String query = "(x * 5) == (1 / -4) || ((4 > (8 + 3)) && (9 < 1 - 2)) || 11 >= 12 || ~(34 <= -54)";

    static private VariableType outputType = new BooleanVariableType();



    @Parameter(value = 0)

    public CheckerGenerator generator;



    @Parameter(value = 1)

    public String RealExpectedOutput;



    @Test

    public void doTest() {

        VariableParser vars = new VariableParser("x");

        MatlabParser parser = new MatlabParser(vars, query);

System.out.println(parser.getRootExpression().toString());

        assertEquals(RealExpectedOutput, parser.getRootExpression().getCheckerOutput(generator, outputType));

    }

}