Commit 4b923fad authored by Matthew Dawson's avatar Matthew Dawson
Browse files

SMT-LIB requires real literals to have a decimal point. So we do that. 

In SMT-LIB, any real literal *must* have a decimal point, otherwise various
parsers may explode.  Since I know if a literal is supposed to be real, fix
this issue by appending a harmless ".0" to the string of the number.  Fix
tests to verify this.

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

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

+7 −1
Original line number Diff line number Diff line
@@ -33,7 +33,13 @@ public class SMTLIBGenerator implements CheckerGenerator { 


    @Override

    public String GenerateLiterlaValue(String value, VariableType requestedType) {

        if (requestedType instanceof RealVariableType || requestedType instanceof MatlabLiteral.LiteralNumberType) {

        if (requestedType instanceof RealVariableType) {

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

                return value;

            } else {

                return value + ".0";

            }

        }else if (requestedType instanceof MatlabLiteral.LiteralNumberType) {

            return value;

        } else {

            throw new IllegalArgumentException("Can't cast literal to that type!");

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

+2 −2
Original line number Diff line number Diff line
@@ -35,7 +35,7 @@ public class MatlabParserTest { 
        CheckerGenerator generator = new CVC3Generator();

        assertEquals("5", expr.getCheckerOutput(generator, new RealVariableType()));

        generator = new SMTLIBGenerator();

        assertEquals("5", expr.getCheckerOutput(generator, new RealVariableType()));

        assertEquals("5.0", expr.getCheckerOutput(generator, new RealVariableType()));

    }

    

    @Test
@@ -161,6 +161,6 @@ public class MatlabParserTest { 
        CheckerGenerator generator = new CVC3Generator();

        assertEquals("(((z = 1) AND (x = 0)) AND (y = 2))", expr.getCheckerOutput(generator, expr.type()));

        generator = new SMTLIBGenerator();

        assertEquals("(and (and (= z 1) (= x 0)) (= y 2))", expr.getCheckerOutput(generator, expr.type()));

        assertEquals("(and (and (= z 1.0) (= x 0.0)) (= y 2.0))", expr.getCheckerOutput(generator, expr.type()));

    }

}