Commit 37749598 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Handle the case when no complete queries exist in the grid walker. 

When walking an empty grid, no queries for either complete or disjoint are
generated.  Disjoint handled this fine, but complete did not.  Fix this.

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

src/main/java/ca/mcmaster/cas/smtlibchecker/HierarchicalGridSMTLIBGenerator.java

+6 −3
Original line number Diff line number Diff line
@@ -72,10 +72,13 @@ final public class HierarchicalGridSMTLIBGenerator implements HierarchcialGridCh 


        query = "(assert ";

        query += generateQueryPrefix();

        if (m_currentCompleteQueries.size() == 1) {

            query += "(not " + m_currentCompleteQueries.get(0);

        query += "(not ";

        if (m_currentCompleteQueries.isEmpty()) {

            query += "true";

        } else if (m_currentCompleteQueries.size() == 1) {

            query +=  m_currentCompleteQueries.get(0);

        } else {

            query += "(not (or " + StringUtils.join(m_currentCompleteQueries, " ") + ")";

            query += "(or " + StringUtils.join(m_currentCompleteQueries, " ") + ")";

        }

        query += ")))";

        m_queries.add(query);

src/test/java/ca/mcmaster/cas/smtlibchecker/HierarchicalGridSMTLIBGeneratorTest.java

+19 −0
Original line number Diff line number Diff line
@@ -85,4 +85,23 @@ public class HierarchicalGridSMTLIBGeneratorTest { 


        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(new VariableParser("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);

    }

}