Commit 1bb332a8 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

First run at SMT-LIB generated table test. 

Implement a first run (with simple non-exhaustive test) of the SMT-LIB generator
for hierarchical tables.  This generates the same information as the cvc3
generator, but using the appropriate syntax.  Note that the generated script
can't be directly run, due to how SMT-LIB verifiers work regarding reading of
values, so the queries need to be piped directly across one by one for
verification.

Also, since SMT-LIB doesn't have an equivalent to CVC3's QUERY command, all
queries have a not placed in front.  This lead to a few changes to the queries:
 - Disjoint queries now had a format of: (not (and (not (and e1 e2)))).  This
can be simplified with De Morgan's law to (or (and e1 e2)) (by removing the
(not (and (not to the more simple (or).
 - Complete queries now have an extra (not in front.  No further optimization
is possible.
 - For the parent part of any query, instead of using (not (=> (p e)), which
removes the potential disjoint optimization, the not is pushed down so the
format is now (and p (not e)).  Also, for simplification p is always defined,
and is true when no parent cells exist.

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

Matlab2SMT/src/main/java/ca/mcmaster/cas/smtlibgenerator/HierarchicalGridSMTLIBGenerator.java

0 → 100644
+160 −0
Original line number Diff line number Diff line 
/*

 * Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>

 *

 * This program is free software: you can redistribute it and/or modify

 * it under the terms of the GNU General Public License as published by

 * the Free Software Foundation, either version 3 of the License, or

 * (at your option) any later version.

 *

 * This program is distributed in the hope that it will be useful,

 * but WITHOUT ANY WARRANTY; without even the implied warranty of

 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the

 * GNU General Public License for more details.

 *

 * You should have received a copy of the GNU General Public License

 * along with this program.  If not, see <http://www.gnu.org/licenses/>.

 */

package ca.mcmaster.cas.smtlibgenerator;



import ca.mcmaster.cas.matlab2smt.BooleanVariableType;

import ca.mcmaster.cas.matlab2smt.CVC3Generator;

import ca.mcmaster.cas.matlab2smt.MatlabParser;

import ca.mcmaster.cas.matlab2smt.SMTLIBGenerator;

import ca.mcmaster.cas.matlab2smt.VariableParser;

import ca.mcmaster.cas.tablularexpression.Cell;

import ca.mcmaster.cas.tablularexpression.HierarchcialGridCheckerGenerator;

import org.apache.commons.lang3.StringUtils;



import java.util.ArrayDeque;

import java.util.ArrayList;

import java.util.Deque;

import java.util.List;



/**

 *

 * @author Matthew Dawson <matthew@mjdsystems.ca>

 */

final public class HierarchicalGridSMTLIBGenerator implements HierarchcialGridCheckerGenerator {



    public HierarchicalGridSMTLIBGenerator(VariableParser variableDefinitions) {

        m_variableDefinitions = variableDefinitions;

    }



    private String generateQueryPrefix() {

        if (!m_parentCellsCVC3Code.isEmpty()){

            String output = "(and ";

            output += StringUtils.join(m_parentCellsCVC3Code, " ") + " ";

            return output;

        }

        return "(and true ";

    }



    private void outputCells() {

        // First is disjoint testing.

        m_output += "(push 1)\n";



        String query = "(assert ";

        query += generateQueryPrefix();

        if (m_currentDisjointQueries.isEmpty()) {

            query += "false";

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

            query += m_currentDisjointQueries.get(0);

        } else {

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

        }

        query += "))";

        m_queries.add(query);

        m_output += query + "\n";



        m_output += "(check-sat)\n(pop 1)\n";



        // Next is complete.

        m_output += "(push 1)\n";



        query = "(assert ";

        query += generateQueryPrefix();

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

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

        } else {

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

        }

        query += ")))";

        m_queries.add(query);

        m_output += query + "\n";



        m_output += "(check-sat)\n(pop 1)\n";



        m_currentlyRunning = false;



        // And finally clear the running list of current queries.

        m_currentCompleteQueries.clear();

        m_currentDisjointQueries.clear();

    }



    @Override

    public void descendIntoGridFromCell(Cell cell) {

        if (m_currentlyRunning) {

            outputCells();

        }

        m_parentCellsCVC3Code.addFirst(new MatlabParser(m_variableDefinitions, cell.contents()).getRootExpression().getCheckerOutput(m_CVC3Generator, m_booleanType));

        m_currentlyRunning = true;

    }



    @Override

    public void ascendFromGrid() {

        if (m_currentlyRunning) {

            outputCells();

        }

        m_parentCellsCVC3Code.removeFirst();

    }



    @Override

    public void handleEdgeCell(Cell cell) {

        handleLeafCell(cell);

    }



    @Override

    public void handleLeafCell(Cell cell) {

        // First get the appropriate CVC3 code from matlab.

        String newCellCode = new MatlabParser(m_variableDefinitions, cell.contents()).getRootExpression().getCheckerOutput(m_CVC3Generator, m_booleanType);



        // Next form the disjoint queries and add to the list.

        for(String otherCellCode : m_currentCompleteQueries) {

            String newDisjointQuery = "(and " + otherCellCode  + " " + newCellCode + ")";

            m_currentDisjointQueries.add(newDisjointQuery);

        }



        // Lastly add the cell to the list for the complete query

        m_currentCompleteQueries.add(newCellCode);

    }



    @Override

    public String getFinalString() {

        if (m_currentlyRunning) {

            outputCells();

        }

        return m_output;

    }



    public List<String> getFinalQueries() {

        if (m_currentlyRunning) {

            outputCells();

        }

        return m_queries;

    }



    Deque<String> m_parentCellsCVC3Code = new ArrayDeque<String>();



    List<String> m_currentDisjointQueries = new ArrayList<String>();

    List<String> m_currentCompleteQueries = new ArrayList<String>();



    boolean m_currentlyRunning = true;



    String m_output = "";

    List<String> m_queries = new ArrayList<String>();



    // To fix properly.

    VariableParser m_variableDefinitions;

    static BooleanVariableType m_booleanType = new BooleanVariableType();

    SMTLIBGenerator m_CVC3Generator = new SMTLIBGenerator();

}

Matlab2SMT/src/test/java/ca/mcmaster/cas/smtlibgenerator/HierarchicalGridSMTLIBGeneratorTest.java

0 → 100644
+89 −0
Original line number Diff line number Diff line 
/*

 * Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>

 *

 * This program is free software: you can redistribute it and/or modify

 * it under the terms of the GNU General Public License as published by

 * the Free Software Foundation, either version 3 of the License, or

 * (at your option) any later version.

 *

 * This program is distributed in the hope that it will be useful,

 * but WITHOUT ANY WARRANTY; without even the implied warranty of

 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the

 * GNU General Public License for more details.

 *

 * You should have received a copy of the GNU General Public License

 * along with this program.  If not, see <http://www.gnu.org/licenses/>.

 */

package ca.mcmaster.cas.smtlibgenerator;



import ca.mcmaster.cas.cvc3generator.HierarchicalGridCVC3Generator;

import ca.mcmaster.cas.matlab2smt.VariableParser;

import ca.mcmaster.cas.tablularexpression.HierarchcialGridCheckerWalkerGenerator;

import ca.mcmaster.cas.tablularexpression.HierarchicalCell;

import ca.mcmaster.cas.tablularexpression.HierarchicalGrid;

import org.junit.Test;

import org.junit.runner.RunWith;

import org.junit.runners.JUnit4;



import java.util.List;



import static org.junit.Assert.assertEquals;



/**

 *

 * @author Matthew Dawson <matthew@mjdsystems.ca>

 */

@RunWith(JUnit4.class)

public class HierarchicalGridSMTLIBGeneratorTest {



    // Exercise the cvc3 generator using a table designed in matlab.

    @Test

    public void exerciseCVC3Generator() {

        HierarchicalGrid grid = new HierarchicalGrid();

        List<HierarchicalCell> topCells = grid.getSubHiearchy();



        topCells.add(new HierarchicalCell("x > 0"));

        topCells.add(new HierarchicalCell("x == 0"));

        topCells.add(new HierarchicalCell("0 > x"));



        List<HierarchicalCell> nextGrid = topCells.get(1).getSubHiearchy();

        nextGrid.add(new HierarchicalCell("z > 0"));

        nextGrid.add(new HierarchicalCell("z == 0"));

        nextGrid.add(new HierarchicalCell("0 > z"));



        nextGrid.get(1).getSubHiearchy().add(new HierarchicalCell("z == 0"));



        String out = HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(grid, new HierarchicalGridSMTLIBGenerator(new VariableParser("x,z")));



        String expected = "(push 1)\n" +

                "(assert (and true (or (and (> x 0.0) (= x 0.0))\n" +

                "(and (> x 0.0) (> 0.0 x))\n" +

                "(and (= x 0.0) (> 0.0 x)))))\n" +

                "(check-sat)\n" +

                "(pop 1)\n" +

                "(push 1)\n" +

                "(assert (and true (not (or (> x 0.0) (= x 0.0) (> 0.0 x)))))\n" +

                "(check-sat)\n" +

                "(pop 1)\n" +

                "(push 1)\n" +

                "(assert (and (= x 0.0) (or (and (> z 0.0) (= z 0.0))\n" +

                "(and (> z 0.0) (> 0.0 z))\n" +

                "(and (= z 0.0) (> 0.0 z)))))\n" +

                "(check-sat)\n" +

                "(pop 1)\n" +

                "(push 1)\n" +

                "(assert (and (= x 0.0) (not (or (> z 0.0) (= z 0.0) (> 0.0 z)))))\n" +

                "(check-sat)\n" +

                "(pop 1)\n" +

                "(push 1)\n" +

                "(assert (and (= z 0.0) (= x 0.0) false))\n" +

                "(check-sat)\n" +

                "(pop 1)\n" +

                "(push 1)\n" +

                "(assert (and (= z 0.0) (= x 0.0) (not (= z 0.0))))\n" +

                "(check-sat)\n" +

                "(pop 1)\n";



        assertEquals(expected, out);

    }

}