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 = [];
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.');
    
    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