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

Better handle the case of a single cell in the CVC3 grid generator. 

Instead of generating invalid CVC3 code when a grid has a single used cell,
instead simply do not generate a disjoint TCC as it will always be true
anyways.
parent 8080ae7f

src/main/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3Generator.java

+19 −16
Original line number Diff line number Diff line
@@ -55,11 +55,13 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridBrea 
    }



    private void outputCells() {

        // First is disjoint testing.

        String query = "";

        // First is disjoint testing.  Only emitted if more then 1 cell was seen.

        if (!m_currentDisjointQueries.isEmpty()) {

            m_output += "ECHO \"begin" + m_currentTCC + "\";\n";

            m_output += "PUSH;\n";



        String query = "QUERY ";

            query += "QUERY ";

            query += generateQueryPrefix();

            query += "(" + StringUtils.join(m_currentDisjointQueries, " AND\n");

            query += ");";
@@ -71,6 +73,7 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridBrea 


            // Finished first TCC, increment counter.

            m_currentTCC++;

        }



        // Next is complete.

        m_output += "ECHO \"begin" + m_currentTCC + "\";\n";

src/test/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3GeneratorTest.java

+3 −18
Original line number Diff line number Diff line
@@ -93,14 +93,9 @@ public class HierarchicalGridCVC3GeneratorTest { 
"ECHO \"end4\";\n"+

"ECHO \"begin5\";\n"+

"PUSH;\n"+

"QUERY ((z = 0) AND (x = 0)) => ();\n"+

"POP;\n"+

"ECHO \"end5\";\n"+

"ECHO \"begin6\";\n"+

"PUSH;\n"+

"QUERY ((z = 0) AND (x = 0)) => ((z = 0));\n"+

"POP;\n"+

"ECHO \"end6\";\n";

"ECHO \"end5\";\n";

        assertEquals(expected, out);

    }
@@ -149,14 +144,9 @@ public class HierarchicalGridCVC3GeneratorTest { 
                "ECHO \"end5\";\n" +

                "ECHO \"begin6\";\n" +

                "PUSH;\n" +

                "QUERY ((BVMULT(8,x,y) = 0bin00000000)) => ();\n" +

                "POP;\n" +

                "ECHO \"end6\";\n" +

                "ECHO \"begin7\";\n" +

                "PUSH;\n" +

                "QUERY ((BVMULT(8,x,y) = 0bin00000000)) => (BVGT(BVSUB(8,x,y),0bin00000000));\n" +

                "POP;\n" +

                "ECHO \"end7\";\n";

                "ECHO \"end6\";\n";

        assertEquals(expected, out);

    }
@@ -209,14 +199,9 @@ public class HierarchicalGridCVC3GeneratorTest { 
                "ECHO \"end6\";\n" +

                "ECHO \"begin7\";\n" +

                "PUSH;\n" +

                "QUERY ((BVMULT(8,x,y) = 0bin00000000)) => ();\n" +

                "POP;\n" +

                "ECHO \"end7\";\n" +

                "ECHO \"begin8\";\n" +

                "PUSH;\n" +

                "QUERY ((BVMULT(8,x,y) = 0bin00000000)) => (BVSGT(BVSUB(8,x,y),0bin00000000));\n" +

                "POP;\n" +

                "ECHO \"end8\";\n";

                "ECHO \"end7\";\n";

        assertEquals(expected, out);

    }