Commit 8b6b389b authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Handle variable predicates in the generators. 

For both SMTLIB and CVC3, variable subtypes conditions are now emitted into
the necessary places.  This doesn't directly relate to the PVS support added
earlier.  For now, no proof is done that the subtype has any allowed input,
but that doesn't matter as the table would still be "valid" for no input.
Determining that the connected Simulink blocks have correct typing is not
considered currently.

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

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/CVC3Generator.java

+11 −0
Original line number Diff line number Diff line
@@ -189,12 +189,23 @@ final public class CVC3Generator implements CheckerGenerator{ 
    @Override

    public String GenerateVariablesDeclaration(Map<String, Variable> vars) {

        StringBuilder ret = new StringBuilder();

        // First generate all the variables.

        for(Variable var : vars.values()) {

            ret.append(var.name())

               .append(":")

               .append(GenerateVariableType(var.type()))

               .append(";\n");

        }



        // Then generate the variable predicates.  This ensures any dependent variables are declared.

        for(Variable var : vars.values()) {

            if (var.type().subtypePredicate() != null) {

                ret.append("ASSERT ")

                   .append(var.type().subtypePredicate().getCheckerOutput(this, new BooleanVariableType()))

                   .append(";\n");

            }

        }



        return ret.toString();

    }

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/SMTLIBGenerator.java

+10 −0
Original line number Diff line number Diff line
@@ -49,6 +49,7 @@ public class SMTLIBGenerator implements CheckerGenerator { 
    @Override

    public String GenerateVariablesDeclaration(Map<String, Variable> vars) {

        StringBuilder ret = new StringBuilder();

        // First generate all the variables.

        for (Variable var : vars.values()) {

            ret.append("(declare-fun ")

               .append(var.name())
@@ -56,6 +57,15 @@ public class SMTLIBGenerator implements CheckerGenerator { 
               .append(GenerateVariableType(var.type()))

               .append(")\n");

        }



        // Then generate the variable predicates.  This ensures any dependent variables are declared.

        for(Variable var : vars.values()) {

            if (var.type().subtypePredicate() != null) {

                ret.append("(assert ")

                        .append(var.type().subtypePredicate().getCheckerOutput(this, new BooleanVariableType()))

                        .append(")\n");

            }

        }

        return ret.toString();

    }

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/VariableTest.java

+28 −0
Original line number Diff line number Diff line
@@ -4,6 +4,7 @@ 
 */

package ca.mcmaster.cas.tabularexpressiontoolbox.expression;



import static org.hamcrest.CoreMatchers.is;

import static org.junit.Assert.*;



import org.junit.Test;
@@ -40,6 +41,33 @@ public class VariableTest { 
        assertEquals("(declare-fun " +name+ " () Real)\n", generator.GenerateVariablesDeclaration(varlist));

    }



    @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);



        CheckerGenerator generator = new CVC3Generator();

        String varDecl = generator.GenerateVariablesDeclaration(varList);



        assertThat(varDecl, is("var:REAL;\nASSERT (var > 0);\n"));



        generator = new SMTLIBGenerator();

        varDecl = generator.GenerateVariablesDeclaration(varList);



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