% Obtain the number of verified branches for each verified instance.

% Specify the filename of the logfile.
filename = './results/all (gpu-1024)/cora/results.txt';
% filename = './results/center/cora/results.txt';
% filename = './results/fgsm/cora/results.txt';
% filename = './results/gpu-128/cora/results.txt';
% filename = './results/cpu/cora/results.txt';
% filename = './results/local-grad+refinement/cora/results.txt';
% filename = './results/conzono-exact-bounds-prop1/cora/results.txt';


% Specify the benchmark names.
benchmarkNames = {'acasxu_2023'};

% Specify a maximum number of iterations.
maxIterations = inf; % 50;
% Specify the indices of instances.
instanceIdx = 1:45;

% Read the log file.
logtext = fileread(filename);

% Specify the separators in the log file.
benchmarkSep = ...
['(' '__________________________________________________________________\\n' ...
 '------------------------------------------------------------------\\n' ...
 'BENCHMARK\\s+(%s)\\s+\\((\\d+)\\/(\\d+)\\)\\n' ...
 '------------------------------------------------------------------\\n' ...
 '|' 'Completed!' ')'];
instanceSep = ...
['__________________________________________________________________\n' ...
 'INSTANCE\s+\((\d+)\/(\d+)\)\n' ...
 '------------------------------------------------------------------\n'];
resultRegex = '[^:]+ -- [^:]+: (unsat|sat|unknown)\n';
timeRegex = '--- Verification time: ([0-9]*\.?[0-9]+) / (([0-9]*\.?[0-9]+)|Inf) \[s\]\n';
tableHeader = [...
    '‖===========================================================================‖\n' ...
    '‖ Iteration | #Queue | #Verified Branches | avg. Radius | ~Unknown Vol. [%] ‖\n' ...
    '‖===========================================================================‖\n'];
tableVerifiedBranchesColumn = '‖%s\\|[^|]*\\|%s\\|[^|]*\\|[^|]*‖';
tableBottomRule = ...
    '‖===========================================================================‖';

% Find the different benchmarks in the log file.
for i=1:length(benchmarkNames)
    % Separate the benchmark from the log.
    benchmarkLog = regexp(logtext, ...
        [sprintf(benchmarkSep,benchmarkNames{i}) '.+?' ...
        '(?=' sprintf(benchmarkSep,'\w+') ')'], ...
        'match');
    % Match the different instances.
    instanceLogs = regexp(benchmarkLog{1},instanceSep,'split');
    % The first one is just the preamble.
    instanceLogs = instanceLogs(2:end);

    % Only select the relevant instances.
    if ~isempty(instanceIdx)
        instanceLogs = instanceLogs(instanceIdx);
    end

    % Initialize the results.
    numVerifiedBranches = -ones(1,length(instanceLogs));
    numSatWithinMaxIter = 0;
    numUnsatWithinMaxIter = 0;
    verificationTime = -ones(1,length(instanceLogs));

    % Iterate over the instance logs and aggregate the statistics for
    % verified instances.
    for j=1:length(instanceLogs)
        % Obtain the j-th instance log.
        instanceLogj = instanceLogs{j};
        % Find the verification result.
        resultj = regexp(instanceLogj,resultRegex,'tokens');
        % Find the verification time.
        timej = regexp(instanceLogj,timeRegex,'tokens');
        % Obtain the number of iterations.
        numIterations_ = regexp(instanceLogj, ...
            [sprintf(tableVerifiedBranchesColumn,'\s*(\d+) ','[^|]*') '\n' tableBottomRule],'tokens');
        if str2double(numIterations_{1}) > maxIterations
            % More the the maximum number of iterations; skip this
            % instance.
            continue;
        end
        % We only consider 'verified' ('unsat') and 'falsified ('sat') instances.
        switch resultj{1}{1}
            case 'unsat'
                % Find the last number of verified branches for each table.
                numVerifiedBranches_ = regexp(instanceLogj, ...
                    [sprintf(tableVerifiedBranchesColumn,'[^|]*','\s*(\d+) ') '\n' tableBottomRule],'tokens');
                % Sum the number of verified instances.
                numVerifiedBranches(j) = ...
                    sum(cellfun(@(k) str2double(k),numVerifiedBranches_));
                % Count the number od 'unsat' instances which have less 
                % than maxIterations.
                numUnsatWithinMaxIter = numUnsatWithinMaxIter + 1;
                % Store the verification time.
                verificationTime(j) = str2double(timej{1}{1});
            case 'sat'
                % Count the number of 'sat' instances which have less than
                % maxIterations.
                numSatWithinMaxIter = numSatWithinMaxIter + 1;
                % Store the verification time.
                verificationTime(j) = str2double(timej{1}{1});
            otherwise
                % Skip this instance.

                % Store the verification time.
                verificationTime(j) = str2double(timej{1}{1});
        end
    end
    % We only consider the verified instances.
    numVerifiedBranches(numVerifiedBranches == -1) = [];
    % We only consider solved instances.
    verificationTime(verificationTime == -1) = [];

    % Print the statistics.
    fprintf('__________________________________________________________________\n');
    fprintf('------------------------------------------------------------------\n');
    fprintf('[%s] BENCHMARK %s\n',filename,benchmarkNames{i});
    fprintf('------------------------------------------------------------------\n');
    % Compute the percentage of solved instances.
    percentSolved = (numUnsatWithinMaxIter + numSatWithinMaxIter)/length(instanceLogs);
    fprintf('- %%Solved (#Verified / #Falsified) (within iter <= %s): %.2f%% (%d / %d)\n', ...
        string(maxIterations),percentSolved*100,numUnsatWithinMaxIter,numSatWithinMaxIter);
    % Compute average time of solved instances.
    avgVerificationTime = mean(verificationTime);
    fprintf('- avg. verification time (of solved instances): %.2f [s]\n', ...
        avgVerificationTime);
    fprintf('- avg. #Verified Branches: %.2f +- %.2f (min: %d, max: %d)\n', ...
        mean(numVerifiedBranches),std(numVerifiedBranches), ...
        min(numVerifiedBranches),max(numVerifiedBranches));
    fprintf('__________________________________________________________________\n');
end



