Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/GenericGeneratorTest.java

+/*
+ * 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.tabularexpressiontoolbox.expression;
+
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParser;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParser;
+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 java.util.Map;
+
+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 (= (* x 5.0) (/ 1.0 (- 4.0))) (or (and (> x (+ 8.0 3.0)) (< 9.0 (- x 2.0))) (or (>= x 12.0) (or (not (<= 34.0 (- x))) (> 5.0 4.0))))) (distinct x 5.0))",
+                        null,
+                        null},
+                {new CVC3Generator(),
+                        "((((x * 5) = (1 / (- 4))) OR (((x > (8 + 3)) AND (9 < (x - 2))) OR ((x >= 12) OR ((NOT (34 <= (- x))) OR (5 > 4))))) => (x /= 5))",
+                        "(((BVMULT(8,x,0bin00010100) = BVSDIV(0bin00000100,BVUMINUS(0bin00010000))) OR ((BVSGT(x,BVPLUS(8,0bin00100000,0bin00001100)) AND BVSLT(0bin00100100,BVSUB(x,0bin00001000))) OR (BVSGE(x,0bin00110000) OR ((NOT BVSLE(0bin10001000,BVUMINUS(x))) OR (5 > 4))))) => (x /= 0bin00010100))",
+                        "(((BVMULT(8,x,0bin00010100) = BVUDIV(0bin00000100,BVUMINUS(0bin00010000))) OR ((BVGT(x,BVPLUS(8,0bin00100000,0bin00001100)) AND BVLT(0bin00100100,BVSUB(x,0bin00001000))) OR (BVGE(x,0bin00110000) OR ((NOT BVLE(0bin10001000,BVUMINUS(x))) OR (5 > 4))))) => (x /= 0bin00010100))"
+                }
+        });
+    }
+
+    static private String query = "(x * 5) = (1 / -4) OR ((x > (8 + 3)) AND (9 < x - 2)) OR x >= 12 OR NOT (34 <= -x) OR (5 > 4) => (x /= 5)";
+    static private VariableType outputType = new BooleanVariableType();
+
+    @Parameter(value = 0)
+    public CheckerGenerator generator;
+
+    @Parameter(value = 1)
+    public String RealExpectedOutput;
+
+    @Parameter(value = 2)
+    public String SignedFixedPointExpectedOutput;
+
+    @Parameter(value = 3)
+    public String UnsignedFixedPointExpectedOutput;
+
+    @Test
+    public void RealTest() {
+        if (RealExpectedOutput != null) {
+            VariableCollection vars = variableParser.parseVariables("x");
+            Expression expr = PVSSimpleParser.parsePVSCode(vars, query);
+            assertEquals(RealExpectedOutput, expr.getCheckerOutput(generator, outputType));
+        }
+    }
+
+    @Test
+    public void SignedFixedPointTest() {
+        if (SignedFixedPointExpectedOutput != null) {
+            VariableCollection vars = variableParser.parseVariables("x:fixedt(1, 8, 2)");
+            Expression expr = PVSSimpleParser.parsePVSCode(vars, query);
+            assertEquals(SignedFixedPointExpectedOutput, expr.getCheckerOutput(generator, outputType));
+        }
+    }
+
+    @Test
+    public void UnsignedFixedPointTest() {
+        if (UnsignedFixedPointExpectedOutput != null) {
+            VariableCollection vars = variableParser.parseVariables("x:fixedt(0, 8, 2)");
+            Expression expr = PVSSimpleParser.parsePVSCode(vars, query);
+            assertEquals(UnsignedFixedPointExpectedOutput, expr.getCheckerOutput(generator, outputType));
+        }
+    }
+
+    VariableParser variableParser = new VariableParser();
+}

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/MatlabExpressionBinaryOperationTest.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+import static org.junit.Assert.*;
+import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.junit.runners.JUnit4;
+
+/**
+ *
+ * @author matthew
+ */
+@RunWith(JUnit4.class)
+public class MatlabExpressionBinaryOperationTest {
+    /**
+     * Test of type method, of class ExpressionBinaryOperation.
+     */
+    @Test
+    public void testWithSimpleRealVariablesAddedTogether() {
+        Variable l = new Variable("a", new RealVariableType()), r = new Variable("b", new RealVariableType());
+        ExpressionBinaryOperation instance = new ExpressionBinaryOperation(l, BinaryOperation.Addition, r);
+        
+        String CVC3Output = "(a + b)";
+        VariableType expressionType = new RealVariableType();
+        
+        assertEquals(CVC3Output, instance.getCheckerOutput(generator, expressionType));
+        assertEquals(expressionType, instance.actualOutputTypeForRequestedOutput(expressionType));
+    }
+    /**
+     * Test of type method, of class ExpressionBinaryOperation.
+     */
+    @Test
+    public void testWithSimpleFixedPointVariablesAddedTogether() {
+        Variable l = new Variable("a", new FixedPointVariableType(true, 17, 4)), r = new Variable("b", new FixedPointVariableType(true, 17, 4));
+        ExpressionBinaryOperation instance = new ExpressionBinaryOperation(l, BinaryOperation.Addition, r);
+        
+        String CVC3Output = "BVPLUS(17,a,b)";
+        VariableType expressionType = new FixedPointVariableType(true, 17, 4);
+        
+        assertEquals(CVC3Output, instance.getCheckerOutput(generator, expressionType));
+        assertEquals(expressionType, instance.actualOutputTypeForRequestedOutput(expressionType));
+    }
+    /**
+     * Test of setLHS/RHS, verify they set variables correctly.
+     */
+    @Test
+    public void testSettingsLHSAndRHS() {
+        Variable l = new Variable("a", new RealVariableType()), r = new Variable("b", new RealVariableType());
+        ExpressionBinaryOperation instance = new ExpressionBinaryOperation(l, BinaryOperation.Addition, r);
+        
+        //Reverse a+b to b+a.
+        instance.setLHS(r);
+        instance.setRHS(l);
+        
+        String CVC3Output = "(b + a)";
+        VariableType expressionType = new RealVariableType();
+
+        assertEquals(expressionType, instance.actualOutputTypeForRequestedOutput(expressionType));
+        assertEquals(CVC3Output, instance.getCheckerOutput(new CVC3Generator(), expressionType));
+    }
+    
+    /**
+     * Test when RHS/LHS have different castable types.
+     */
+    @Test
+    public void testCastableTypes() {
+        Literal lit = new Literal("5");
+        Variable var = new Variable("A", new RealVariableType());
+        VariableType exprType;
+        
+        // Test when adding a Real var to a lit, type always becomes Real.
+        exprType = new RealVariableType();
+        assertEquals(exprType, new ExpressionBinaryOperation(lit, BinaryOperation.Addition, var).actualOutputTypeForRequestedOutput(exprType));
+        assertEquals(exprType, new ExpressionBinaryOperation(var, BinaryOperation.Addition, lit).actualOutputTypeForRequestedOutput(exprType));
+
+        // Test when comparing a Real var to a lit, type always becomes boolean.
+        exprType = new BooleanVariableType();
+        assertEquals(exprType, new ExpressionBinaryOperation(lit, BinaryOperation.Equals, var).actualOutputTypeForRequestedOutput(exprType));
+        assertEquals(exprType, new ExpressionBinaryOperation(var, BinaryOperation.Equals, lit).actualOutputTypeForRequestedOutput(exprType));
+    }
+
+    /**
+     * Test operations changing types (== doing REAL+REAL -> BOOLEAN)
+     */
+    @Test
+    public void testCastingOperations() {
+        Literal l = new Literal("5"), r = new Literal("6");
+        ExpressionBinaryOperation exp = new ExpressionBinaryOperation(l, BinaryOperation.Equals, r);
+
+        // Test when adding a Real var to a lit, type always becomes Real.
+        VariableType expressionType = new BooleanVariableType();
+        assertEquals(expressionType, exp.actualOutputTypeForRequestedOutput(expressionType));
+        assertEquals("(5 = 6)", exp.getCheckerOutput(generator, expressionType));
+    }
+
+    /**
+     * Test operations fails when a requested type is invalid!
+     */
+    @Test(expected=IllegalArgumentException.class)
+    public void testInvalidOutputType() {
+        Literal l = new Literal("5"), r = new Literal("6");
+        ExpressionBinaryOperation exp = new ExpressionBinaryOperation(l, BinaryOperation.Equals, r);
+
+        exp.getCheckerOutput(generator, new RealVariableType()); //Returns a boolean, so will fail.
+    }
+
+    /**
+     * Test doing multiple boolean operations AND'd together.
+     */
+    @Test
+    public void testBooleanAndFromComparision() {
+        Expression l = new Variable("a", new RealVariableType()), r = new Literal("6"),
+                      l2 = new Variable("b", new RealVariableType()), r2 = new Literal("8");
+        ExpressionBinaryOperation exp = new ExpressionBinaryOperation(new ExpressionBinaryOperation(l, BinaryOperation.Equals, r),
+                BinaryOperation.BooleanAnd,
+                new ExpressionBinaryOperation(l2, BinaryOperation.Equals, r2));
+
+        // Test when adding a Real var to a lit, type always becomes Real.
+        VariableType expressionType = new BooleanVariableType();
+        assertEquals(expressionType, exp.actualOutputTypeForRequestedOutput(expressionType));
+        assertEquals("((a = 6) AND (b = 8))", exp.getCheckerOutput(generator, expressionType));
+    }
+
+    CheckerGenerator generator = new CVC3Generator();
+}

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/VariableTest.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+import static org.hamcrest.CoreMatchers.is;
+import static org.junit.Assert.*;
+
+import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.junit.runners.JUnit4;
+
+import java.util.HashMap;
+import java.util.Map;
+
+/**
+ *
+ * @author matthew
+ */
+@RunWith(JUnit4.class)
+public class VariableTest {
+    @Test
+    public void exerciseVariable() {
+        String name = "Var";
+        VariableType type = new RealVariableType();
+        
+        Variable var = new Variable(name, type);
+        
+        assertSame(name, var.name());
+        assertSame(type, var.type());
+        assertEquals(name, var.getCheckerOutput(null, new RealVariableType()));
+
+        Map<String, Variable> varList = new HashMap<String, Variable>();
+        varList.put(name, var);
+        VariableCollection variableCollection = new VariableCollection(varList);
+
+        CheckerGenerator generator = new CVC3Generator();
+        assertEquals(name+":REAL;\n", generator.GenerateVariablesDeclaration(variableCollection));
+
+        generator = new SMTLIBGenerator();
+        assertEquals("(declare-fun " +name+ " () Real)\n", generator.GenerateVariablesDeclaration(variableCollection));
+    }
+
+    @Test
+    public void testSubtypePredicate() {
+        // Construct a basic variable.  Assume it is correct due to the above test.
+        Variable var = new Variable("var", new RealVariableType());
+
+        // Next create a subtype predicate.  For now, make it work over positive reals (excluding 0)
+        Expression predicate = new ExpressionBinaryOperation(var, BinaryOperation.GreaterThen, new Literal("0"));
+        var.type().setSubtypePredicate(predicate);
+
+        // Verify the predicate took.
+        assertThat(var.type().subtypePredicate(), is(predicate));
+
+        // Make a variable list for the generators.
+        Map<String, Variable> varList = new HashMap<String, Variable>();
+        varList.put("var", var);
+        VariableCollection variableCollection = new VariableCollection(varList);
+
+        CheckerGenerator generator = new CVC3Generator();
+        String varDecl = generator.GenerateVariablesDeclaration(variableCollection);
+
+        assertThat(varDecl, is("var:REAL;\nASSERT (var > 0);\n"));
+
+        generator = new SMTLIBGenerator();
+        varDecl = generator.GenerateVariablesDeclaration(variableCollection);
+
+        assertThat(varDecl, is("(declare-fun var () Real)\n(assert (> var 0.0))\n"));
+    }
+
+    // Verify handling of invalid type to getCheckerOutput
+    @Test(expected=IllegalArgumentException.class)
+    public void testInvalidOutputType() {
+        String name = "Var";
+        VariableType type = new BooleanVariableType();
+
+        Variable var = new Variable(name, type);
+
+        var.getCheckerOutput(null, new RealVariableType()); //Returns a boolean, so will fail.
+    }
+}

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/test/AppTest.java

+package ca.mcmaster.cas.tabularexpressiontoolbox.expression.test;
+
+import junit.framework.Test;
+import junit.framework.TestCase;
+import junit.framework.TestSuite;
+
+/**
+ * Unit test for simple App.
+ */
+public class AppTest 
+    extends TestCase
+{
+    /**
+     * Create the test case
+     *
+     * @param testName name of the test case
+     */
+    public AppTest( String testName )
+    {
+        super( testName );
+    }
+
+    /**
+     * @return the suite of tests being tested
+     */
+    public static Test suite()
+    {
+        return new TestSuite( AppTest.class );
+    }
+
+    /**
+     * Rigourous Test :-)
+     */
+    public void testApp()
+    {
+        assertTrue( true );
+    }
+
+    /**
+     * Rigourous Test :-)
+     */
+    public void testAppFail()
+    {
+        assertFalse( false );
+    }
+}

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/test/BooleanVariableTypeTest.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression.test;
+
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BooleanVariableType;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CVC3Generator;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.RealVariableType;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.SMTLIBGenerator;
+import org.junit.Test;
+import static org.junit.Assert.*;
+import org.junit.runner.RunWith;
+import org.junit.runners.JUnit4;
+
+/**
+ *
+ * @author matthew
+ */
+@RunWith(JUnit4.class)
+public class BooleanVariableTypeTest {
+
+    /**
+     * Test of getCVC3Definition method, of class RealVariableType.
+     */
+    @Test
+    public void testGetCVC3Definition() {
+        CVC3Generator generator = new CVC3Generator();
+        String variableName = "test_variable";
+        BooleanVariableType instance = new BooleanVariableType();
+        String expResult = "BOOLEAN";
+        String result = generator.GenerateVariableType(instance);
+        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.
+     */
+    @Test
+    public void testEquals() {
+        BooleanVariableType test = new BooleanVariableType();
+        assertTrue(test.equals(new BooleanVariableType()));
+        assertTrue(test.equals(test));
+        assertFalse(test.equals(new Object()));
+    }
+
+    /**
+     * Test of hashCode method, of class RealVariableType.
+     */
+    @Test
+    public void testHashCode() {
+        BooleanVariableType instance = new BooleanVariableType();
+        assertEquals(0, instance.hashCode());
+    }
+
+    /**
+     * Test of canCastToType method, of class RealVariableType.  Reals (for now)
+     * don't cast.
+     */
+    @Test
+    public void testCanCastToType() {
+        BooleanVariableType instance = new BooleanVariableType();
+        assertFalse(instance.canCastToType(new RealVariableType()));
+        assertFalse(instance.canCastToType(new BooleanVariableType()));
+    }
+}

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/test/MatlabLiteralTest.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression.test;
+
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CVC3Generator;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CheckerGenerator;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.FixedPointVariableType;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Literal;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.RealVariableType;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableType;
+import org.junit.Test;
+import static org.junit.Assert.*;
+import org.junit.runner.RunWith;
+import org.junit.runners.JUnit4;
+
+/**
+ *
+ * @author matthew
+ */
+@RunWith(JUnit4.class)
+public class MatlabLiteralTest {
+    /**
+     * Test of canHandleOutputType method, of class Literal.
+     */
+    @Test
+    public void testType() {
+        Literal instance = new Literal(null);
+        VariableType exprType = new RealVariableType();
+        assertEquals(exprType, instance.actualOutputTypeForRequestedOutput(exprType));
+    }
+
+    /**
+     * Test of getCVC3Output method, of class Literal.  Test only natural numbers;
+     */
+    @Test
+    public void testGetCVC3Output() {
+        Literal instance = new Literal("5");
+        assertEquals("5", instance.getCheckerOutput(generator, new RealVariableType()));
+        assertEquals("0bin00101", instance.getCheckerOutput(generator, new FixedPointVariableType(true, 5, 0)));
+        assertEquals("0bin01010", instance.getCheckerOutput(generator, new FixedPointVariableType(true, 5, 1)));
+    }
+
+    /**
+     * Test of getCVC3Output method, of class Literal.  Test fun fixed point number;
+     */
+    @Test
+    public void testCVC3OutputOnInterestingFixedPoint() {
+        Literal instance = new Literal("0");
+        assertEquals("0bin00000", instance.getCheckerOutput(generator, new FixedPointVariableType(true, 5, 1)));
+        
+        instance = new Literal("5.5");
+        assertEquals("0bin01011", instance.getCheckerOutput(generator, new FixedPointVariableType(true, 5, 1)));
+        
+        instance = new Literal("-5.5");
+        assertEquals("0bin10101", instance.getCheckerOutput(generator, new FixedPointVariableType(true, 5, 1)));
+        
+        instance = new Literal("-5");
+        assertEquals("0bin11011", instance.getCheckerOutput(generator, new FixedPointVariableType(true, 5, 0)));
+    }
+    CheckerGenerator generator = new CVC3Generator();
+}

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/test/RealVariableTypeTest.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression.test;
+
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BooleanVariableType;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CVC3Generator;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.RealVariableType;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.SMTLIBGenerator;
+import org.junit.Test;
+import static org.junit.Assert.*;
+import org.junit.runner.RunWith;
+import org.junit.runners.JUnit4;
+
+/**
+ *
+ * @author matthew
+ */
+@RunWith(JUnit4.class)
+public class RealVariableTypeTest {
+
+    /**
+     * Test of getCVC3Definition method, of class RealVariableType.
+     */
+    @Test
+    public void testGetCVC3Definition() {
+        CVC3Generator generator = new CVC3Generator();
+        String variableName = "test_variable";
+        RealVariableType instance = new RealVariableType();
+        String expResult = "REAL";
+        String result = generator.GenerateVariableType(instance);
+        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.
+     */
+    @Test
+    public void testEquals() {
+        RealVariableType test = new RealVariableType();
+        assertTrue(test.equals(new RealVariableType()));
+        assertTrue(test.equals(test));
+        assertFalse(test.equals(new Object()));
+    }
+
+    /**
+     * Test of hashCode method, of class RealVariableType.
+     */
+    @Test
+    public void testHashCode() {
+        RealVariableType instance = new RealVariableType();
+        assertEquals(0, instance.hashCode());
+    }
+
+    /**
+     * Test of canCastToType method, of class RealVariableType.  Reals (for now)
+     * don't cast.
+     */
+    @Test
+    public void testCanCastToType() {
+        RealVariableType instance = new RealVariableType();
+        assertFalse(instance.canCastToType(new RealVariableType()));
+        assertFalse(instance.canCastToType(new BooleanVariableType()));
+    }
+}

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/test/MatlabParserTest.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.parsers.test;
+
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BooleanVariableType;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CVC3Generator;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CheckerGenerator;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Expression;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Literal;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableCollection;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParser;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.RealVariableType;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.SMTLIBGenerator;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Variable;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParser;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableType;
+import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.junit.runners.JUnit4;
+import static org.junit.Assert.*;
+
+/**
+ *
+ * @author matthew
+ */
+@RunWith(JUnit4.class)
+public class MatlabParserTest {
+    @Test
+    public void testSimpleNumberParse() {
+        Expression expr = MatlabParser.parseMatlabCode(new VariableCollection(null), "5\n");
+        VariableType variableType = new RealVariableType();
+
+        assertSame(Literal.class, expr.getClass());
+        CheckerGenerator generator = new CVC3Generator();
+        assertEquals("5", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("5.0", expr.getCheckerOutput(generator, variableType));
+    }
+
+    @Test
+    public void testSimpleRealVariableParse() {
+        Expression expr = MatlabParser.parseMatlabCode(variableParser.parseVariables("a"), "a\n");
+
+        assertSame(Variable.class, expr.getClass());
+        CheckerGenerator generator = new CVC3Generator();
+        VariableType variableType = new RealVariableType();
+        assertEquals("a", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("a", expr.getCheckerOutput(generator, variableType));
+    }
+
+    @Test
+    public void testSimpleAdditionWithLiterals() {
+        Expression expr = MatlabParser.parseMatlabCode(new VariableCollection(null), "4+5\n");
+
+        CheckerGenerator generator = new CVC3Generator();
+        VariableType variableType = new RealVariableType();
+        assertEquals("(4 + 5)", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("(+ 4.0 5.0)", expr.getCheckerOutput(generator, variableType));
+    }
+
+    @Test
+    public void testSimpleMultiplicationWithLiterals() {
+        Expression expr = MatlabParser.parseMatlabCode(new VariableCollection(null), "4*5\n");
+
+        VariableType variableType = new RealVariableType();
+        CheckerGenerator generator = new CVC3Generator();
+        assertEquals("(4 * 5)", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("(* 4.0 5.0)", expr.getCheckerOutput(generator, variableType));
+    }
+
+    @Test
+    public void testSimpleNegationWithLiterals() {
+        Expression expr = MatlabParser.parseMatlabCode(new VariableCollection(null), "~0\n");
+
+        VariableType variableType = new RealVariableType();
+        CheckerGenerator generator = new CVC3Generator();
+        assertEquals("(NOT 0)", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("(not 0.0)", expr.getCheckerOutput(generator, variableType));
+    }
+
+    @Test
+    public void testDoubleAdditionWithLiterals() {
+        Expression expr = MatlabParser.parseMatlabCode(new VariableCollection(null), "4+5+6\n");
+
+        VariableType variableType = new RealVariableType();
+        CheckerGenerator generator = new CVC3Generator();
+        assertEquals("((4 + 5) + 6)", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("(+ (+ 4.0 5.0) 6.0)", expr.getCheckerOutput(generator, variableType));
+    }
+
+    @Test
+    public void testMultiplyThenAddWithLiterals() {
+        Expression expr = MatlabParser.parseMatlabCode(new VariableCollection(null), "4*5+6\n");
+
+        VariableType variableType = new RealVariableType();
+        CheckerGenerator generator = new CVC3Generator();
+        assertEquals("((4 * 5) + 6)", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("(+ (* 4.0 5.0) 6.0)", expr.getCheckerOutput(generator, variableType));
+    }
+
+    @Test
+    public void testAddThenMultiplyWithLiterals() {
+        Expression expr = MatlabParser.parseMatlabCode(new VariableCollection(null), "4+5*6\n");
+
+        VariableType variableType = new RealVariableType();
+        CheckerGenerator generator = new CVC3Generator();
+        assertEquals("(4 + (5 * 6))", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("(+ 4.0 (* 5.0 6.0))", expr.getCheckerOutput(generator, variableType));
+    }
+
+    @Test
+    public void testInsanseExpressionsWithLiterals() {
+        Expression expr = MatlabParser.parseMatlabCode(new VariableCollection(null), "4*5+6*7\n");
+        Expression expr2 = MatlabParser.parseMatlabCode(new VariableCollection(null), "4+5+6*7*8\n");
+
+        CheckerGenerator cvc3generator = new CVC3Generator();
+        CheckerGenerator smtlibgenerator = new SMTLIBGenerator();
+
+        VariableType variableType = new RealVariableType();
+        assertEquals("((4 * 5) + (6 * 7))", expr.getCheckerOutput(cvc3generator, variableType));
+        assertEquals("(+ (* 4.0 5.0) (* 6.0 7.0))", expr.getCheckerOutput(smtlibgenerator, variableType));
+
+        assertEquals("((4 + 5) + ((6 * 7) * 8))", expr2.getCheckerOutput(cvc3generator, variableType));
+        assertEquals("(+ (+ 4.0 5.0) (* (* 6.0 7.0) 8.0))", expr2.getCheckerOutput(smtlibgenerator, variableType));
+    }
+
+    @Test
+    public void testSimpleConditionalsWithLiterals() {
+        Expression expr = MatlabParser.parseMatlabCode(new VariableCollection(null), "5 > 5\n");
+
+        VariableType variableType = new BooleanVariableType();
+        CheckerGenerator generator = new CVC3Generator();
+        assertEquals("(5 > 5)", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("(> 5.0 5.0)", expr.getCheckerOutput(generator, variableType));
+    }
+
+    @Test
+    public void testInsanseExpressionsWithLiteralsAndVariables() {
+        Expression expr = MatlabParser.parseMatlabCode(variableParser.parseVariables("x,z,y"), "z == 1 && x == 0 && y == 2");
+
+        VariableType variableType = new BooleanVariableType();
+        assertEquals(variableType, expr.actualOutputTypeForRequestedOutput(variableType));
+        CheckerGenerator generator = new CVC3Generator();
+        assertEquals("(((z = 1) AND (x = 0)) AND (y = 2))", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("(and (and (= z 1.0) (= x 0.0)) (= y 2.0))", expr.getCheckerOutput(generator, variableType));
+    }
+
+    VariableParser variableParser = new VariableParser();
+}

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/test/PVSSimpleParserTest.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.parsers.test;
+
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BooleanVariableType;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CVC3Generator;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CheckerGenerator;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Expression;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Literal;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.RealVariableType;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.SMTLIBGenerator;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Variable;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableCollection;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableType;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParser;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParser;
+import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.junit.runners.JUnit4;
+
+import static org.junit.Assert.assertEquals;
+import static org.junit.Assert.assertSame;
+
+/**
+ *
+ * @author matthew
+ */
+@RunWith(JUnit4.class)
+public class PVSSimpleParserTest {
+    @Test
+    public void testSimpleNumberParse() {
+        Expression expr = PVSSimpleParser.parsePVSCode(new VariableCollection(null), "5\n");
+        VariableType variableType = new RealVariableType();
+
+        assertSame(Literal.class, expr.getClass());
+        CheckerGenerator generator = new CVC3Generator();
+        assertEquals("5", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("5.0", expr.getCheckerOutput(generator, variableType));
+    }
+
+    @Test
+    public void testSimpleRealVariableParse() {
+        Expression expr = PVSSimpleParser.parsePVSCode(variableParser.parseVariables("a"), "a\n");
+
+        assertSame(Variable.class, expr.getClass());
+        CheckerGenerator generator = new CVC3Generator();
+        VariableType variableType = new RealVariableType();
+        assertEquals("a", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("a", expr.getCheckerOutput(generator, variableType));
+    }
+
+    @Test
+    public void testSimpleAdditionWithLiterals() {
+        Expression expr = PVSSimpleParser.parsePVSCode(new VariableCollection(null), "4+5\n");
+
+        CheckerGenerator generator = new CVC3Generator();
+        VariableType variableType = new RealVariableType();
+        assertEquals("(4 + 5)", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("(+ 4.0 5.0)", expr.getCheckerOutput(generator, variableType));
+    }
+
+    @Test
+    public void testSimpleMultiplicationWithLiterals() {
+        Expression expr = PVSSimpleParser.parsePVSCode(new VariableCollection(null), "4*5\n");
+
+        VariableType variableType = new RealVariableType();
+        CheckerGenerator generator = new CVC3Generator();
+        assertEquals("(4 * 5)", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("(* 4.0 5.0)", expr.getCheckerOutput(generator, variableType));
+    }
+
+    @Test
+    public void testSimpleNegationWithLiterals() {
+        Expression expr = PVSSimpleParser.parsePVSCode(new VariableCollection(null), "NOT 0\n");
+
+        VariableType variableType = new RealVariableType();
+        CheckerGenerator generator = new CVC3Generator();
+        assertEquals("(NOT 0)", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("(not 0.0)", expr.getCheckerOutput(generator, variableType));
+    }
+
+    @Test
+    public void testDoubleAdditionWithLiterals() {
+        Expression expr = PVSSimpleParser.parsePVSCode(new VariableCollection(null), "4+5+6\n");
+
+        VariableType variableType = new RealVariableType();
+        CheckerGenerator generator = new CVC3Generator();
+        assertEquals("((4 + 5) + 6)", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("(+ (+ 4.0 5.0) 6.0)", expr.getCheckerOutput(generator, variableType));
+    }
+
+    @Test
+    public void testMultiplyThenAddWithLiterals() {
+        Expression expr = PVSSimpleParser.parsePVSCode(new VariableCollection(null), "4*5+6\n");
+
+        VariableType variableType = new RealVariableType();
+        CheckerGenerator generator = new CVC3Generator();
+        assertEquals("((4 * 5) + 6)", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("(+ (* 4.0 5.0) 6.0)", expr.getCheckerOutput(generator, variableType));
+    }
+
+    @Test
+    public void testAddThenMultiplyWithLiterals() {
+        Expression expr = PVSSimpleParser.parsePVSCode(new VariableCollection(null), "4+5*6\n");
+
+        VariableType variableType = new RealVariableType();
+        CheckerGenerator generator = new CVC3Generator();
+        assertEquals("(4 + (5 * 6))", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("(+ 4.0 (* 5.0 6.0))", expr.getCheckerOutput(generator, variableType));
+    }
+
+    @Test
+    public void testInsanseExpressionsWithLiterals() {
+        Expression expr = PVSSimpleParser.parsePVSCode(new VariableCollection(null), "4*5+6*7\n");
+        Expression expr2 = PVSSimpleParser.parsePVSCode(new VariableCollection(null), "4+5+6*7*8\n");
+
+        CheckerGenerator cvc3generator = new CVC3Generator();
+        CheckerGenerator smtlibgenerator = new SMTLIBGenerator();
+
+        VariableType variableType = new RealVariableType();
+        assertEquals("((4 * 5) + (6 * 7))", expr.getCheckerOutput(cvc3generator, variableType));
+        assertEquals("(+ (* 4.0 5.0) (* 6.0 7.0))", expr.getCheckerOutput(smtlibgenerator, variableType));
+
+        assertEquals("((4 + 5) + ((6 * 7) * 8))", expr2.getCheckerOutput(cvc3generator, variableType));
+        assertEquals("(+ (+ 4.0 5.0) (* (* 6.0 7.0) 8.0))", expr2.getCheckerOutput(smtlibgenerator, variableType));
+    }
+
+    @Test
+    public void testSimpleConditionalsWithLiterals() {
+        Expression expr = PVSSimpleParser.parsePVSCode(new VariableCollection(null), "5 > 5\n");
+
+        VariableType variableType = new BooleanVariableType();
+        CheckerGenerator generator = new CVC3Generator();
+        assertEquals("(5 > 5)", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("(> 5.0 5.0)", expr.getCheckerOutput(generator, variableType));
+    }
+
+    @Test
+    public void testInsanseExpressionsWithLiteralsAndVariables() {
+        Expression expr = PVSSimpleParser.parsePVSCode(variableParser.parseVariables("x,z,y"), "z = 1 AND x = 0 AND y = 2");
+
+        VariableType variableType = new BooleanVariableType();
+        assertEquals(variableType, expr.actualOutputTypeForRequestedOutput(variableType));
+        CheckerGenerator generator = new CVC3Generator();
+        assertEquals("((z = 1) AND ((x = 0) AND (y = 2)))", expr.getCheckerOutput(generator, variableType));
+        generator = new SMTLIBGenerator();
+        assertEquals("(and (= z 1.0) (and (= x 0.0) (= y 2.0)))", expr.getCheckerOutput(generator, variableType));
+    }
+
+    VariableParser variableParser = new VariableParser();
+}

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/test/ParserOperatorParseTest.java

+/*
+ * 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.tabularexpressiontoolbox.parsers.test;
+
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BinaryOperation;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionBinaryOperation;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionUnaryOperation;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.UnaryOperation;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableCollection;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParser;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParser;
+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.lang.reflect.InvocationTargetException;
+import java.lang.reflect.Method;
+import java.util.Arrays;
+import java.util.Collection;
+import java.util.Map;
+
+import static org.hamcrest.CoreMatchers.is;
+import static org.junit.Assert.assertThat;
+
+/** This test simply tests that each operator parses correctly.
+ *
+ * This is a simply parametrized test set that only deals only with testing the individual operators.  It avoids
+ * all the other details (it just uses literals for input).  It also avoids any dependency on generators.
+ *
+ * @author Matthew Dawson <matthew@mjdsystems.ca>
+ */
+@RunWith(Parameterized.class)
+public class ParserOperatorParseTest {
+    @Parameters
+    public static Collection<Object[]> data() {
+        return Arrays.asList(new Object[][]{
+                {"+",  "+",   BinaryOperation.Addition,         null},
+                {"-",  "-",   BinaryOperation.Minus,            null},
+                {"*",  "*",   BinaryOperation.Multiplication,   null},
+                {"/",  "/",   BinaryOperation.Division,         null},
+                {"^",  "^",   BinaryOperation.Exponentiation,   null},
+                {">",  ">",   BinaryOperation.GreaterThen,      null},
+                {">=", ">=",  BinaryOperation.GreaterThenEqual, null},
+                {"<",  "<",   BinaryOperation.LessThen,         null},
+                {"<=", "<=",  BinaryOperation.LessThenEqual,    null},
+                {"==", "=",   BinaryOperation.Equals,           null},
+                {"~=", "/=",  BinaryOperation.NotEquals,        null},
+                {null, "=>",  BinaryOperation.Implies,          null},
+                {"&&", "AND", BinaryOperation.BooleanAnd,       null},
+                {"||", "OR",  BinaryOperation.BooleanOr,        null},
+                {"~",  "NOT", null,                             UnaryOperation.Negation},
+                {"-",  "-",   null,                             UnaryOperation.Minus}
+        });
+    }
+    @Parameter
+    public String matlabInputSymbol;
+
+    @Parameter(value = 1)
+    public String pvsInputSymbol;
+
+    @Parameter(value = 2)
+    public BinaryOperation bop;
+
+    @Parameter(value = 3)
+    public UnaryOperation uop;
+
+    private void doTest(String expr, Method method) throws InvocationTargetException, IllegalAccessException {
+        if (expr == null) {
+            // No symbol for this parser.  Thus skip this test.
+            return ;
+        }
+        if (bop != null) {
+            // Binary op to test ...
+            ExpressionBinaryOperation exp = (ExpressionBinaryOperation)method.invoke(null, fakeVariableCollection, "1 " + expr + " 2\n");
+
+            assertThat(exp.toString(), is("(1 " + bop.toString() + " 2)"));
+        } else {
+            // Unary op to test ...
+            ExpressionUnaryOperation exp = (ExpressionUnaryOperation)method.invoke(null, fakeVariableCollection, expr + " 3\n");
+
+            assertThat(exp.toString(), is("( " + uop.toString() + " 3)"));
+        }
+    }
+
+    @Test
+    public void testMatlabParser() throws NoSuchMethodException, InvocationTargetException, IllegalAccessException {
+        doTest(matlabInputSymbol, MatlabParser.class.getMethod("parseMatlabCode", VariableCollection.class, String.class));
+    }
+
+    @Test
+    public void testPVSSimpleParser() throws NoSuchMethodException, InvocationTargetException, IllegalAccessException {
+        doTest(pvsInputSymbol, PVSSimpleParser.class.getMethod("parsePVSCode", VariableCollection.class, String.class));
+    }
+
+    private VariableCollection fakeVariableCollection = new VariableCollection(null);
+}

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/test/VariableParserTest.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.parsers.test;
+
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BooleanVariableType;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CVC3Generator;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CheckerGenerator;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.FixedPointVariableType;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.RealVariableType;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Variable;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableCollection;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableType;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParser;
+
+import static org.hamcrest.CoreMatchers.*;
+import static org.junit.Assert.*;
+
+import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.junit.runners.JUnit4;
+
+import java.util.Map;
+
+
+/**
+ *
+ * @author matthew
+ */
+@RunWith(JUnit4.class)
+public class VariableParserTest {
+    @Test
+    public void testSimpleVariable() {
+        VariableParser variableParser = new VariableParser();
+        VariableCollection variableCollection = variableParser.parseVariables("a");
+        Map<String, Variable> vars = variableCollection.getVariables();
+        Variable a = vars.get("a");
+        assertEquals("a", a.name());
+        assertEquals(new RealVariableType(), a.type());
+        assertThat(vars, is(variableCollection.getVariablesAndEnumeratedValues()));
+    }
+    @Test
+    public void testRealVariable() {
+        VariableParser variableParser = new VariableParser();
+        VariableCollection variableCollection = variableParser.parseVariables("a: real");
+        Map<String, Variable> vars = variableCollection.getVariables();
+        Variable a = vars.get("a");
+        assertEquals("a", a.name());
+        assertEquals(new RealVariableType(), a.type());
+    }
+    @Test
+    public void testBooleanVariable() {
+        VariableParser variableParser = new VariableParser();
+        VariableCollection variableCollection = variableParser.parseVariables("a: bool");
+        Map<String, Variable> vars = variableCollection.getVariables();
+        Variable a = vars.get("a");
+        assertEquals("a", a.name());
+        assertEquals(new BooleanVariableType(), a.type());
+    }
+    @Test
+    public void testFixedPointNoDecimalVariable() {
+        VariableParser variableParser = new VariableParser();
+        VariableCollection variableCollection = variableParser.parseVariables("a: fixedt(1, 16)");
+        Map<String, Variable> vars = variableCollection.getVariables();
+        Variable a = vars.get("a");
+        FixedPointVariableType type = (FixedPointVariableType)a.type();
+        assertEquals("a", a.name());
+        assertNotNull(type);
+        assertEquals(true, type.isSigned());
+        assertEquals(16, type.digits());
+        assertEquals(0, type.fractionPart());
+
+        vars = variableParser.parseVariables("a: fixedt(0, 15, 4)").getVariables();
+        a = vars.get("a");
+        type = (FixedPointVariableType)a.type();
+        assertEquals("a", a.name());
+        assertNotNull(type);
+        assertEquals(false, type.isSigned());
+        assertEquals(15, type.digits());
+        assertEquals(4, type.fractionPart());
+    }
+    @Test
+    public void testCaseInsensitivtySearch() {
+        VariableParser variableParser = new VariableParser();
+        VariableCollection variableCollection = variableParser.parseVariables("a: ReAl");
+        Map<String, Variable> vars = variableCollection.getVariables();
+        Variable a = vars.get("a");
+        assertEquals("a", a.name());
+        assertEquals(new RealVariableType(), a.type());
+
+        vars = variableParser.parseVariables("A: REAL").getVariables();
+        a = vars.get("A");
+        assertEquals("A", a.name());
+        assertEquals(new RealVariableType(), a.type());
+    }
+    @Test
+    public void testMultiVariableOutput() {
+        VariableParser variableParser = new VariableParser();
+        VariableCollection variableCollection = variableParser.parseVariables("a,b");
+        try {
+            assertEquals("a:REAL;\nb:REAL\n;", generator.GenerateVariablesDeclaration(variableCollection));
+        } catch(AssertionError e) {
+            //Depending upon maps sort order, either a or be may be first.  Either is correct, so if the first test fails, retry with order reversed.
+            assertEquals("b:REAL;\na:REAL;\n", generator.GenerateVariablesDeclaration(variableCollection));
+        }
+
+        variableCollection = variableParser.parseVariables("a:fixedt(1,16,9),b");
+        try {
+            assertEquals("a:BITVECTOR(16);\nb:REAL\n;", generator.GenerateVariablesDeclaration(variableCollection));
+        } catch(AssertionError e) {
+            //Depending upon maps sort order, either a or be may be first.  Either is correct, so if the first test fails, retry with order reversed.
+            assertEquals("b:REAL;\na:BITVECTOR(16);\n", generator.GenerateVariablesDeclaration(variableCollection));
+        }
+    }
+    @Test
+    public void testSubtypeTypeExtraction() {
+        VariableParser variableParser = new VariableParser();
+        VariableCollection variableCollection = variableParser.parseVariables("d:{y|c OR y > 5},a,b:{x:real|x>5},c:bool,z:{x:bool|x /= c}");
+        Map<String, Variable> vars = variableCollection.getVariables();
+        assertThat(vars.size(), is(5));
+
+        assertThat(vars.get("d").name(), is("d"));
+        assertThat(vars.get("d").type(), is((VariableType) new RealVariableType()));
+        assertThat(vars.get("d").type().subtypePredicate().toString(), is("(c BooleanOr (d GreaterThen 5))"));
+
+        assertThat(vars.get("a").name(), is("a"));
+        assertThat(vars.get("a").type(), is((VariableType) new RealVariableType()));
+        assertThat(vars.get("a").type().subtypePredicate(), is((Object)null));
+
+        assertThat(vars.get("b").name(), is("b"));
+        assertThat(vars.get("b").type(), is((VariableType) new RealVariableType()));
+        assertThat(vars.get("b").type().subtypePredicate().toString(), is("(b GreaterThen 5)"));
+
+        assertThat(vars.get("c").name(), is("c"));
+        assertThat(vars.get("c").type(), is((VariableType) new BooleanVariableType()));
+        assertThat(vars.get("c").type().subtypePredicate(), is((Object)null));
+
+        assertThat(vars.get("z").name(), is("z"));
+        assertThat(vars.get("z").type(), is((VariableType) new BooleanVariableType()));
+        assertThat(vars.get("z").type().subtypePredicate().toString(), is("(z NotEquals c)"));
+    }
+
+    @Test
+    public void testCustomType() {
+        VariableParser variableParser = new VariableParser();
+        variableParser.addCustomType("myreal", new RealVariableType());
+        BooleanVariableType customBool = new BooleanVariableType();
+        customBool.setSubtypePredicate(new Variable("c", new BooleanVariableType()));
+        variableParser.addCustomType("mybool", customBool);
+
+        Map<String, Variable> vars = variableParser.parseVariables("a:myreal,b:mybool").getVariables();
+        assertThat(vars.size(), is(2));
+
+        assertThat(vars.get("a").name(), is("a"));
+        assertThat(vars.get("a").type(), is((VariableType) new RealVariableType()));
+
+        assertThat(vars.get("b").name(), is("b"));
+        assertThat(vars.get("b").type(), is((VariableType) new BooleanVariableType()));
+        assertThat(vars.get("b").type().subtypePredicate().toString(), is("c"));
+    }
+
+    @Test
+    public void testUnknownCustomType() {
+        VariableParser variableParser = new VariableParser();
+
+        Map<String, Variable> vars = variableParser.parseVariables("a:unknowntype").getVariables();
+        assertThat(vars.size(), is(1));
+
+        assertThat(vars.get("a").name(), is("a"));
+        assertThat(vars.get("a").type(), is((VariableType) new RealVariableType()));
+    }
+
+    CheckerGenerator generator = new CVC3Generator();
+}

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/smtlibchecker/CheckerRunnerResultTest.java

+/*
+ * 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.tabularexpressiontoolbox.smtlibchecker;
+
+import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.junit.runners.JUnit4;
+
+import java.util.HashMap;
+
+import static org.junit.Assert.*;
+
+/**
+ * @author Matthew Dawson <matthew@mjdsystems.ca>
+ */
+@RunWith(JUnit4.class)
+public class CheckerRunnerResultTest {
+    @Test
+    public void TestGenerateMatlabVariableDeclarations() {
+        CheckerRunnerResult instance = new CheckerRunnerResult();
+
+        instance.SampleValues = new HashMap<String, String>();
+        instance.SampleValues.put("x", "5.0");
+        instance.SampleValues.put("z", "STRCONST");
+
+        try {
+            assertEquals("x = 5.0;\nz = STRCONST;\n", instance.GenerateMatlabVariableDeclarations());
+        } catch(AssertionError e) {
+            assertEquals("z = STRCONST;\nx = 5.0;\n", instance.GenerateMatlabVariableDeclarations());
+        }
+    }
+}

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/smtlibchecker/CheckerRunnerTest.java

+/*
+ * 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.tabularexpressiontoolbox.smtlibchecker;
+
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParser;
+import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchicalCell;
+import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchicalGrid;
+import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.junit.runners.JUnit4;
+
+import java.util.List;
+
+import static org.junit.Assert.*;
+
+/**
+ * @author Matthew Dawson <matthew@mjdsystems.ca>
+ */
+@RunWith(JUnit4.class)
+public class CheckerRunnerTest {
+    @Test
+    public void TestRunningZ3() {
+        HierarchicalGrid grid = new HierarchicalGrid();
+        List<HierarchicalCell> topCells = grid.getSubHiearchy();
+
+        topCells.add(new HierarchicalCell("x > 0"));
+        topCells.add(new HierarchicalCell("x == 0"));
+        topCells.add(new HierarchicalCell("0 > x"));
+
+        List<HierarchicalCell> nextGrid = topCells.get(1).getSubHiearchy();
+        nextGrid.add(new HierarchicalCell("z > 0"));
+        nextGrid.add(new HierarchicalCell("z == 1"));
+        nextGrid.add(new HierarchicalCell("0 > z"));
+
+        //nextGrid.get(1).getSubHiearchy().add(new HierarchicalCell("z == 0"));
+
+        List<CheckerRunnerResult> res = CheckerRunner.RunZ3(grid, variableParser.parseVariables("x,z"));
+        assertEquals(2, res.size());
+        assertEquals(2, res.get(0).SampleValues.size());
+        assertEquals("0.0", res.get(0).SampleValues.get("x"));
+        assertEquals("1.0", res.get(0).SampleValues.get("z"));
+
+        assertEquals(2, res.get(1).SampleValues.size());
+        assertEquals("0.0", res.get(1).SampleValues.get("x"));
+        assertEquals("0.0", res.get(1).SampleValues.get("z"));
+    }
+    @Test
+    public void TestRunningZ3WithNegative() {
+        HierarchicalGrid grid = new HierarchicalGrid();
+        List<HierarchicalCell> topCells = grid.getSubHiearchy();
+
+        topCells.add(new HierarchicalCell("x > 0"));
+        topCells.add(new HierarchicalCell("x == 0"));
+        topCells.add(new HierarchicalCell("0 > x"));
+
+        List<HierarchicalCell> nextGrid = topCells.get(1).getSubHiearchy();
+        nextGrid.add(new HierarchicalCell("z > 0"));
+        nextGrid.add(new HierarchicalCell("z == 0"));
+        nextGrid.add(new HierarchicalCell("z == -1"));
+        nextGrid.add(new HierarchicalCell("0 > z"));
+
+        //nextGrid.get(1).getSubHiearchy().add(new HierarchicalCell("z == 0"));
+
+        List<CheckerRunnerResult> res = CheckerRunner.RunZ3(grid, variableParser.parseVariables("x,z"));
+        assertEquals(1, res.size());
+        assertEquals(2, res.get(0).SampleValues.size());
+        assertEquals("0.0", res.get(0).SampleValues.get("x"));
+        assertEquals("(- 1.0)", res.get(0).SampleValues.get("z"));
+    }
+    @Test
+    public void TestRunningZ3WithFractionalReturn() {
+        HierarchicalGrid grid = new HierarchicalGrid();
+        List<HierarchicalCell> topCells = grid.getSubHiearchy();
+
+        topCells.add(new HierarchicalCell("x > 0"));
+        topCells.add(new HierarchicalCell("x == 0"));
+        topCells.add(new HierarchicalCell("x == 2.5"));
+        topCells.add(new HierarchicalCell("0 > x"));
+
+        List<CheckerRunnerResult> res = CheckerRunner.RunZ3(grid, variableParser.parseVariables("x"));
+        assertEquals(1, res.size());
+        assertEquals(1, res.get(0).SampleValues.size());
+        assertEquals("(5.0 / 2.0)", res.get(0).SampleValues.get("x"));
+    }
+    @Test
+    public void TestRunningZ3WithNegativeFractionalReturn() {
+        HierarchicalGrid grid = new HierarchicalGrid();
+        List<HierarchicalCell> topCells = grid.getSubHiearchy();
+
+        topCells.add(new HierarchicalCell("x > 0"));
+        topCells.add(new HierarchicalCell("x == 0"));
+        topCells.add(new HierarchicalCell("x == -2.5"));
+        topCells.add(new HierarchicalCell("0 > x"));
+
+        List<CheckerRunnerResult> res = CheckerRunner.RunZ3(grid, variableParser.parseVariables("x"));
+        assertEquals(1, res.size());
+        assertEquals(1, res.get(0).SampleValues.size());
+        assertEquals("(- (5.0 / 2.0))", res.get(0).SampleValues.get("x"));
+    }
+
+    VariableParser variableParser = new VariableParser();
+}

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/smtlibchecker/HierarchicalGridSMTLIBGeneratorTest.java

+/*
+ * 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.tabularexpressiontoolbox.smtlibchecker;
+
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParser;
+import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchcialGridCheckerWalkerGenerator;
+import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchicalCell;
+import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchicalGrid;
+import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.junit.runners.JUnit4;
+
+import java.util.List;
+
+import static org.junit.Assert.assertEquals;
+
+/**
+ *
+ * @author Matthew Dawson <matthew@mjdsystems.ca>
+ */
+@RunWith(JUnit4.class)
+public class HierarchicalGridSMTLIBGeneratorTest {
+
+    // Exercise the smtlib generator using a table designed in matlab.
+    @Test
+    public void exerciseSMTLIBGenerator() {
+        HierarchicalGrid grid = new HierarchicalGrid();
+        List<HierarchicalCell> topCells = grid.getSubHiearchy();
+
+        topCells.add(new HierarchicalCell("x > 0"));
+        topCells.add(new HierarchicalCell("x == 0"));
+        topCells.add(new HierarchicalCell("0 > x"));
+
+        List<HierarchicalCell> nextGrid = topCells.get(1).getSubHiearchy();
+        nextGrid.add(new HierarchicalCell("z > 0"));
+        nextGrid.add(new HierarchicalCell("z == 0"));
+        nextGrid.add(new HierarchicalCell("0 > z"));
+
+        nextGrid.get(1).getSubHiearchy().add(new HierarchicalCell("z == 0"));
+
+        String out = HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(grid, new HierarchicalGridSMTLIBGenerator(variableParser.parseVariables("x,z")));
+
+        String expected = "(push 1)\n" +
+                "(assert (and true (or (and (> x 0.0) (= x 0.0))\n" +
+                "(and (> x 0.0) (> 0.0 x))\n" +
+                "(and (= x 0.0) (> 0.0 x)))))\n" +
+                "(check-sat)\n" +
+                "(pop 1)\n" +
+                "(push 1)\n" +
+                "(assert (and true (not (or (> x 0.0) (= x 0.0) (> 0.0 x)))))\n" +
+                "(check-sat)\n" +
+                "(pop 1)\n" +
+                "(push 1)\n" +
+                "(assert (and (= x 0.0) (or (and (> z 0.0) (= z 0.0))\n" +
+                "(and (> z 0.0) (> 0.0 z))\n" +
+                "(and (= z 0.0) (> 0.0 z)))))\n" +
+                "(check-sat)\n" +
+                "(pop 1)\n" +
+                "(push 1)\n" +
+                "(assert (and (= x 0.0) (not (or (> z 0.0) (= z 0.0) (> 0.0 z)))))\n" +
+                "(check-sat)\n" +
+                "(pop 1)\n" +
+                "(push 1)\n" +
+                "(assert (and (= z 0.0) (= x 0.0) false))\n" +
+                "(check-sat)\n" +
+                "(pop 1)\n" +
+                "(push 1)\n" +
+                "(assert (and (= z 0.0) (= x 0.0) (not (= z 0.0))))\n" +
+                "(check-sat)\n" +
+                "(pop 1)\n";
+
+        assertEquals(expected, out);
+    }
+
+    // Test the smtlib generator using an empty table
+    @Test
+    public void testEmptyTable() {
+        HierarchicalGrid grid = new HierarchicalGrid();
+
+        String out = HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(grid, new HierarchicalGridSMTLIBGenerator(variableParser.parseVariables("x,z")));
+
+        String expected = "(push 1)\n" +
+                "(assert (and true false))\n" +
+                "(check-sat)\n" +
+                "(pop 1)\n" +
+                "(push 1)\n" +
+                "(assert (and true (not true)))\n" +
+                "(check-sat)\n" +
+                "(pop 1)\n";
+
+        assertEquals(expected, out);
+    }
+
+    VariableParser variableParser = new VariableParser();
+}

TET.m

+classdef (Sealed) TET < handle
+    %TET provides the global settings for the Tabular Expression Toolbox
+    %   TET provides the system through which all global settings are
+    %   accssed and changed.  It also provides a convient place for some
+    %   globals used in the TET.
+
+    properties (Access = private)
+        variableParser = ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParser
+    end
+
+    methods
+        function variableParser = getVariableParser(obj)
+                variableParser = obj.variableParser;
+        end
+    end
+
+    methods (Access = private)
+        function obj = TET
+        end
+    end
+    methods (Static)
+      function singleObj = getInstance
+         persistent localObj
+         if isempty(localObj) || ~isvalid(localObj)
+            localObj = TET;
+         end
+         singleObj = localObj;
+      end
+   end
+
+end
+

TTdiag.m

 % Author: Colin Eles elesc@mcmaster.ca
 % Organization: McMaster Centre for Software Certification
 function TTdiag(varargin)
+% Java needs to be loaded here.  Thus load it.
+
+% First find the path.
+path = mfilename('fullpath');
+path = [path(1:size(path, 2)-6) 'Matlab2SMT/Matlab2SMT-1.0-SNAPSHOT-jar-with-dependencies.jar'];
+
+% Verify the jar isn't already in the classpath.
+classpath = javaclasspath;
+exists = 0;
+for i=1:size(classpath,1)
+    if strcmp(classpath{i}, path) == 1
+        exists = 1;
+    end
+end
+if exists == 0
+    % Not added yet, thus add it.
+    javaaddpath(path);
+end
+
 
 orig_gcbh = gcbh;