Commit 78632af9 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Finish testing fixed point support for CVC3. 

Fixed point operations are now all tested.  Due to literals automatically
casting to reals, it is necessary to push the "x" variable further into the
expression.  To ensure everything works, add one more condition without x to
make sure everything stays stable.  Everything works, after adjusting search
strings.

Also, deal with both signed/unsigned fixed point types.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10711 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 365b3fc7

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

+42 −2
Original line number Diff line number Diff line
@@ -33,6 +33,12 @@ final public class CVC3Generator implements CheckerGenerator{ 
                return "BVSDIV(";

            case GreaterThen:

                return "BVSGT(";

            case GreaterThenEqual:

                return "BVSGE(";

            case LessThen:

                return "BVSLT(";

            case LessThenEqual:

                return "BVSLE(";

        }

        return GetIndifferentFixedPointFunctionFor(op);

    }
@@ -43,6 +49,12 @@ final public class CVC3Generator implements CheckerGenerator{ 
                return "BVUDIV(";

            case GreaterThen:

                return "BVGT(";

            case GreaterThenEqual:

                return "BVGE(";

            case LessThen:

                return "BVLT(";

            case LessThenEqual:

                return "BVLE(";

        }

        return GetIndifferentFixedPointFunctionFor(op);

    }
@@ -82,7 +94,7 @@ final public class CVC3Generator implements CheckerGenerator{ 
                if (!((FixedPointVariableType) type).isSigned()) {

                    func = GetUnsignedFixedPointFunctionFor(op);

                }

                if ((op == MatlabBinaryOperation.Addition || op == MatlabBinaryOperation.Multiplication) && type instanceof FixedPointVariableType) {

                if (op == MatlabBinaryOperation.Addition || op == MatlabBinaryOperation.Multiplication) {

                    FixedPointVariableType typeF = (FixedPointVariableType) type;

                    return func + typeF.digits() + ",";

                } else {
@@ -127,7 +139,35 @@ final public class CVC3Generator implements CheckerGenerator{ 


    @Override

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

        return "(" + GetUnaryOperationSymbolFor(op) + " " + expression + ")";

        switch (CVC3Generator.OpTypeForVariableType(op, usedType)) {

            case PrefixOp:

                return "(" + CVC3Generator.ConvertToOutputOp(op, usedType) + " " + expression + ")";

            case Function:

                return CVC3Generator.ConvertToOutputOp(op, usedType) + "(" + expression + ")";

            default:

                throw new IllegalStateException("Cannot output expression operation for requested operation type.");

        }

    }



    private static OperationType OpTypeForVariableType(MatlabUnaryOperation op, VariableType usedType) {

        if (usedType instanceof FixedPointVariableType) {

            return OperationType.Function;

        }

        return OperationType.PrefixOp;

    }



    private static String ConvertToOutputOp(MatlabUnaryOperation op, VariableType usedType) {

        switch (op) {

            case Negation:

                return "NOT";

            case Minus:

                if (usedType instanceof FixedPointVariableType) {

                    return "BVUMINUS";

                } else {

                    return "-";

                }

        }

        throw new IllegalArgumentException("Unhandled operation: " + op);

    }



    public String GenerateVariableType(VariableType type) {

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

+25 −9
Original line number Diff line number Diff line
@@ -35,15 +35,19 @@ public class GenericGeneratorTest { 
    @Parameters

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

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

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

                {new SMTLIBGenerator(),

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

                        null,

                        null},

                {new CVC3Generator(),

                        "(((((x * 5) = (1 / (- 4))) OR ((4 > (8 + 3)) AND (9 < (1 - 2)))) OR (11 >= 12)) OR (NOT (34 <= (- 54))))",

                        "((((BVMULT(8,x,0bin00010100) = BVSDIV(0bin00000100,(- 0bin00010000))) OR ((4 > (8 + 3)) AND (9 < (1 - 2)))) OR (11 >= 12)) OR (NOT (34 <= (- 54))))"

                        "((((((x * 5) = (1 / (- 4))) OR ((x > (8 + 3)) AND (9 < (x - 2)))) OR (x >= 12)) OR (NOT (34 <= (- x)))) OR (5 > 4))",

                        "(((((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))",

                        "(((((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))"

                }

        });

    }



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

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

    static private VariableType outputType = new BooleanVariableType();



    @Parameter(value = 0)
@@ -53,7 +57,10 @@ public class GenericGeneratorTest { 
    public String RealExpectedOutput;



    @Parameter(value = 2)

    public String FixedPointExpectedOutput;

    public String SignedFixedPointExpectedOutput;



    @Parameter(value = 3)

    public String UnsignedFixedPointExpectedOutput;



    @Test

    public void RealTest() {
@@ -65,11 +72,20 @@ public class GenericGeneratorTest { 
    }



    @Test

    public void FixedPointTest() {

        if (FixedPointExpectedOutput != null) {

            VariableParser vars = new VariableParser("x:fixedt(1, 8, 2");

    public void SignedFixedPointTest() {

        if (SignedFixedPointExpectedOutput != null) {

            VariableParser vars = new VariableParser("x:fixedt(1, 8, 2)");

            MatlabParser parser = new MatlabParser(vars, query);

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

        }

    }



    @Test

    public void UnsignedFixedPointTest() {

        if (UnsignedFixedPointExpectedOutput != null) {

            VariableParser vars = new VariableParser("x:fixedt(0, 8, 2)");

            MatlabParser parser = new MatlabParser(vars, query);

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

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

        }

    }

}