Commit c5509d2a authored by Colin Eles's avatar Colin Eles
Browse files

added support for dependant subtypes, seems to work well with ones like the... 

added support for dependant subtypes, seems to work well with ones like the power conditioning example, if you try to give a specific type, ie. {x:real|x>5}, cvc is not able to prove unless you provide a witness of the type. Currently translates from pvs style typing to the cvc style so that user only needs to know one way, the pvs way is cleaner

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6559 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent bcabe7a3

@CVC_checker/CVC_checker.m

+1 −1
Original line number Diff line number Diff line
@@ -15,7 +15,7 @@ classdef CVC_checker 
        [ code , query] = generate_cvc_grid( grid , level)

        [ code ] = find_parents( grid )

        cvc_string = matlab_to_cvc_syntax_translation(matlab_string)



        [ cvc_type ] = pvs_to_cvc_subtypes( pvs_type )

        

    end

@CVC_checker/cvc_check.m

+13 −1
Original line number Diff line number Diff line
@@ -40,6 +40,18 @@ seqs = []; 
%     

% end



% look for parse errors

fatal_exception = regexp(result,'*** Fatal exception');



if ~isempty(fatal_exception)

    msgbox(['CVC3 encountered a fatal exception' char(10) result],'Fatal Exception','error');

     check = 0;

         seqs = 'canceled';

         delete(box);

         return;

    

end





for i = 1:size(queries,2)

    asserts = [];
@@ -73,7 +85,7 @@ for i = 1:size(queries,2) 
end



if isempty(seqs)

    check = 1

    check = 1;

else

    check = 0;

end

@CVC_checker/generate_file.m

+8 −3
Original line number Diff line number Diff line
@@ -10,12 +10,17 @@ code = []; 
% output the input variables

inputs = EMLGenerator.parse_inputs(object.data.function_inputs);

for i = 1:size(inputs,2)

    code = [code char(inputs{i}(1)) ':REAL;' char(10)];

    if size(inputs{i},2) > 1

        cvc_type = CVC_checker.pvs_to_cvc_subtypes(inputs{i}(2));

    else

        cvc_type = 'REAL';

    end

    code = [code char(inputs{i}(1)) ':' char(cvc_type) ';' char(10)];

end





% call the recursive function to generate the queries

new_code = ''

new_code = '';

queries = [];

%generate grid 2

if size(object.data.Grid2.cells,2) > 1
@@ -25,7 +30,7 @@ code = [code new_code]; 


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

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

    queries = [queries new_queries]

    queries = [queries new_queries];

    code = [code new_code];



end

@CVC_checker/pvs_to_cvc_subtypes.m

0 → 100644
+28 −0
Original line number Diff line number Diff line 
function [ cvc_type ] = pvs_to_cvc_subtypes( pvs_type )

%PVS_TO_CVC_SUBTYPES Summary of this function goes here

%   Detailed explanation goes here



%pvs_type is parsed

string = char(pvs_type);

% remove brackets

string_no_brack = regexp(string,'(?<=\{)[^\n]*(?=\})','match');

if isempty(string_no_brack)

    cvc_type = pvs_type;

    return

end



split_at_pipe = regexp(char(string_no_brack),'\|','split');

if (size(split_at_pipe,2) ~= 2)

    %something strange happened

    cvc_type = pvs_type;

    return;

end



new_type = ['SUBTYPE( LAMBDA (' char(split_at_pipe{1}) '): ' char(split_at_pipe{2}) ')'];

cvc_type = {new_type};



    





end