Commit 90fd1509 authored by Colin Eles's avatar Colin Eles
Browse files

latest update for smt solver 

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6520 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 3581723a

@CVC_checker/generate_file.m

+12 −3
Original line number Diff line number Diff line
@@ -10,16 +10,25 @@ code = []; 
% output the input variables

inputs = EMLGenerator.parse_inputs(object.data.function_inputs);

for i = 1:size(inputs,2)

    code = [code char(inputs{i}(1)) ':INT;' char(10)];

    code = [code char(inputs{i}(1)) ':REAL;' char(10)];

end





% call the recursive function to generate the queries



%generate grid 1

%generate grid 2

if size(object.data.Grid2.cells,2) > 1  

    [new_code,queries] = CVC_checker.generate_cvc_grid(object.data.Grid2,0);

end

code = [code new_code];



if size(object.data.Grid1.cells,2) > 1

    [new_code,new_queries] = CVC_checker.generate_cvc_grid(object.data.Grid1,size(queries,2));

    queries = [queries new_queries]

    code = [code new_code];



end   





% generate grid 2

@GUI/check_call.m

+4 −1
Original line number Diff line number Diff line
@@ -26,7 +26,10 @@ else 
end



if ~isempty(msg)

    

    if isempty(event)

        msgbox(msg);

    end

    error = 1;

end

@GUI/cvc_ext_call.m

0 → 100644
+37 −0
Original line number Diff line number Diff line 
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);

end

error = object.check_call([],2);





if (~error)

    

    [check,result] = object.CVC.cvc_check;

    

    if (check == 1)

        msgbox('table is valid');

    elseif (check == 0 && strcmp(result,'canceled'))

        return;

    else

        Valid_Report = ValidationReport(object);

        Valid_Report.set_results(result);

        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

@GUI/pvs_ext_call.m

+1 −2
Original line number Diff line number Diff line
@@ -14,7 +14,7 @@ object.save_data; 
if (object.validation_report_handle ~= 0)

    delete(object.validation_report_handle);

end

error = object.check_call;

error = object.check_call([],2);



if(object.multi_mode == 0)

    object.PVS.output_type = object.output_data_type;
@@ -22,7 +22,6 @@ if(object.multi_mode == 0) 
    object.PVS.input_type = object.input_data_type;

    

    

    

end



object.PVS.type_mode = 0;