Commit 6e9bbbd0 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Add a utility class to hold checker results. 

Add a simple class to hold the results of a failed query to a SMT checker.
Also, it has a utility function to easily generate a matlab expression for
the failed test's counter-model.  Also test.

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

Matlab2SMT/src/main/java/ca/mcmaster/cas/smtlibchecker/CheckerRunnerResult.java

0 → 100644
+40 −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.smtlibchecker;



import java.util.List;

import java.util.Map;



/**

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

 */

final public class CheckerRunnerResult {

    public String Query;

    Map<String, String> SampleValues;



    public String GenerateMatlabVariableDeclarations() {

        StringBuilder ret = new StringBuilder();

        for(Map.Entry<String, String> var: SampleValues.entrySet()) {

            ret.

                    append(var.getKey()).

                    append(" = ").

                    append(var.getValue()).

                    append(";\n");

        }

        return ret.toString();

    }

}

Matlab2SMT/src/test/java/ca/mcmaster/cas/smtlibchecker/CheckerRunnerTest.java

0 → 100644
+62 −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.smtlibchecker;



import ca.mcmaster.cas.matlab2smt.VariableParser;

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.HashMap;

import java.util.List;



import static org.junit.Assert.*;



/**

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

 */

@RunWith(JUnit4.class)

public class CheckerRunnerTest {

    @Test

    public void TestRunningZ3() {

        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 == 1"));

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



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



        List<CheckerRunnerResult> res = CheckerRunner.RunZ3(grid, new VariableParser("x,z"));

        assertEquals(2, res.size());

        assertEquals(2, res.get(0).SampleValues.size());

        assertEquals("0.0", res.get(0).SampleValues.get("x"));

        assertEquals("1.0", res.get(0).SampleValues.get("z"));



        assertEquals(2, res.get(1).SampleValues.size());

        assertEquals("0.0", res.get(1).SampleValues.get("x"));

        assertEquals("0.0", res.get(1).SampleValues.get("z"));

    }

}