From e3b0099292d48e387769125effb3db9fbdaef7a5 Mon Sep 17 00:00:00 2001 From: Matthew Dawson Date: Fri, 12 Jul 2013 19:28:50 +0000 Subject: [PATCH] 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 --- @PVS_checker/parse_pvs_result.m | 6 +++--- @PVS_checker/pvs_check.m | 4 +++- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/@PVS_checker/parse_pvs_result.m b/@PVS_checker/parse_pvs_result.m index 817adb7..bec651b 100644 --- a/@PVS_checker/parse_pvs_result.m +++ b/@PVS_checker/parse_pvs_result.m @@ -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'); diff --git a/@PVS_checker/pvs_check.m b/@PVS_checker/pvs_check.m index aa2b7b8..17d221d 100644 --- a/@PVS_checker/pvs_check.m +++ b/@PVS_checker/pvs_check.m @@ -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 -- GitLab