begnining of application of SMT solver, using CVC3 solver. only works for 1D...

classdef CVC_checker

    %CVC_CHECKER Summary of this class goes here

    %   Detailed explanation goes here

    properties

        command = 'cvc3'

        data = [];

    end

    methods(Static)

        [ code , query] = generate_cvc_grid( grid , level)

        [ code ] = find_parents( grid )

        cvc_string = matlab_to_cvc_syntax_translation(matlab_string)

    end

    methods

        function object = CVC_checker(data)

            object.data = data;

        end

    end

end

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])

    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

        seqs = [seqs struct('id', '1234a', 'TCC', 'test', '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

function [ output_args ] = cvc_parse_result( input_args )

%CVC_PARSE_RESULT Summary of this function goes here

%   Detailed explanation goes here

end

function [ code ] = find_parents( cell )

% assumption, initial input will be grid we want to find parents for not

% parent cell itself

code = '';

if isempty(cell)

    % current cell is empty

    code = '';

else

    if isempty(cell.parent_grid.parent_cell)

        % no parent cell

    else

        % there is a parent cell

        top = char(CVC_checker.find_parents(cell.parent_grid.parent_cell));

        code = char(cell.parent_grid.parent_cell.cond_text);

        if isempty(top);

            % there were no more above this cell

        else

            % there were more above this cell

            code = [code ' AND ' top];

        end

    end

end

end

function [ code , query] = generate_cvc_grid( grid , level)

%GENERATE_CVC_GRID Summary of this function goes here

%   Detailed explanation goes here

% generate the formulas for the main grid

parents = CVC_checker.find_parents(grid.cells(1));

if isempty(parents);

    disjoint = 'QUERY (';

    complete = 'QUERY (';

else

    disjoint = ['QUERY ' parents ' => ('];

    complete = ['QUERY ' parents ' => ('];

end

for i=1:size(grid.cells,2)

%   1

%   2  

%   3

%   

%   1 2

%   1 3

%   2 3

%   

%   1 2 3 4

%   1 2

%   1 3

%   1 4

%   

    for j = i+1:size(grid.cells,2)

        % compare i to j

        disjoint = [disjoint 'NOT ( (' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(i).cond_text)) ') AND (' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(j).cond_text)) ') )'];

        if j~= size(grid.cells,2)

             disjoint = [disjoint ' AND ' char(10)];

        end

    end

  % need to do pairwise disjointness

    % otherwise doesn't work

    complete = [complete '(' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(i).cond_text)) ')'];

    if i < size(grid.cells,2) - 1

        disjoint = [disjoint ' AND ' char(10)];

    end

    if i < size(grid.cells,2) 

        complete = [complete ' OR '];

    end

end

disjoint = [disjoint ');'];

complete = [complete ');'];

query = [{disjoint} {complete}];

code = ['ECHO "begin' num2str(level+1) '";' char(10) 'PUSH;'  char(10) disjoint char(10) 'COUNTERMODEL;' char(10) 'POP;' char(10) 'ECHO "end' num2str(level+1) '";' char(10)];

code = [code 'ECHO "begin' num2str(level+2) '";' char(10) 'PUSH;' char(10) complete  char(10) 'COUNTERMODEL;' char(10) 'POP;' char(10) 'ECHO "end' num2str(level+2) '";' char(10)];

for i=1:size(grid.cells,2)

    if ~isempty(grid.cells(i).subgrid)

        [new_code,new_queries] = CVC_checker.generate_cvc_grid(grid.cells(i).subgrid,level+2);

        code = [code new_code];

        query = [query new_queries];

        level = size(query,2) - 2;

    end

end

end