Commit e09f49f2 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Implement Z3 in the matlab code. 

Show an option for checking against Z3, and also hook it up to the matlab
code for use.  Everything should be working now.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10667 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 79b8e448

@GUI/GUI.m

+2 −0
Original line number Diff line number Diff line
@@ -64,6 +64,7 @@ classdef GUI < handle 
        multi_opt_out = [];

        prover_opt_pvs = [];

        prover_opt_cvc = [];

        prover_opt_smtlib = [];

        version = '0.7';

        undo_man = [];

        undo_opt = [];
@@ -72,6 +73,7 @@ classdef GUI < handle 
        default_prover = [];

        PVS_const = 1;

        CVC_const = 2;

        SMTLIB_const = 3;

        

    end

@GUI/init.m

+3 −0
Original line number Diff line number Diff line
@@ -161,6 +161,7 @@ uimenu(checkmenu,'Label','Typecheck','Accelerator','t','Callback',@(src,event)ty 
prover_menu = uimenu(checkmenu,'Label','Default Prover');

object.prover_opt_cvc = uimenu(prover_menu,'Label','CVC3','Callback',@(src,event)prover_select_call(object,src,event));

object.prover_opt_pvs = uimenu(prover_menu,'Label','PVS','Callback',@(src,event)prover_select_call(object,src,event));

object.prover_opt_smtlib = uimenu(prover_menu,'Label','Z3','Callback',@(src,event)prover_select_call(object,src,event));

uimenu(checkmenu,'Label', 'Syntax Check','Callback',@(src,event)check_call(object,src,event));
@@ -173,6 +174,8 @@ uimenu(checkmenu,'Label','PVS Check Status','Callback',@(src,event)prf_file_call 
uimenu(checkmenu,'Label','PVS Generate file','Callback',@(src,event)pvs_file_call(object,src,event));

uimenu(checkmenu,'Label','PVS Typecheck SimTypes','Callback',@(src,event)pvs_ext_call_sim(object,src,event));



uimenu(checkmenu,'Label','Z3 Typecheck','Separator','on','Callback',@(src,event)smtlib_ext_call(object,src,event));



uimenu(helpmenu,'Label','Product Help','Callback',@(src,event)help_call(object,src,event));

uimenu(helpmenu,'Label','About Tabular Expression Toolbox','Callback',@(src,event)about_call(object,src,event));

@GUI/prover_select_call.m

+3 −1
Original line number Diff line number Diff line
@@ -3,8 +3,10 @@ label = get(src,'Label'); 
% determine which label the user clicked on

if strcmp(label,'CVC3')

    object.default_prover = object.CVC_const;

else

elseif strcmp(label,'PVS')

    object.default_prover = object.PVS_const;

else

    object.default_prover = object.SMTLIB_const;

end



object.update_prover_check_status;

@GUI/smtlib_ext_call.m

0 → 100644
+68 −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);

    object.validation_report_handle = 0;

end

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





if (~error)

    

    inputs = ca.mcmaster.cas.matlab2smt.VariableParser(object.Data.function_inputs);

    vars = inputs.getVarList()



    HGrid = ca.mcmaster.cas.tablularexpression.HierarchicalGrid

    TableBlock.convert_hierarchical_grid_to_java(object.Data.Grid2.cells, HGrid.getSubHiearchy());



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



    if object.Data.multi_mode == 0 && size(object.Data.Grid1.cells,2) > 1

        HGrid = ca.mcmaster.cas.tablularexpression.HierarchicalGrid

        TableBlock.convert_hierarchical_grid_to_java(object.Data.Grid1.cells, HGrid.getSubHiearchy());



        res2 = ca.mcmaster.cas.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 = {}

            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

            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

@GUI/typecheck_call.m

+2 −1
Original line number Diff line number Diff line
@@ -3,8 +3,9 @@ function [ output_args ] = typecheck_call( object,src,event ) 
%   Detailed explanation goes here



if object.default_prover == object.CVC_const

    

    cvc_ext_call(object,src,event);

elseif object.default_prover == object.SMTLIB_const

    smtlib_ext_call(object,src,event);

else

    pvs_ext_call(object,src,event);

end