+TableBlock/convert_hierarchical_grid_to_java.m

+%% convert_hierarchical_grid_to_java
+% generates a java version fo the hiearchcial grid
+%
+% inputs:
+%   grid:Grid - grid to convert
+%   java_grid:List<HierarchicalCell> - place to put changed cells.
+%
+% outputs;
+%   none
+% Author: Matthew Dawson matthew@mjdsystems.ca
+% Organization: McMaster Centre for Software Certification
+
+function convert_hierarchical_grid_to_java(grid, java_grid)
+
+for i=1:size(grid,2)
+    new_cell = ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchicalCell;
+    
+    old_cell = grid(i)
+    new_cell.setContents(old_cell.cond_text)
+    
+    if ~isempty(old_cell.subgrid)
+        TableBlock.convert_hierarchical_grid_to_java(old_cell.subgrid.cells, new_cell.getSubHiearchy())
+    end
+    java_grid.add(new_cell)
+end
+
+end
+

@CVC_checker/CVC_checker.m

@@ -6,16 +6,8 @@ classdef CVC_checker
         
         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);
-        [ cvc_type ] = pvs_to_cvc_subtypes( pvs_type );
+        generator = ca.mcmaster.cas.tabularexpressiontoolbox.expression.CVC3Generator();
+        boolean_type = ca.mcmaster.cas.tabularexpressiontoolbox.expression.BooleanVariableType();
         
     end
     

@CVC_checker/cvc_check.m

@@ -56,7 +56,7 @@ if ~isempty(fatal_exception)
 end
 
 
-for i = 1:size(queries,2)
+for i = 1:queries.size()
     asserts = [];
 
     % find results of individual queries, using regexp and notations in
@@ -77,7 +77,7 @@ for i = 1:size(queries,2)
         name = [filename '_' num2str(i) '_COM'];
     end    
 
-        seqs = [seqs struct('id', '1234a', 'TCC', name, 'seq', queries(i), 'ce', {asserts})];
+        seqs = [seqs struct('id', '1234a', 'TCC', name, 'seq', queries.get(i-1), 'ce', {asserts})];
     end
     
     

@CVC_checker/cvc_parse_result.m

-function [ output_args ] = cvc_parse_result( input_args )
-%CVC_PARSE_RESULT Summary of this function goes here
-%   Detailed explanation goes here
-
-
-end
-

@CVC_checker/find_parents.m

-%% find_parents
-% function will find all the parents of a cell, used to determine what
-% preconditions must be true.
-%
-% inputs:
-%   cell:Cell - cell to find the parents of
-%
-% outputs;
-%   code:string - string of conjunction of all parent cells.
-% Author: Colin Eles elesc@mcmaster.ca
-% Organization: McMaster Centre for Software Certification
-
-function [ code ] = find_parents( cell )
-% assumption, initial input will be grid we want to find parents for not
-%  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
-

@CVC_checker/generate_cvc_grid.m

@@ -4,6 +4,8 @@
 % inputs:
 %   grid:Grid - grid to generate conditions for.
 %   level:int - count of the queries generated.
+%   var_def:VariableParser - Parsed input of the variables, available in
+%   the MATLAB2SMT java package.
 %
 % outputs;
 %   code:string - string representing code to generate including comments
@@ -12,68 +14,17 @@
 % Author: Colin Eles elesc@mcmaster.ca
 % Organization: McMaster Centre for Software Certification
 
-function [ code , query] = generate_cvc_grid( grid , level)
+function [ code , query] = generate_cvc_grid( object, grid , level, var_def)
 
+% New Junk
+% First build grid in java
+HGrid = ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchicalGrid
+TableBlock.convert_hierarchical_grid_to_java(grid.cells, HGrid.getSubHiearchy());
 % 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 ' CVC_checker.matlab_to_cvc_syntax_translation(parents) ' => ('];
-    complete = ['QUERY ' CVC_checker.matlab_to_cvc_syntax_translation(parents) ' => ('];
-end
-
-for i=1:size(grid.cells,2)
-    
-  
-    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) '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) '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
-
-    
+gridGenerator = ca.mcmaster.cas.tabularexpressiontoolbox.cvc3generator.HierarchicalGridCVC3Generator(var_def, level);
+code = char(ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(HGrid, gridGenerator));
+query = gridGenerator.getFinalQueries();
 
 
 

@CVC_checker/generate_file.m

@@ -19,15 +19,8 @@ function_name = char(function_names{1}(1));
 
 code = [];
 % output the input variables
-inputs = EMLGenerator.parse_inputs(object.data.function_inputs);
-for i = 1:size(inputs,2)
-    if size(inputs{i},2) > 1
-        cvc_type = CVC_checker.pvs_to_cvc_subtypes(inputs{i}(2));
-    else
-        cvc_type = 'REAL';
-    end
-    code = [code char(inputs{i}(1)) ':' char(cvc_type) ';' char(10)];
-end
+inputs = TET.getInstance.getVariableParser.parseVariables(object.data.function_inputs);
+code = char(object.generator.GenerateVariablesDeclaration(inputs));
 
 
 % call the recursive function to generate the queries
@@ -35,13 +28,13 @@ new_code = '';
 queries = [];
 %generate grid 2
 if size(object.data.Grid2.cells,2) > 1  
-    [new_code,queries] = CVC_checker.generate_cvc_grid(object.data.Grid2,0);
+    [new_code,queries] = object.generate_cvc_grid(object.data.Grid2,1, inputs);
 end
 code = [code new_code];
 
 if object.data.multi_mode == 0 && 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];
+    [new_code,new_queries] = object.generate_cvc_grid(object.data.Grid1,queries.size(), inputs);
+    queries.addAll(new_queries);
     code = [code new_code];
 
 end   

@CVC_checker/matlab_to_cvc_syntax_translation.m

-%% matlab_to_cvc_syntax_translation
-%translate matlab syntax to cvc syntax,
-% will be added to in the future
-% will only work for functions in the prelude
-%
-% inputs:
-%   object:cvc_checker - cvc_checker object
-%   matlab_string:string - string to be converted from matlab
-%       syntax to cvc
-% outputs;
-%   cvc_string:string - string converted to cvc syntax.
-% Author: Colin Eles elesc@mcmaster.ca
-% Organization: McMaster Centre for Software Certification
-function cvc_string = matlab_to_cvc_syntax_translation(matlab_string)
-
-s = [matlab_string(1,:)];
-for j = 2:size(matlab_string,1)
-   s = [s ' ' matlab_string(j,:)];
-end
-matlab_string = s;
-
-cvc_string = regexprep(matlab_string,'&&',' AND ');
-cvc_string = regexprep(cvc_string,'~(?!=)',' NOT ');
-cvc_string = regexprep(cvc_string,'~=',' /= ');
-cvc_string = regexprep(cvc_string,'==',' = ');
-cvc_string = regexprep(cvc_string,'\|\|',' OR ');
-cvc_string = regexprep(cvc_string,'ceil','ceiling');
-
-floats = regexp(cvc_string,'[0-9]*\.[0-9]*','match');
-for i=1:size(floats,2)
-   cvc_string = regexprep(cvc_string,floats{i},['(' strtrim(num2str(rats(eval(floats{i})))) ')'] );
-end
-
-end
-
-
-
-

@CVC_checker/pvs_to_cvc_subtypes.m

-%% pvs_to_cvc_subtypes
-% converts types of the pvs syntax to cvc3 syntax. the syntax for doing
-% typing in the two languages is slightly different so we need to write
-% this function to translate between them.
-%
-% inputs:
-%   pvs_type:string - a string of a pvs type
-% outputs;
-%   cvc_type:string - a string of the cvc type.
-% Author: Colin Eles elesc@mcmaster.ca
-% Organization: McMaster Centre for Software Certification
-
-function [ cvc_type ] = pvs_to_cvc_subtypes( pvs_type )
-%PVS_TO_CVC_SUBTYPES Summary of this function goes here
-%   Detailed explanation goes here
-
-
-
-
-%pvs_type is parsed
-string = char(pvs_type);
-
-% change cases
-string = regexprep(string,'real','REAL');
-string = regexprep(string,'Real','REAL');
-string = regexprep(string,'int','INT');
-string = regexprep(string,'Int','INT');
-string = regexprep(string,'bool','BOOLEAN');
-string = regexprep(string,'Bool','BOOLEAN');
-string = regexprep(string,'BOOL[^EAN]','BOOLEAN');
-
-% remove brackets
-string_no_brack = regexp(string,'(?<=\{)[^\n]*(?=\})','match');
-if isempty(string_no_brack)
-    
-    cvc_type = {string};
-    return
-end
-
-split_at_pipe = regexp(char(string_no_brack),'\|','split');
-if (size(split_at_pipe,2) ~= 2)
-    %something strange happened
-    cvc_type = {string};
-    return;
-end
-
-new_type = ['SUBTYPE( LAMBDA (' char(split_at_pipe{1}) '): ' char(split_at_pipe{2}) ')'];
-cvc_type = {new_type};
-
-    
-
-
-end
-

@EMLGenerator/generate_preamble.m

@@ -13,11 +13,14 @@ function code = generate_preamble(object)
 code = [];
 function_name = EMLGenerator.parse_inputs(object.data.function_name);
 %generate input list
-parsed_input = EMLGenerator.parse_inputs(object.data.function_inputs);
+inputs = TET.getInstance.getVariableParser.parseVariables(object.data.function_inputs);
+parsed_input = inputs.getVariables().values();
+input_iter = parsed_input.iterator()
 input = [];
-for i= 1:size(parsed_input,2)
-    input = [input char(parsed_input{i}(1))];
-    if i ~= size(parsed_input,2)
+while input_iter.hasNext()
+    var = input_iter.next()
+    input = [input char(var.name())];
+    if input_iter.hasNext()
         input = [input ','];
     end
 end

@GUI/GUI.m

@@ -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/check_inputs.m

@@ -11,7 +11,9 @@
 % Author: Colin Eles elesc@mcmaster.ca
 % Organization: McMaster Centre for Software Certification
 function error = check_inputs(object)
-parsed_input = EMLGenerator.parse_inputs(get(object.function_inputs_control,'string'));
+%parsed_input = EMLGenerator.parse_inputs(get(object.function_inputs_control,'string'));
+%TODO FIX THIS!
+parsed_input = [];
 error = [];
 for i=1:size(parsed_input,2)
     if(size(parsed_input{i},2) == 2)

@GUI/check_matlab_syntax_condition.m

@@ -15,7 +15,9 @@
 % Organization: McMaster Centre for Software Certification
 function error = check_matlab_syntax_condition(object,string,result)
 % split the list of inputs to get inputs seperatly
-
+%TODO FIX THIS!
+error = [];
+return ;
 parsed_input = EMLGenerator.parse_inputs(get(object.function_inputs_control,'string'));
 check_string = [];
 

@GUI/init.m

@@ -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,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

+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
+
+

@GUI/typecheck_call.m

@@ -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

@GUI/update_prover_check_status.m

@@ -11,9 +11,15 @@ function update_prover_check_status( object )
 
 
 if object.default_prover == object.CVC_const
+    set(object.prover_opt_smtlib,'Checked','off');
     set(object.prover_opt_cvc,'Checked','on');
     set(object.prover_opt_pvs,'Checked','off');
+elseif object.default_prover == object.SMTLIB_const
+    set(object.prover_opt_smtlib,'Checked','on');
+    set(object.prover_opt_cvc,'Checked','off');
+    set(object.prover_opt_pvs,'Checked','off');
 else
+    set(object.prover_opt_smtlib,'Checked','off');
     set(object.prover_opt_cvc,'Checked','off');
     set(object.prover_opt_pvs,'Checked','on');
 end

Matlab2SMT/pom.xml

+<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+
+    <groupId>ca.mcmaster.cas.tabularexpressiontoolbox</groupId>
+    <artifactId>Matlab2SMT</artifactId>
+    <version>1.0-SNAPSHOT</version>
+    <packaging>jar</packaging>
+
+    <name>Matlab2SMT</name>
+    <url>http://maven.apache.org</url>
+
+    <properties>
+        <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
+    </properties>
+
+    <dependencies>
+        <dependency>
+            <groupId>junit</groupId>
+            <artifactId>junit</artifactId>
+            <version>4.11</version>
+            <scope>test</scope>
+        </dependency>
+        <dependency>
+            <groupId>org.antlr</groupId>
+            <artifactId>antlr4-runtime</artifactId>
+            <version>4.1</version>
+        </dependency>
+        <dependency>
+            <groupId>org.apache.commons</groupId>
+            <artifactId>commons-lang3</artifactId>
+            <version>3.1</version>
+        </dependency>
+    </dependencies>
+  
+    <build>
+        <plugins>
+            <plugin>
+                <groupId>org.antlr</groupId>
+                <artifactId>antlr4-maven-plugin</artifactId>
+                <version>4.1</version>
+                <configuration>
+                    <sourceDirectory>src/main/java</sourceDirectory>
+                </configuration>
+                <executions>
+                    <execution>
+                        <goals>
+                            <goal>antlr4</goal>
+                        </goals>
+                    </execution>
+                </executions>
+            </plugin>
+            <plugin>
+                <groupId>org.apache.maven.plugins</groupId>
+                <artifactId>maven-compiler-plugin</artifactId>
+                <version>2.3.2</version>
+                <configuration>
+                    <showDeprecation>true</showDeprecation>
+                    <source>1.6</source>
+                    <target>1.6</target>
+                </configuration>
+            </plugin>
+            <plugin>
+                <groupId>org.apache.maven.plugins</groupId>
+                <artifactId>maven-assembly-plugin</artifactId>
+                <version>2.2</version>
+                <configuration>
+                    <descriptorRefs>
+                        <descriptorRef>jar-with-dependencies</descriptorRef>
+                    </descriptorRefs>
+                    <archive>
+                        <manifest>
+                            <mainClass>ca.mcmaster.cas.tabularexpressiontoolbox.expression.App</mainClass>
+                        </manifest>
+                    </archive>
+                </configuration>
+                <executions>
+                    <execution>
+                        <phase>package</phase>
+                        <goals>
+                            <goal>single</goal>
+                        </goals>
+                    </execution>
+                </executions>
+            </plugin>
+        </plugins>
+    </build>
+</project>

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/cvc3generator/HierarchicalGridCVC3Generator.java

+/*
+ * Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.cvc3generator;
+
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Variable;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableCollection;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParser;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BooleanVariableType;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CVC3Generator;
+import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.Cell;
+import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchcialGridCheckerGenerator;
+import java.util.ArrayList;
+import java.util.ArrayDeque;
+import java.util.Deque;
+import java.util.List;
+import java.util.Map;
+
+import org.apache.commons.lang3.StringUtils;
+
+/**
+ *
+ * @author Matthew Dawson <matthew@mjdsystems.ca>
+ */
+final public class HierarchicalGridCVC3Generator implements HierarchcialGridCheckerGenerator {
+
+    public HierarchicalGridCVC3Generator(VariableCollection variableDefinitions, int queryCountStart) {
+        m_variableDefinitions = variableDefinitions;
+        m_currentTCC = queryCountStart;
+    }
+
+    private String generateQueryPrefix() {
+        if (!m_parentCellsCVC3Code.isEmpty()){
+            String output = "(";
+            output += StringUtils.join(m_parentCellsCVC3Code, " AND ");
+            output += ") => ";
+            return output;
+        }
+        return "";
+    }
+
+    private void outputCells() {
+        // First is disjoint testing.
+        m_output += "ECHO \"begin" + m_currentTCC + "\";\n";
+        m_output += "PUSH;\n";
+
+        String query = "QUERY ";
+        query += generateQueryPrefix();
+        query += "(" + StringUtils.join(m_currentDisjointQueries, " AND\n");
+        query += ");";
+        m_queries.add(query);
+        m_output += query + "\n";
+
+        m_output += "POP;\n";
+        m_output += "ECHO \"end" + m_currentTCC + "\";\n";
+
+        // Finished first TCC, increment counter.
+        m_currentTCC++;
+
+        // Next is complete.
+        m_output += "ECHO \"begin" + m_currentTCC + "\";\n";
+        m_output += "PUSH;\n";
+
+        query = "QUERY ";
+        query += generateQueryPrefix();
+        query += "(" + StringUtils.join(m_currentCompleteQueries, " OR ");
+        query += ");";
+        m_queries.add(query);
+        m_output += query + "\n";
+
+        m_output += "POP;\n";
+        m_output += "ECHO \"end" + m_currentTCC + "\";\n";
+
+        // Finished other TCC, increment counter.
+        m_currentTCC++;
+
+        m_currentlyRunning = false;
+
+        // And finally clear the running list of current queries.
+        m_currentCompleteQueries.clear();
+        m_currentDisjointQueries.clear();
+    }
+
+    @Override
+    public void descendIntoGridFromCell(Cell cell) {
+        if (m_currentlyRunning) {
+            outputCells();
+        }
+        m_parentCellsCVC3Code.addFirst(MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_CVC3Generator, m_booleanType));
+        m_currentlyRunning = true;
+    }
+
+    @Override
+    public void ascendFromGrid() {
+        if (m_currentlyRunning) {
+            outputCells();
+        }
+        m_parentCellsCVC3Code.removeFirst();
+    }
+
+    @Override
+    public void handleEdgeCell(Cell cell) {
+        handleLeafCell(cell);
+    }
+
+    @Override
+    public void handleLeafCell(Cell cell) {
+        // First get the appropriate CVC3 code from matlab.
+        String newCellCode = MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_CVC3Generator, m_booleanType);
+
+        // Next form the disjoint queries and add to the list.
+        for(String otherCellCode : m_currentCompleteQueries) {
+            String newDisjointQuery = "NOT ( " + otherCellCode  + " AND " + newCellCode + " )";
+            m_currentDisjointQueries.add(newDisjointQuery);
+        }
+
+        // Lastly add the cell to the list for the complete query
+        m_currentCompleteQueries.add(newCellCode);
+    }
+
+    @Override
+    public String getFinalString() {
+        if (m_currentlyRunning) {
+            outputCells();
+        }
+        return m_output;
+    }
+
+    public List<String> getFinalQueries() {
+        if (m_currentlyRunning) {
+            outputCells();
+        }
+        return m_queries;
+    }
+
+    Deque<String> m_parentCellsCVC3Code = new ArrayDeque<String>();
+
+    List<String> m_currentDisjointQueries = new ArrayList<String>();
+    List<String> m_currentCompleteQueries = new ArrayList<String>();
+    
+    boolean m_currentlyRunning = true;
+    int m_currentTCC = 1;
+
+    String m_output = "";
+    List<String> m_queries = new ArrayList<String>();
+
+    // To fix properly.
+    VariableCollection m_variableDefinitions;
+    static BooleanVariableType m_booleanType = new BooleanVariableType();
+    CVC3Generator m_CVC3Generator = new CVC3Generator();
+}