Commit 85713f86 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

CVC3 doesn't allow decimal points, thus always use fractions. 

CVC3 doesn't allow decimal points to represent rational numbers.  Thus simplify
things by putting the literal into fractional form.  Currently reduction is
not attempted, and the simplest form is used.  Ex. 4.56 becomes (456/100) (as
tested in the accompanying unit test).

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10714 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 370ad2b8

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

+11 −1
Original line number Diff line number Diff line
@@ -190,7 +190,17 @@ final public class CVC3Generator implements CheckerGenerator{ 
    @Override

    public String GenerateLiterlaValue(String value, VariableType requestedType) {

        if (requestedType instanceof RealVariableType) {

            if (value.contains(".")) {

                String[] fraction = value.split("\\.");



                String res = "(";

                res += StringUtils.join(fraction, "");

                res += "/1" + StringUtils.repeat('0', fraction[1].length()) + ")";



                return res;

            } else {

                return value;

            }

        } else if (requestedType instanceof FixedPointVariableType) {

            FixedPointVariableType type = (FixedPointVariableType) requestedType;

            BigDecimal decimal = new BigDecimal(value);

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

+10 −0
Original line number Diff line number Diff line
@@ -24,4 +24,14 @@ public class CVC3GeneratorTest { 
        assertEquals("+", CVC3Generator.ConvertToOutputOp(op, new RealVariableType()));

        assertEquals("BVPLUS(13,", CVC3Generator.ConvertToOutputOp(op, new FixedPointVariableType(true, 13, 5)));

    }

    /**

     * Test of literals containing decimals.

     *

     * All decimals must be represented as fractions.  Ensure that this happens.

     */

    @Test

    public void testLiteralRationalsAreFractions() {

        MatlabLiteral literal = new MatlabLiteral("4.56");

        assertEquals("(456/100)", literal.getCheckerOutput(new CVC3Generator(), new RealVariableType()));

    }

}