Skip to content
/*
* 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();
}
/*
* 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();
}
/*
* 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.
}
}
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 );
}
}
/*
* 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()));
}
}
/*
* 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();
}
/*
* 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()));
}
}
/*
* 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();
}
/*
* 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();
}
/*
* 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);
}
/*
* 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();
}
/*
* 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());
}
}
}
/*
* 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();
}
/*
* 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();
}
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
% 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;
......