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

First run full integration. 

Matlab -> CVC output is now fully handled by the java app.  Currently
requires some manual setup, but once done everything just works from the
gui.  Some extra output needs work still.


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

@CVC_checker/CVC_checker.m

+2 −2
Original line number Diff line number Diff line
@@ -12,9 +12,9 @@ classdef CVC_checker 
    

    methods(Static)

        

        [ code , query] = generate_cvc_grid( grid , level);

        [ code , query] = generate_cvc_grid( grid , level, var_def);

        [ code ] = find_parents( grid );

        cvc_string = matlab_to_cvc_syntax_translation(matlab_string);

        cvc_string = matlab_to_cvc_syntax_translation(matlab_string, var_def);

        [ cvc_type ] = pvs_to_cvc_subtypes( pvs_type );

        

    end

@CVC_checker/generate_cvc_grid.m

+8 −6
Original line number Diff line number Diff line
@@ -4,6 +4,8 @@ 
% inputs:

%   grid:Grid - grid to generate conditions for.

%   level:int - count of the queries generated.

%   var_def:VariableParser - Parsed input of the variables, available in

%   the MATLAB2SMT java package.

%

% outputs;

%   code:string - string representing code to generate including comments
@@ -12,7 +14,7 @@ 
% Author: Colin Eles elesc@mcmaster.ca

% Organization: McMaster Centre for Software Certification



function [ code , query] = generate_cvc_grid( grid , level)

function [ code , query] = generate_cvc_grid( grid , level, var_def)



% generate the formulas for the main grid
@@ -21,8 +23,8 @@ if isempty(parents); 
    disjoint = 'QUERY (';

    complete = 'QUERY (';

else

    disjoint = ['QUERY ' CVC_checker.matlab_to_cvc_syntax_translation(parents) ' => ('];

    complete = ['QUERY ' CVC_checker.matlab_to_cvc_syntax_translation(parents) ' => ('];

    disjoint = ['QUERY ' CVC_checker.matlab_to_cvc_syntax_translation(parents, var_def) ' => ('];

    complete = ['QUERY ' CVC_checker.matlab_to_cvc_syntax_translation(parents, var_def) ' => ('];

end



for i=1:size(grid.cells,2)
@@ -30,7 +32,7 @@ for i=1:size(grid.cells,2) 
  

    for j = i+1:size(grid.cells,2)

        % compare i to j

        disjoint = [disjoint 'NOT ( (' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(i).cond_text)) ') AND (' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(j).cond_text)) ') )'];

        disjoint = [disjoint 'NOT ( (' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(i).cond_text), var_def) ') AND (' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(j).cond_text), var_def) ') )'];



        if j~= size(grid.cells,2)

             disjoint = [disjoint ' AND ' char(10)];
@@ -43,7 +45,7 @@ for i=1:size(grid.cells,2) 
    

    

    

    complete = [complete '(' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(i).cond_text)) ')'];

    complete = [complete '(' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(i).cond_text), var_def) ')'];

    

    if i < size(grid.cells,2) - 1

        disjoint = [disjoint ' AND ' char(10)];
@@ -65,7 +67,7 @@ code = [code 'ECHO "begin' num2str(level+2) '";' char(10) 'PUSH;' char(10) compl 


for i=1:size(grid.cells,2)

    if ~isempty(grid.cells(i).subgrid)

        [new_code,new_queries] = CVC_checker.generate_cvc_grid(grid.cells(i).subgrid,level+2);

        [new_code,new_queries] = CVC_checker.generate_cvc_grid(grid.cells(i).subgrid,level+2, var_def);

        code = [code new_code];

        query = [query new_queries];

        level = size(query,2) - 2;

@CVC_checker/generate_file.m

+2 −2
Original line number Diff line number Diff line
@@ -28,12 +28,12 @@ new_code = ''; 
queries = [];

%generate grid 2

if size(object.data.Grid2.cells,2) > 1  

    [new_code,queries] = CVC_checker.generate_cvc_grid(object.data.Grid2,0);

    [new_code,queries] = CVC_checker.generate_cvc_grid(object.data.Grid2,0, inputs);

end

code = [code new_code];



if object.data.multi_mode == 0 && size(object.data.Grid1.cells,2) > 1

    [new_code,new_queries] = CVC_checker.generate_cvc_grid(object.data.Grid1,size(queries,2));

    [new_code,new_queries] = CVC_checker.generate_cvc_grid(object.data.Grid1,size(queries,2), inputs);

    queries = [queries new_queries];

    code = [code new_code];

@CVC_checker/matlab_to_cvc_syntax_translation.m

+6 −10
Original line number Diff line number Diff line
@@ -11,7 +11,7 @@ 
%   cvc_string:string - string converted to cvc syntax.

% Author: Colin Eles elesc@mcmaster.ca

% Organization: McMaster Centre for Software Certification

function cvc_string = matlab_to_cvc_syntax_translation(matlab_string)

function cvc_string = matlab_to_cvc_syntax_translation(matlab_string, var_def)



s = [matlab_string(1,:)];

for j = 2:size(matlab_string,1)
@@ -19,18 +19,14 @@ for j = 2:size(matlab_string,1) 
end

matlab_string = s;



cvc_string = regexprep(matlab_string,'&&',' AND ');

cvc_string = regexprep(cvc_string,'~(?!=)',' NOT ');

cvc_string = regexprep(cvc_string,'~=',' /= ');

cvc_string = regexprep(cvc_string,'==',' = ');

cvc_string = regexprep(cvc_string,'\|\|',' OR ');

cvc_string = regexprep(cvc_string,'ceil','ceiling');



floats = regexp(cvc_string,'[0-9]*\.[0-9]*','match');

floats = regexp(matlab_string,'[0-9]*\.[0-9]*','match');

for i=1:size(floats,2)

   cvc_string = regexprep(cvc_string,floats{i},['(' strtrim(num2str(rats(eval(floats{i})))) ')'] );

   matlab_string = regexprep(matlab_string,floats{i},['(' strtrim(num2str(rats(eval(floats{i})))) ')'] );

end



parser = ca.mcmaster.cas.matlab2smt.MatlabParser(var_def, matlab_string);

cvc_string = char(parser.getRootExpression().getCVC3Output())



end

Matlab2SMT/src/main/java/ca/mcmaster/cas/matlab2smt/MatlabExpression.java

+1 −1
Original line number Diff line number Diff line
@@ -8,7 +8,7 @@ package ca.mcmaster.cas.matlab2smt; 
 *

 * @author matthew

 */

interface MatlabExpression {

public interface MatlabExpression {

    VariableType type();

    

    String getCVC3Output();