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

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
+