Skip to content
matlab_to_cvc_syntax_translation.m 1.12 KiB
Newer Older
%% matlab_to_cvc_syntax_translation
%translate matlab syntax to cvc syntax,
% will be added to in the future
% will only work for functions in the prelude
%
% inputs:
%   object:cvc_checker - cvc_checker object
%   matlab_string:string - string to be converted from matlab
%       syntax to cvc
% outputs;
%   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)

s = [matlab_string(1,:)];
for j = 2:size(matlab_string,1)
   s = [s ' ' matlab_string(j,:)];
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');
for i=1:size(floats,2)
   cvc_string = regexprep(cvc_string,floats{i},['(' strtrim(num2str(rats(eval(floats{i})))) ')'] );
end