function [ check, seqs ] = cvc_check( object ) %CVC_CHECK Summary of this function goes here % Detailed explanation goes here box = waitbar(0,'Generating Proof Script'); [filename, queries] = object.generate_file; waitbar(.10,box,'Running Proof'); [status, result] = system(['cvc3 ' filename]) if (status ~= 0) if (status == 127) msgbox('CVC3 command not found') else msgbox(['an error has occured!' char(10) result]); end check = 0; seqs = 'canceled'; delete(box); return; end waitbar(.70,box,'Parsing Results'); seqs = []; % look for incompleteness, happens with non-linear artihmetic, ie. % % multiplication % incomplete = regexp(result,'CVC3 was incomplete in this example due to','match'); % if ~isempty(incomplete) % incomplete_reason = regexp(result,'(?<=CVC3 was incomplete in this example due to:\n)[^\n]*','match','once') % msgbox(['CVC could not typecheck this table for the following reasons:' char(10) incomplete_reason]); % % check = 0; % seqs = 'canceled'; % delete(box); % return; % % 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 = []; % find results of individual queries, using regexp and notations in % output begin1 ... end1 query_result = regexp(result,['(?<=begin' num2str(i) ').*(?=end' num2str(i) ')'],'match'); invalid_found = regexp(char(query_result),'Invalid.|Unknown.'); if ~isempty(invalid_found) % formula was found to be invalid % look for a counter example asserts = regexp(char(query_result),'(?<=ASSERT[ ]*\()[^\n]*(?==)|(?<==)[^\n]*(?=\);)','match'); % for j = 1:size(asserts,2) % splits = {splits regexp(asserts(j),'=','split')}; % % end if mod(i,2) == 1 name = [filename '_' num2str(i) '_DIS']; else name = [filename '_' num2str(i) '_COM']; end seqs = [seqs struct('id', '1234a', 'TCC', name, 'seq', queries(i), 'ce', {asserts})]; end end if isempty(seqs) check = 1; else check = 0; end waitbar(1,box,'Deleting Proof Script'); delete(box); end