cvc_check.m

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