smtlib_ext_call.m

function [] = cvc_ext_call( object,src,event )
%CVC_EXT_CALL Summary of this function goes here
%   Detailed explanation goes here


object.save_call([],[]);
object.save_data;
if (object.validation_report_handle ~= 0)
    delete(object.validation_report_handle);
    object.validation_report_handle = 0;
end
error = object.check_call([],2);


if (~error)
    
    inputs = TET.getInstance.getVariableParser.parseVariables(object.Data.function_inputs);
    vars = inputs.getVariables().values();

    HGrid = ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchicalGrid
    TableBlock.convert_hierarchical_grid_to_java(object.Data.Grid2.cells, HGrid.getSubHiearchy());

    res = ca.mcmaster.cas.tabularexpressiontoolbox.smtlibchecker.CheckerRunner.RunZ3(HGrid, inputs);

    if object.Data.multi_mode == 0 && size(object.Data.Grid1.cells,2) > 1
        HGrid = ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchicalGrid
        TableBlock.convert_hierarchical_grid_to_java(object.Data.Grid1.cells, HGrid.getSubHiearchy());

        res2 = ca.mcmaster.cas.tabularexpressiontoolbox.smtlibchecker.CheckerRunner.RunZ3(HGrid, inputs);
        res.addAll(res2);
    end   
    
    if (res.isEmpty())
        check = 1;
        msgbox('table is valid');
    else
        check = 0;
        result = [];
        for i=0:res.size()-1
            r = res.get(i)
            var_out = {}
            % It is possible not sample values are present.  Just use an
            % empty cell array in this case.
            if ~isempty(r.SampleValues)
                var_it = vars.iterator()
                j = 0;
                while var_it.hasNext()
                    var = var_it.next()
                    var = var.name()
                    var_out(j*2+1:j*2+2) = {char(var), r.SampleValues.get(var)};
                    j = j+1;
                end
                var_out
            end
            result = [result struct('id', '1234a', 'TCC', 'TCC', 'seq', r.Query, 'ce', {var_out})]
        end
        Valid_Report = ValidationReport(object);
        Valid_Report.set_results(result);
        Valid_Report.set_mode(1);
        Valid_Report.init();
    end
    object.pvs_checked = check;
    object.update_Statusbar;
    if (object.mode == 1)
        
        TableBlock.set_block_display(object.block_handle,object.pvs_checked);
    end
    
end
end