From 90fd1509123bd48874d5deaf8b20464af0d75853 Mon Sep 17 00:00:00 2001
From: Colin Eles <elesc@mcmaster.ca>
Date: Thu, 11 Nov 2010 21:16:42 +0000
Subject: [PATCH] latest update for smt solver

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6520 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
---
 @CVC_checker/generate_file.m | 15 ++++++++++++---
 @GUI/check_call.m            |  5 ++++-
 @GUI/cvc_ext_call.m          | 37 ++++++++++++++++++++++++++++++++++++
 @GUI/pvs_ext_call.m          |  3 +--
 4 files changed, 54 insertions(+), 6 deletions(-)
 create mode 100644 @GUI/cvc_ext_call.m

diff --git a/@CVC_checker/generate_file.m b/@CVC_checker/generate_file.m
index d05e555..59e0eda 100644
--- a/@CVC_checker/generate_file.m
+++ b/@CVC_checker/generate_file.m
@@ -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
-[new_code,queries] = CVC_checker.generate_cvc_grid(object.data.Grid2,0);
+%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
 
diff --git a/@GUI/check_call.m b/@GUI/check_call.m
index 08c4f0e..8e2c2c1 100644
--- a/@GUI/check_call.m
+++ b/@GUI/check_call.m
@@ -26,7 +26,10 @@ else
 end
 
 if ~isempty(msg)
-    msgbox(msg);
+    
+    if isempty(event)
+        msgbox(msg);
+    end
     error = 1;
 end
 
diff --git a/@GUI/cvc_ext_call.m b/@GUI/cvc_ext_call.m
new file mode 100644
index 0000000..57b539d
--- /dev/null
+++ b/@GUI/cvc_ext_call.m
@@ -0,0 +1,37 @@
+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
+
+
diff --git a/@GUI/pvs_ext_call.m b/@GUI/pvs_ext_call.m
index 5cb1594..b762b40 100644
--- a/@GUI/pvs_ext_call.m
+++ b/@GUI/pvs_ext_call.m
@@ -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;
-- 
GitLab