Commit e3b00992 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Fix pvs check to work on numbers always, and work if the string changes. 

Instead of assuming the number is always at a certain position, use a regexp
to find it.  It basically looks for "PVS Version 0.0", and only uses the 0.0.


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

@PVS_checker/parse_pvs_result.m

+3 −3
Original line number Diff line number Diff line
@@ -24,12 +24,12 @@ else 
            % These parsing depend on the version of PVS used,

            % which may be a bad idea, although pvs is not

            

            if strncmp(object.pvs_version,'PVS Version 4.0',15)

            if object.pvs_version <= 4.0

                % find the TCC that was unprovable

                search_str = sprintf('(?<=Proving formula %s[\\n]*)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)),char(found(i)));

            elseif strncmp(object.pvs_version,'PVS Version 4.2',15)

            elseif object.pvs_version <= 4.2

                search_str =  sprintf('(?<=Installing rewrite rule \\w+\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)));

            elseif strncmp(object.pvs_version,'PVS Version ',12) && str2num(object.pvs_version(13:15))>=5.0

            elseif object.pvs_version >= 5.0

                search_str =  sprintf('(?<=Installing rewrite rule.*\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)));

            end

            found2 = regexp(result,char(search_str),'match','once');

@PVS_checker/pvs_check.m

+3 −1
Original line number Diff line number Diff line
@@ -31,7 +31,9 @@ end 






object.pvs_version = PVS_checker.get_pvs_version;

version_string = PVS_checker.get_pvs_version;

version = regexp(version_string, 'PVS Version (...)', 'tokens');

object.pvs_version = str2double(char(version{1}));





% THIS SECTION NEEDS SOME WORK