Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/MatlabParser.g4

+grammar MatlabParser;
+
+/*
+
+Things to fix:	
+
+0) lots of warnings.  This is because of anonymous function handles; see details in appropriate XXX comment.
+   if you comment out one line, all of the warnings go away.  I believe that even with the warnings,
+   the grammar is doing the right thing.
+1) "clear" statements can accept wildcards as part of IDs, but we can't (due to the way lexing happens)
+2) control flow statements require a newline or comma to resolve an ambiguity (but matlab doesn't)
+3) vector construction requires comma delimiters because of whitespace madness (but matlab doesn't)
+4) matrix transpose doesn't work (again because of lexing, and distinguishing strings from transposes).
+5) block comments don't work (and I can't figure out why)
+
+For each case, see the appropriate XXX comment below.
+
+*/
+
+/*options {
+	output=AST;
+}
+
+tokens {
+	// imaginary nodes for our AST
+	PROGRAM;
+	FUNCTION;
+	FUNCTION_RETURN;
+	PARAMETER_LIST;
+	FUNCTION_PARAMETER_LIST;
+	STATEMENT_LIST;
+	EXPRESSION;
+	EXPR_STMT;
+	NULL_STMT;
+	ASSIGN;
+	APPLY;
+	FIELDACCESS;
+	DYNFIELDACCESS;
+	CELLACCESS;
+	MATRIX;
+	VECTOR;
+	CELL;
+	CLEAR;
+	LHS;
+	RHS;
+	ID_NODE;
+	PARENS;
+}*/
+
+@parser::members{
+
+// This scans backwards in the token stream looking for a hidden newline.
+// The newline must occur after the last visible token and before the current token.
+
+// C IMPLEMENTATION
+/*
+
+    int check_for_hidden_newline( pmatlabParser ctx ) {
+
+      pANTLR3_TOKEN_STREAM ts = ctx->pParser->tstream;
+
+      int tok_ind = INDEX(); // this is the index of LT(1)
+      pANTLR3_COMMON_TOKEN cur_tok = LT(1);
+
+      ANTLR3_UINT32 cur_tok_chan = cur_tok->getChannel( cur_tok ); // this is the current channel.
+
+      int rval = 0;
+
+      while ( tok_ind > 0 ) {
+	tok_ind--;
+	cur_tok = ts->get( ts, tok_ind );
+	if ( cur_tok->getChannel( cur_tok ) == cur_tok_chan ) {
+	  // uh-oh.  we found a non-hidden token further back in the stream, but no newline in between.  fail.
+	  break;
+	}
+	if ( cur_tok->getType( cur_tok ) == NL ) {
+	  // found it!
+	  rval = 1;
+	  break;
+	}
+      }
+
+      return rval;
+    }
+
+
+
+*/
+// JAVA IMPLEMENTATION
+// Useful for debugging.  NOTE: UNCOMMENT THE RELEVANT LINE IN hidden_nl!
+
+
+boolean check_for_hidden_newline( TokenStream input ) {
+        int tok_ind = input.index(); // this is the index of LT(1)
+        Token cur_tok = input.LT(1); 
+        int cur_tok_chan = cur_tok.getChannel(); // this is the current channel.
+
+        boolean rval = false;
+
+        while ( tok_ind > 0 ) {
+        	tok_ind--;
+        	cur_tok = input.get( tok_ind );
+
+        	if ( cur_tok.getChannel() == cur_tok_chan ) {
+        		// uh-oh.  we found a non-hidden token further back in the stream, but no newline in between.  fail.
+        		break;
+        	}
+        	if ( cur_tok.getType() == NL ) {
+        		// found it!
+        		rval = true;
+        		break;
+        	}
+        }
+
+        return rval;
+}
+
+
+
+} // end of parser::members
+
+//
+// ==================================================================
+//
+// PARSER RULES
+//
+
+// we mostly want to ignore whitespace, but every now and then
+// it's significant -- as a statement delimiter, as part of
+// matrix construction, etc.  This checks the hiddent channel for a newline.
+
+hidden_nl
+	// Java
+	: ( { check_for_hidden_newline( _input ) }? )
+	// C
+	//: ( { check_for_hidden_newline( ctx ) }? )
+	;
+
+nloc	: ( hidden_nl | COMMA ); // mnemonic: newline or comma
+nlos	: ( hidden_nl | SEMI ); // mnemonic: newline or semicolon
+
+//
+// scripts and m-files
+//
+
+mfile 	: function_definition+;
+
+scriptfile: statement_list;
+
+program	: func_or_statement_list;
+
+//
+// functions and statements
+//
+
+function_definition
+	: FUNCTION function_return? ID parameter_list? nloc
+	  func_or_statement_list
+	  END
+	;
+
+function_return
+	: ID EQ
+	| LSBRACE (ID COMMA?)+? RSBRACE EQ
+	;
+
+// the contents of a function (or a .m file) are statements and function definitions
+func_or_statement: ( function_definition | statement );
+func_or_statement_list: func_or_statement*;
+
+// there are times when you can have a list of statements, but not function
+// definitions -- for example, inside of an "if" block.
+statement_list
+	:  statement*
+	;
+
+parameter_list
+	: LPAREN ( ID COMMA? )* RPAREN
+	;
+
+// Note: there is a functional difference between terminating a statement with a
+// newline vs. a semicolon, so we have to remember the appropriate token in the AST.
+
+statement
+	: lhs EQ rhs nlosoc #ASSIGNMENT
+	| expression nlosoc #EXPRESSION
+	| if_statement #IF_STATEMENT
+	| for_statement #FOR_STATEMENT
+	| while_statement #WHILE_STATEMENT
+	| switch_statement #SWITCH_STATEMENT
+	| try_statement #TRY_STATEMENT
+	| return_statement #RETURN_STATEMENT
+	| break_statement #BREAK_STATEMENT
+	| continue_statement #CONTINUE_STATEMENT
+	| clear_statement # CLEAR_STATEMENT
+	| global_statement #GLOBAL_STATEMENT
+	| persistent_statement #PERSISTENT_STATEMENT
+	| SEMI # NULL_STMT // a null statement
+	;
+
+nlosoc	: ( hidden_nl | SEMI | COMMA );
+
+lhs: id_plus_indexers;
+rhs: expression;
+
+/* 
+XXX CONTROL FLOW AMBIGUITIES:
+
+The statement
+    while a (5) end;
+is parsed as
+    while (a(5))
+      [empty]
+    end;
+and not
+    while a
+      (5)
+     end;
+but I can't seem to get a non-ambiguous grammar to do that.
+so, I enforce a newline or a comma after the expression to
+delimit it from the body of the statements.  everywhere you
+see a "nloc" below, you shouldn't really need one; this
+grammar therefore parses only a subset of "true" matlab.
+(Of course, *I* think that reasonable code wouldn't have
+such ambiguities, don't you?  :) )
+
+Similarly:	
+
+The statement
+    while 1 -5, end;
+is parsed as
+    while (1)
+      -5,
+    end;
+while the statement
+    while 1 - 5, end;
+is parsed as
+    while (1-5)
+      [empty]
+    end;
+
+NOTE : THIS FEELS A LOT LIKE THE VECTOR AMBIGUITIES BELOW.
+Perhaps solving one solves them both, since both are essentially
+'space-delimited expressions' ambiguities.
+
+*/
+	
+if_statement
+	: IF expression nloc statement_list elseif_statement* else_statement? END
+	;
+
+elseif_statement
+	: ELSEIF expression nloc statement_list
+	;
+	
+else_statement
+	: ELSE statement_list
+	;
+		
+for_statement
+	: FOR ID EQ expression nloc statement_list END
+	;
+	
+while_statement
+	: WHILE expression nloc statement_list END
+	;
+	
+switch_statement
+	: SWITCH expression nloc case_statement* otherwise_statement? END
+	;
+	
+case_statement
+	: CASE expression nloc statement_list
+	;
+
+otherwise_statement
+	: OTHERWISE nloc statement_list
+	;
+	
+try_statement
+	: TRY statement_list catch_statement? END
+	;
+	
+catch_statement
+        : CATCH ID? nlosoc statement_list
+	;
+	
+return_statement
+	: RETURNS nlosoc
+	;
+
+break_statement
+	: BREAK nlosoc
+	;
+	
+continue_statement
+	: CONTINUE nlosoc
+	;
+
+global_statement
+	: GLOBAL (ID COMMA?)+? nlosoc
+	;
+
+persistent_statement
+	: PERSISTENT (ID COMMA?)+? nlosoc
+	;
+
+/*	
+XXX CLEAR STATEMENT WILDCARDS
+
+How can we fix wildcards in clear statements?
+For example, "clear foo* bob" ought to be parsed as
+  clear (foo*) (bob)
+but this is hard since the '*' is lexed as its own
+character, and we've discarded the fact that there is
+whitespace between '*' and 'bob', but not between
+'foo' and '*'.  This means we can't tell that it's supposed
+to be part of the foo identifier.
+
+Options	for solving:
+1) parser-context sensitive lexing?  (I don't think this is right)
+2) poke around in the hidden channel to find out where the whitespace is.
+   this is probably the best solution, but seems like a pain.
+   
+*/
+
+
+clear_statement
+	: CLEAR (ID COMMA?)*? nlosoc
+	;
+
+//
+// ===============================
+//
+
+// a precedence hierarchy for parsing expressions
+
+// these are groups of operators that have equivalent precedences
+g1	: ( NEQ | DOUBLE_EQ | GRTE | GRT | LSTE | LST );
+g2	: ( PLUS | MINUS );
+g3	: ( LEFTDIV | RIGHTDIV | TIMES | EL_LEFTDIV | EL_RIGHTDIV | EL_TIMES );
+g4	: ( EXP | EL_EXP );
+
+
+/*
+
+XXX MATRIX TRANSPOSE PROBLEM.
+
+The single quote operator is problematic because of things like this:	
+
+aa' + foo('some string here')+bb'
+
+Right now, the operator is placed in the correct place in the grammar,
+and the grammar checks out just fine, but you get lexing errors if you
+try to use it.
+
+*/
+
+postfix_operator
+	: ( CCT | EL_CCT );
+prefix_operator
+	: ( PLUS | MINUS | NEG );
+
+// the hierarchy is defined from LOWEST to HIGHEST priority.
+
+expression : e0;
+
+e0	: e1;
+
+e1	: e2 (LOG_OR e2)*;
+e2	: e3 (LOG_AND e3)*;
+e3	: e4 (BIN_OR e4)*;
+e4	: e5 (BIN_AND e5)*;
+e5	: e6 (g1 e6)*;
+e6	: e7 (COLON e7)*;
+e7	: e8 (g2 e8)*;
+e8	: e9 (g3 e9)*;
+e9	: prefix_operator e9 | e10;
+e10	: e11 (g4 e11)*; // note: in matlab, exponentiation is left-associative
+e11	: unary_expression postfix_operator?;
+
+unary_expression
+	: base_expression #BASE_EXPRESIION
+	| LPAREN expression RPAREN # PARENS_EXPRESSION
+	;
+
+base_expression
+	: id_plus_indexers
+	| literal_number
+	| STRING
+	| anon_func_handle
+	| cell
+	| matrix
+	;
+
+literal_number
+        : INT
+        | FLOAT
+        ;
+
+/*
+XXX ANONYMOUS EXPRESSION AMBIGUITIES
+
+This generates a ton of warnings, but it does the right thing.
+At least, I think it does.
+
+We want anonymous expressions to be "greedy".
+
+The statement
+    a+@()x+y
+parses as
+   a+( @()x+y )
+and not as
+   a+ ( @()x ) +y
+but I can't seem to make the right behavior explicit.  The way that
+ANTLR is disabling the alternatives seems to result in the right
+behavior, though.
+
+If you comment out the second alternative here, the grammar should
+check out perfectly clean.
+*/
+
+anon_func_handle
+	: AT ID
+	| AT parameter_list (expression)?
+	;
+
+// this captures things like foo.(bar){3,4}.baz
+id_plus_indexers
+	:	( i1=ID )
+		( DOT ( i2=ID )
+                | LPAREN expression RPAREN
+		| LPAREN fpl1=function_parameter_list? RPAREN
+		| LBRACE fpl2=function_parameter_list RBRACE
+		)*
+	;
+
+// also permits the use of the colon as an "expression"
+function_parameter_list
+	: function_parameter ( COMMA function_parameter )*
+	;
+	
+function_parameter : expression	| COLON	;
+
+matrix	: LSBRACE vector? ( nlos vector )* RSBRACE;
+
+cell	: LBRACE vector? ( nlos vector )* RBRACE;
+
+/*
+
+XXX
+
+I think the rule is the following
+
+1) if a +/- does not have any space to the right, it's interpreted
+   as a unary op
+2) if there's no whitespace to the left of the operator, it's
+   grouped to the left.
+3) if there's whitespace to the right and left, it's treated as
+   a binary op, and expressions are required on the right and left.
+
+Vectors are pretty crazy.  Because you have a list of expressions
+that can be separated by nothing but whitespace, all sorts of parsing
+ambiguities start happening.  Whitespace becomes syntactically
+meaningful in strange ways that are not totally context free.
+For example,
+
+[ a + b ]	is parsed as 	[ (a+b) ]
+[ a+b ]		is parsed as 	[ (a+b) ]
+[ a +b ]	is parsed as	[ (a) (+b) ]
+
+A longer example:	
+
+[ 1+  2+  3 ]   parses to   6		  
+[ 1 + 2+  3 ]		    6		  
+[ 1  +2+  3 ]		    1     5	  
+[ 1+  2 + 3 ]		    6		  
+[ 1 + 2 + 3 ]		    6		  
+[ 1  +2 + 3 ]		    1     5	  
+[ 1+  2  +3 ]		    3     3	  
+[ 1 + 2  +3 ]		    3     3	  
+[ 1  +2  +3 ]		    1     2     3
+
+So, the weird thing is that we can't just look for the absence of a 
+space between '+' and the next character to determine if it's a binary
+or unary operator -- we also have to know if there's a space to the
+left of it.
+
+This is mostly a problem for prefix operators which can be ambiguous
+in this context, but it also shows up in things like cell arrays
+of anonymous function expressions.
+
+size( { @()a+b } )	is	[ 1 1 ]
+size( { @()a +b } )	is	[ 1 2 ]
+size( { @()a + b } )	is	[ 1 1 ]
+
+NOTE	:	 this feels like the control flow ambiguities above,
+since both are essentially "whitespace-delimited expression" problems.
+
+*/
+
+// XXX The COMMA should really have a ? after it!!!
+// vector	: ( expression COMMA? )+;
+vector	:	expression ( COMMA expression )*;
+
+//
+// ==================================================================
+//
+// LEXER RULES
+//
+
+//
+// language keywords
+//
+
+BREAK	: 'break';
+CASE	: 'case';
+CATCH	: 'catch';
+CONTINUE: 'continue';
+ELSE	: 'else';
+ELSEIF	: 'elseif';
+END	: 'end';
+FOR	: 'for';
+FUNCTION: 'function';
+GLOBAL	: 'global';
+IF	: 'if';
+OTHERWISE: 'otherwise';
+PERSISTENT: 'persistent';
+RETURNS	: 'return'; // not "RETURN" to avoid #define conflicts with readline.h
+SWITCH	: 'switch';
+TRY	: 'try';
+VARARGIN: 'varargin';
+WHILE	: 'while';
+CLEAR	: 'clear';
+
+ENDS	: END SEMI? ;
+
+//
+// operators and assignments
+//
+
+DOUBLE_EQ	: '==';
+
+LOG_OR	: '||';
+LOG_AND	: '&&';
+LSTE	: '<=';
+GRTE	: '>=';
+NEQ	: '~=';
+
+EL_TIMES	: '.*';
+EL_LEFTDIV	: './';
+EL_RIGHTDIV	: '.\\';
+EL_EXP	: '.^';
+EL_CCT	: '.\'';
+
+EQ	: '=';
+
+BIN_OR	: '|';
+BIN_AND	: '&';
+
+LST	: '<';
+GRT	: '>';
+
+COLON	: ':';
+
+PLUS	: '+';
+MINUS	: '-';
+NEG	: '~';
+TIMES	: '*';
+
+LEFTDIV	: '/';
+RIGHTDIV: '\\';
+
+EXP	: '^';
+
+CCT	: '\'';
+
+//
+// Other useful language snippets
+//
+
+SEMI	: ';';
+LPAREN	: '(';
+RPAREN	: ')';
+LBRACE	: '{';
+RBRACE	: '}';
+LSBRACE	: '[';
+RSBRACE	: ']';
+AT	: '@';
+DOT	: '.';
+COMMA	: ',';
+
+//
+// comments
+//
+
+NL	: '\r'? '\n' -> channel(HIDDEN); // newline
+
+// XXX I can't seem to get block comments to work.  The problem is that
+// no matter what I do, the linecomment ends up "overriding" the block
+// comment, and I get a lex error.  I've tried syntactic predicates,
+// but they didn't help...
+// If I comment out the LINECOMMENT rule, the BLOCKCOMMENT works fine.
+// So, since I can only seem to have one or the other, I'm commenting
+// out BLOCKCOMMENT for now.
+
+//BLOCKCOMMENT
+//        : '%{' (options{greedy=false;} : .)*  '%}' { $channel = HIDDEN; }
+//	;
+
+LINECOMMENT
+	: '%' .*? NL -> channel(HIDDEN)
+	;
+
+// I think this is how to use syntactic predicates, but it doesn't seem to work.
+//COMMENT
+//	: ( '%{' ) => '%{' (options{greedy=false;}: .)*  '%}' { $channel = HIDDEN; }
+//	| ( '%' (options{greedy=false;}: .)* NL ) { $channel = HIDDEN; }
+//	;
+
+
+THREEDOTS
+	: ( '...' NL ) -> channel(HIDDEN)
+	;
+
+//
+// identifiers, strings, numbers, whitespace
+//
+
+ID	: ('a'..'z'|'A'..'Z') ('a'..'z'|'A'..'Z'|'0'..'9'|'_')* ;
+
+INT	: '0'..'9'+ ;
+
+FLOAT
+	: ('0'..'9')+ '.' ('0'..'9')* EXPONENT?
+	| '.' ('0'..'9')+ EXPONENT?
+	| ('0'..'9')+ EXPONENT
+	;
+
+STRING
+	: '\'' ( ESC_SEQ | ~('\\'|'\'') )* '\''
+	;
+
+WS
+	: ( ' '
+        | '\t'
+        ) -> skip
+	;
+
+fragment
+EXPONENT
+	: ('e'|'E') ('+'|'-')? ('0'..'9')+ ;
+
+fragment
+HEX_DIGIT
+	: ('0'..'9'|'a'..'f'|'A'..'F') ;
+
+fragment
+ESC_SEQ
+	: '\\' ('b'|'t'|'n'|'f'|'r'|'\"'|'\''|'\\')
+	| UNICODE_ESC
+	| OCTAL_ESC
+	;
+
+fragment
+OCTAL_ESC
+	: '\\' ('0'..'3') ('0'..'7') ('0'..'7')
+	| '\\' ('0'..'7') ('0'..'7')
+	| '\\' ('0'..'7')
+	;
+
+fragment
+UNICODE_ESC
+	: '\\' 'u' HEX_DIGIT HEX_DIGIT HEX_DIGIT HEX_DIGIT
+	;

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/MatlabParser.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.parsers;
+
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BinaryOperation;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Expression;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionUnaryOperation;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionValue;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionBinaryOperation;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionWithSubExpression;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Literal;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.UnaryOperation;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Variable;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableCollection;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.G1Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.G2Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.G3Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.G4Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E0Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E1Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E2Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E3Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E4Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E5Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E6Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E7Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E8Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E9Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E10Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E11Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.Literal_numberContext;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.Id_plus_indexersContext;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.Prefix_operatorContext;
+import java.util.ArrayDeque;
+import java.util.Deque;
+import java.util.Map;
+
+import org.antlr.v4.runtime.ANTLRInputStream;
+import org.antlr.v4.runtime.CommonTokenStream;
+import org.antlr.v4.runtime.tree.ParseTree;
+import org.antlr.v4.runtime.tree.ParseTreeWalker;
+
+/**
+ *
+ * @author matthew
+ */
+final public class MatlabParser {
+
+    private MatlabParser() {
+    }
+
+    public static Expression parseMatlabCode(VariableCollection variableListing, String matlabCode) {
+        // create a CharStream that reads from standard input
+        ANTLRInputStream input = new ANTLRInputStream(matlabCode + "\n");
+
+        // create a lexer that feeds off of input CharStream
+        MatlabParserLexer lexer = new MatlabParserLexer(input);
+
+        // create a buffer of tokens pulled from the lexer
+        CommonTokenStream tokens = new CommonTokenStream(lexer);
+
+        // create a parser that feeds off the tokens buffer
+        MatlabParserParser parser = new MatlabParserParser(tokens);
+
+        ParseTree tree = parser.expression();
+        ParseTreeWalker walker = new ParseTreeWalker();
+        MatlabParserToExpressions listener = new MatlabParserToExpressions(variableListing.getVariablesAndEnumeratedValues());
+        walker.walk(listener, tree);
+
+        return listener.m_rootExpression;
+    }
+
+    private static class MatlabParserToExpressions extends MatlabParserBaseListener implements ExpressionWithSubExpression {
+
+        MatlabParserToExpressions(Map<String, Variable> variableListing) {
+            m_variableParser = variableListing;
+            m_opStack.addFirst(new ExpressionStackContainer(0, this));
+        }
+
+        private void incrementLevel() {
+            this.m_level++;
+        }
+
+        private void decrementLevel() {
+            this.m_level--;
+            if (!m_hiddenOpStack.isEmpty() && m_hiddenOpStack.peekFirst().level == m_level) {
+                // We have a hidden op here.  The normal methods won't find it, so make use of it!
+                HiddenOpStackContainer hiddenOp = m_hiddenOpStack.peekFirst();
+                addExpressionBinaryOperation(new ExpressionBinaryOperation(null, hiddenOp.op, null));
+                if (--hiddenOp.count == 0) {
+                    m_hiddenOpStack.removeFirst();
+                }
+            }
+
+            if (!m_opStack.isEmpty() && m_opStack.peekFirst().level > m_level) {
+                m_opStack.removeFirst();
+            }
+        }
+
+        private void enqueHiddenOp(BinaryOperation op, int count) {
+            m_hiddenOpStack.addFirst(new HiddenOpStackContainer(m_level, op, count));
+        }
+
+        private void addExpressionValue(ExpressionValue expressionValue) {
+            m_opStack.peekFirst().op.setSubExpression(expressionValue);
+        }
+
+        private void addExpressionBinaryOperation(ExpressionBinaryOperation op) {
+            if (m_rootExpression == null) {
+                throw new IllegalStateException("It should not be possible to have"
+                        + "an op where the left hand side is a null expression!");
+            } else {
+                if (m_opStack.peekFirst().level >= m_level) { //This current op happens after the root expression op.  Pull it up.
+                    op.setLHS((Expression) m_opStack.removeFirst().op);
+                    m_opStack.peekFirst().op.setSubExpression(op);
+                } else { //This op happens before.  Push it down the tree.
+                    op.setLHS(m_opStack.peekFirst().op.getSubExpression());
+                    m_opStack.peekFirst().op.setSubExpression(op);
+                }
+                m_opStack.addFirst(new ExpressionStackContainer(m_level, op));
+            }
+        }
+
+        private void addPrefixUnaryOperation(ExpressionUnaryOperation op) {
+        /* Unlike Binary operations, unary operations just always insert
+         * themselves into the operation stack exactly where they appear.
+         * The whole left hand side handling never happens, since there is no
+         * left hand side.  So just put it in place.
+         *
+         * Also, an unary operation is allowed to deal with a null root expression,
+         * since it doesn't use it!
+         */
+            m_opStack.peekFirst().op.setSubExpression(op);
+            m_opStack.addFirst(new ExpressionStackContainer(m_level, op));
+        }
+
+        private static BinaryOperation getBinaryOpForSymbol(String text) {
+            if (text.equals("+")) {
+                return BinaryOperation.Addition;
+            } else if (text.equals("-")) {
+                return BinaryOperation.Minus;
+            } else if (text.equals("*")) {
+                return BinaryOperation.Multiplication;
+            } else if (text.equals("/")) {
+                return BinaryOperation.Division;
+            } else if (text.equals("^")) {
+                return BinaryOperation.Exponentiation;
+            } else if (text.equals(">")) {
+                return BinaryOperation.GreaterThen;
+            } else if (text.equals(">=")) {
+                return BinaryOperation.GreaterThenEqual;
+            } else if (text.equals("<")) {
+                return BinaryOperation.LessThen;
+            } else if (text.equals("<=")) {
+                return BinaryOperation.LessThenEqual;
+            } else if (text.equals("==")) {
+                return BinaryOperation.Equals;
+            } else if (text.equals("~=")) {
+                return BinaryOperation.NotEquals;
+            } else if (text.equals("&&")) {
+                return BinaryOperation.BooleanAnd;
+            } else if (text.equals("||")) {
+                return BinaryOperation.BooleanOr;
+            } else {
+                throw new IllegalArgumentException("No such binary matlab operation defined (" + text + ")!");
+            }
+        }
+
+        private static UnaryOperation getUnaryOpForSymbol(String text) {
+            if (text.equals("~")) {
+                return UnaryOperation.Negation;
+            } else if (text.equals("-")) {
+                return UnaryOperation.Minus;
+            } else {
+                throw new IllegalArgumentException("No such unary matlab operation defined (" + text + ")!");
+            }
+        }
+
+        @Override
+        public Expression getSubExpression() {
+            return m_rootExpression;
+        }
+
+        @Override
+        public void setSubExpression(Expression subExpression) {
+            m_rootExpression = subExpression;
+        }
+
+
+        @Override
+        public void enterE0(E0Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void enterE1(E1Context ctx) {
+            incrementLevel();
+            if (ctx.LOG_OR().size() > 0) {
+                enqueHiddenOp(BinaryOperation.BooleanOr, ctx.LOG_OR().size());
+            }
+        }
+
+        @Override
+        public void enterE2(E2Context ctx) {
+            incrementLevel();
+            if (ctx.LOG_AND().size() > 0) {
+                enqueHiddenOp(BinaryOperation.BooleanAnd, ctx.LOG_AND().size());
+            }
+        }
+
+        @Override
+        public void enterE3(E3Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void enterE4(E4Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void enterE5(E5Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void enterE6(E6Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void enterE7(E7Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void enterE8(E8Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void enterE9(E9Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void enterE10(E10Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void enterE11(E11Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void exitE0(E0Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE1(E1Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE2(E2Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE3(E3Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE4(E4Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE5(E5Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE6(E6Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE7(E7Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE8(E8Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE9(E9Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE10(E10Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE11(E11Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void enterG1(G1Context ctx) {
+            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
+        }
+
+        @Override
+        public void enterG2(G2Context ctx) {
+            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
+        }
+
+        @Override
+        public void enterG3(G3Context ctx) {
+            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
+        }
+
+        @Override
+        public void enterG4(G4Context ctx) {
+            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
+        }
+        @Override
+        public void enterPrefix_operator(Prefix_operatorContext ctx) {
+            addPrefixUnaryOperation(new ExpressionUnaryOperation(getUnaryOpForSymbol(ctx.getText()), null));
+        }
+
+        @Override
+        public void exitPrefix_operator(Prefix_operatorContext ctx) {
+        }
+
+        @Override
+        public void enterLiteral_number(Literal_numberContext ctx) {
+            addExpressionValue(new Literal(ctx.getText()));
+        }
+
+        @Override
+        public void enterId_plus_indexers(Id_plus_indexersContext ctx) {
+            addExpressionValue(m_variableParser.get(ctx.getText()));
+        }
+
+        public Expression m_rootExpression;
+        private int m_level = 0;
+        private Map<String, Variable> m_variableParser;
+
+        private static class ExpressionStackContainer {
+
+            public int level;
+            public ExpressionWithSubExpression op;
+
+            public ExpressionStackContainer(int level, ExpressionWithSubExpression op) {
+                this.level = level;
+                this.op = op;
+            }
+        }
+        Deque<ExpressionStackContainer> m_opStack = new ArrayDeque<ExpressionStackContainer>();
+
+        private static class HiddenOpStackContainer {
+
+            public int level, count;
+            public BinaryOperation op;
+
+            public HiddenOpStackContainer(int level, BinaryOperation op, int count) {
+                this.level = level;
+                this.op = op;
+                this.count = count;
+            }
+        }
+        Deque<HiddenOpStackContainer> m_hiddenOpStack = new ArrayDeque<HiddenOpStackContainer>();
+    }
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/PVSSimpleParser.g4

+grammar PVSSimpleParser;
+
+/* This is a simple PVS syntax parser.  It is designed to be able to parser simple math statements from PVS, instead of
+a full blown parser that could be used to re-implement PVS.  This file is roughly based on MatlabParser.g4, without all
+the extra pieces from it.  It is also modified to make the associated pieces in Java simpler. */
+
+//
+// ===============================
+//
+
+// a precedence hierarchy for parsing expressions
+
+// these are groups of operators that have equivalent precedences
+g1: IMPLIES;
+g2: LOG_OR;
+g3: LOG_AND;
+g4: NEG;
+g5: ( NEQ | EQ | GRTE | GRT | LSTE | LST );
+g6: ( PLUS | MINUS );
+g7: ( LEFTDIV | TIMES );
+g8: MINUS;
+g9: EXPONENTIATION;
+
+// the hierarchy is defined from LOWEST to HIGHEST priority.
+
+expression : e0;
+
+e0	: e1 g1 e0 | e1; // Implies
+e1	: e2 g2 e1 | e2; // Logic OR
+e2	: e3 g3 e2 | e3; // Logc AND
+e3	: g4 e4 | e4; // Logc NOT
+e4	: e4 g5 e5 | e5; // Comparison
+e5	: e5 g6 e6 | e6; // Addition/Subtraction
+e6	: e6 g7 e7 | e7; // Multiplication/Division
+e7	: g8 e8 | e8; // Unary Minus
+e8	: e8 g9 e9 | e9; // note: in PVS, exponentiation is left-associative
+e9	: unary_expression;
+
+unary_expression
+	: base_expression #BASE_EXPRESIION
+	| LPAREN expression RPAREN # PARENS_EXPRESSION
+	;
+
+base_expression
+	: id
+	| literal_number
+	;
+
+literal_number
+        : INT
+        | FLOAT
+        ;
+
+id:	i1=ID;
+
+//
+// operators and assignments
+//
+
+IMPLIES : '=>';
+LOG_OR	: 'OR';
+LOG_AND	: 'AND';
+LSTE	: '<=';
+GRTE	: '>=';
+NEQ	: '/=';
+
+EQ	: '=';
+
+NEG	:   'NOT';
+
+LST	: '<';
+GRT	: '>';
+
+
+PLUS	: '+';
+MINUS	: '-';
+TIMES	: '*';
+LEFTDIV	: '/';
+
+EXPONENTIATION: '^';
+
+
+LPAREN	: '(';
+RPAREN	: ')';
+
+ID	: [a-zA-Z][a-zA-Z0-9]*; //Variable identifier.  Start with letter, then alpha numerical allowed.
+
+INT	: '0'..'9'+ ;
+
+FLOAT
+	: ('0'..'9')+ '.' ('0'..'9')* EXPONENT?
+	| '.' ('0'..'9')+ EXPONENT?
+	| ('0'..'9')+ EXPONENT
+	;
+
+WS
+	: ( ' '
+        | '\t'
+        | '\n'
+        ) -> skip
+	;
+
+fragment
+EXPONENT
+	: ('e'|'E') ('+'|'-')? ('0'..'9')+ ;

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/PVSSimpleParser.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.parsers;
+
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BinaryOperation;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Expression;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionBinaryOperation;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionUnaryOperation;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionValue;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionWithSubExpression;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Literal;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.UnaryOperation;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Variable;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableCollection;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E0Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E1Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E2Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E3Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E4Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E5Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E6Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E7Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E8Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E9Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G1Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G2Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G3Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G4Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G5Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G6Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G7Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G8Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G9Context;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.IdContext;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.Literal_numberContext;
+import org.antlr.v4.runtime.ANTLRInputStream;
+import org.antlr.v4.runtime.CommonTokenStream;
+import org.antlr.v4.runtime.tree.ParseTree;
+import org.antlr.v4.runtime.tree.ParseTreeWalker;
+
+import java.util.ArrayDeque;
+import java.util.Deque;
+import java.util.Map;
+
+/**
+ *
+ * @author matthew
+ */
+final public class PVSSimpleParser {
+
+    private PVSSimpleParser() {
+    }
+
+    public static Expression parsePVSCode(VariableCollection variableListing, String pvsCode) {
+        // create a CharStream that reads from standard input
+        ANTLRInputStream input = new ANTLRInputStream(pvsCode + "\n");
+
+        // create a lexer that feeds off of input CharStream
+        PVSSimpleParserLexer lexer = new PVSSimpleParserLexer(input);
+
+        // create a buffer of tokens pulled from the lexer
+        CommonTokenStream tokens = new CommonTokenStream(lexer);
+
+        // create a parser that feeds off the tokens buffer
+        PVSSimpleParserParser parser = new PVSSimpleParserParser(tokens);
+
+        ParseTree tree = parser.expression();
+        ParseTreeWalker walker = new ParseTreeWalker();
+        PVSParserToExpressions listener = new PVSParserToExpressions(variableListing.getVariablesAndEnumeratedValues());
+        walker.walk(listener, tree);
+
+        return listener.m_rootExpression;
+    }
+
+    private static class PVSParserToExpressions extends PVSSimpleParserBaseListener implements ExpressionWithSubExpression {
+
+        PVSParserToExpressions(Map<String, Variable> variableListing) {
+            m_variableParser = variableListing;
+            m_opStack.addFirst(new ExpressionStackContainer(0, this));
+        }
+
+        private void incrementLevel() {
+            this.m_level++;
+        }
+
+        private void decrementLevel() {
+            this.m_level--;
+            if (!m_hiddenOpStack.isEmpty() && m_hiddenOpStack.peekFirst().level == m_level) {
+                // We have a hidden op here.  The normal methods won't find it, so make use of it!
+                HiddenOpStackContainer hiddenOp = m_hiddenOpStack.peekFirst();
+                addExpressionBinaryOperation(new ExpressionBinaryOperation(null, hiddenOp.op, null));
+                if (--hiddenOp.count == 0) {
+                    m_hiddenOpStack.removeFirst();
+                }
+            }
+
+            if (!m_opStack.isEmpty() && m_opStack.peekFirst().level > m_level) {
+                m_opStack.removeFirst();
+            }
+        }
+
+        private void enqueHiddenOp(BinaryOperation op, int count) {
+            m_hiddenOpStack.addFirst(new HiddenOpStackContainer(m_level, op, count));
+        }
+
+        private void addExpressionValue(ExpressionValue expressionValue) {
+            m_opStack.peekFirst().op.setSubExpression(expressionValue);
+        }
+
+        private void addExpressionBinaryOperation(ExpressionBinaryOperation op) {
+            if (m_rootExpression == null) {
+                throw new IllegalStateException("It should not be possible to have"
+                        + "an op where the left hand side is a null expression!");
+            } else {
+                if (m_opStack.peekFirst().level >= m_level) { //This current op happens after the root expression op.  Pull it up.
+                    op.setLHS((Expression) m_opStack.removeFirst().op);
+                    m_opStack.peekFirst().op.setSubExpression(op);
+                } else { //This op happens before.  Push it down the tree.
+                    op.setLHS(m_opStack.peekFirst().op.getSubExpression());
+                    m_opStack.peekFirst().op.setSubExpression(op);
+                }
+                m_opStack.addFirst(new ExpressionStackContainer(m_level, op));
+            }
+        }
+
+        private void addPrefixUnaryOperation(ExpressionUnaryOperation op) {
+        /* Unlike Binary operations, unary operations just always insert
+         * themselves into the operation stack exactly where they appear.
+         * The whole left hand side handling never happens, since there is no
+         * left hand side.  So just put it in place.
+         *
+         * Also, an unary operation is allowed to deal with a null root expression,
+         * since it doesn't use it!
+         */
+            m_opStack.peekFirst().op.setSubExpression(op);
+            m_opStack.addFirst(new ExpressionStackContainer(m_level, op));
+        }
+
+        private static BinaryOperation getBinaryOpForSymbol(String text) {
+            if (text.equals("+")) {
+                return BinaryOperation.Addition;
+            } else if (text.equals("-")) {
+                return BinaryOperation.Minus;
+            } else if (text.equals("*")) {
+                return BinaryOperation.Multiplication;
+            } else if (text.equals("/")) {
+                return BinaryOperation.Division;
+            } else if (text.equals("^")) {
+                return BinaryOperation.Exponentiation;
+            } else if (text.equals(">")) {
+                return BinaryOperation.GreaterThen;
+            } else if (text.equals(">=")) {
+                return BinaryOperation.GreaterThenEqual;
+            } else if (text.equals("<")) {
+                return BinaryOperation.LessThen;
+            } else if (text.equals("<=")) {
+                return BinaryOperation.LessThenEqual;
+            } else if (text.equals("=")) {
+                return BinaryOperation.Equals;
+            } else if (text.equals("/=")) {
+                return BinaryOperation.NotEquals;
+            } else if (text.equals("=>")) {
+                return BinaryOperation.Implies;
+            } else if (text.equals("AND")) {
+                return BinaryOperation.BooleanAnd;
+            } else if (text.equals("OR")) {
+                return BinaryOperation.BooleanOr;
+            } else {
+                throw new IllegalArgumentException("No such binary PVS operation defined (" + text + ")!");
+            }
+        }
+
+        @Override
+        public Expression getSubExpression() {
+            return m_rootExpression;
+        }
+
+        @Override
+        public void setSubExpression(Expression subExpression) {
+            m_rootExpression = subExpression;
+        }
+
+
+        @Override
+        public void enterE0(E0Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void enterE1(E1Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void enterE2(E2Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void enterE3(E3Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void enterE4(E4Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void enterE5(E5Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void enterE6(E6Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void enterE7(E7Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void enterE8(E8Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void enterE9(E9Context ctx) {
+            incrementLevel();
+        }
+
+        @Override
+        public void exitE0(E0Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE1(E1Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE2(E2Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE3(E3Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE4(E4Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE5(E5Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE6(E6Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE7(E7Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE8(E8Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void exitE9(E9Context ctx) {
+            decrementLevel();
+        }
+
+        @Override
+        public void enterG1(G1Context ctx) {
+            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
+        }
+
+        @Override
+        public void enterG2(G2Context ctx) {
+            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
+        }
+
+        @Override
+        public void enterG3(G3Context ctx) {
+            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
+        }
+
+        @Override
+        public void enterG4(G4Context ctx) {
+            addPrefixUnaryOperation(new ExpressionUnaryOperation(UnaryOperation.Negation, null)); // This is always negation.
+        }
+
+        @Override
+        public void enterG5(G5Context ctx) {
+            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
+        }
+
+        @Override
+        public void enterG6(G6Context ctx) {
+            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
+        }
+
+        @Override
+        public void enterG7(G7Context ctx) {
+            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
+        }
+
+        @Override
+        public void enterG8(G8Context ctx) {
+            addPrefixUnaryOperation(new ExpressionUnaryOperation(UnaryOperation.Minus, null)); // This is always minus.
+        }
+
+        @Override
+        public void enterG9(G9Context ctx) {
+            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
+        }
+
+        @Override
+        public void enterLiteral_number(Literal_numberContext ctx) {
+            addExpressionValue(new Literal(ctx.getText()));
+        }
+
+        @Override
+        public void enterId(IdContext ctx) {
+            addExpressionValue(m_variableParser.get(ctx.getText()));
+        }
+
+        public Expression m_rootExpression;
+        private int m_level = 0;
+        private Map<String, Variable> m_variableParser;
+
+        private static class ExpressionStackContainer {
+
+            public int level;
+            public ExpressionWithSubExpression op;
+
+            public ExpressionStackContainer(int level, ExpressionWithSubExpression op) {
+                this.level = level;
+                this.op = op;
+            }
+        }
+        Deque<ExpressionStackContainer> m_opStack = new ArrayDeque<ExpressionStackContainer>();
+
+        private static class HiddenOpStackContainer {
+
+            public int level, count;
+            public BinaryOperation op;
+
+            public HiddenOpStackContainer(int level, BinaryOperation op, int count) {
+                this.level = level;
+                this.op = op;
+                this.count = count;
+            }
+        }
+        Deque<HiddenOpStackContainer> m_hiddenOpStack = new ArrayDeque<HiddenOpStackContainer>();
+    }
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/VariableParser.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.parsers;
+
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BooleanVariableType;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Expression;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.FixedPointVariableType;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.RealVariableType;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Variable;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableCollection;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParserParser.Bool_typeContext;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParserParser.DefaulttypeContext;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParserParser.Fixed_typeContext;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParserParser.Real_typeContext;
+import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParserParser.VarContext;
+import java.util.HashMap;
+import java.util.Map;
+
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableType;
+import org.antlr.v4.runtime.ANTLRInputStream;
+import org.antlr.v4.runtime.CommonTokenStream;
+import org.antlr.v4.runtime.misc.NotNull;
+import org.antlr.v4.runtime.tree.ParseTree;
+import org.antlr.v4.runtime.tree.ParseTreeWalker;
+import org.antlr.v4.runtime.tree.TerminalNode;
+
+/**
+ *
+ * @author Matthew Dawson
+ */
+final public class VariableParser {
+
+    public VariableCollection parseVariables(String variables) {
+        // create a CharStream that reads from standard input
+        ANTLRInputStream input = new ANTLRInputStream(variables) {
+
+            @Override
+            public int LA(int i) {
+                return Character.toLowerCase(super.LA(i));
+            }
+
+        };
+
+        // create a lexer that feeds off of input CharStream
+        VariableParserLexer lexer = new VariableParserLexer(input);
+
+        // create a buffer of tokens pulled from the lexer
+        CommonTokenStream tokens = new CommonTokenStream(lexer);
+
+        // create a parser that feeds off the tokens buffer
+        VariableParserParser parser = new VariableParserParser(tokens);
+
+        ParseTree tree = parser.varlist();
+        ParseTreeWalker walker = new ParseTreeWalker();
+        VariablesParserToVariables listener = new VariablesParserToVariables();
+        walker.walk(listener, tree);
+
+        return listener.m_variableCollection;
+    }
+
+    public void addCustomType(String typeName, VariableType type) {
+        m_customTypes.put(typeName, type);
+    }
+
+    private final Map<String, VariableType> m_customTypes = new HashMap<String, VariableType>();
+
+    private class VariablesParserToVariables extends VariableParserParserBaseListener {
+        private String currentName;
+        private VariableType currentType;
+        private limitingExpressionData currentLimitingExpression;
+
+        @Override
+        public void enterVar(VarContext ctx) {
+            currentName = ctx.ID().getText();
+        }
+
+        @Override
+        public void enterDefaulttype(DefaulttypeContext ctx) {
+            currentType = new RealVariableType();
+        }
+
+        @Override
+        public void enterReal_type(Real_typeContext ctx) {
+            currentType = new RealVariableType();
+        }
+
+        @Override
+        public void enterBool_type(Bool_typeContext ctx) {
+            currentType = new BooleanVariableType();
+        }
+
+        @Override
+        public void enterUnknown_type(@NotNull VariableParserParser.Unknown_typeContext ctx) {
+            currentType = m_customTypes.get(ctx.UNKNOWN_TYPE().getText());
+            if (currentType == null) { // Assume this unknown.  For now, pretend a real is wanted.
+                currentType = new RealVariableType();
+            }
+        }
+
+        @Override
+        public void enterSubtype_var(@NotNull VariableParserParser.Subtype_varContext ctx) {
+            currentLimitingExpression = new limitingExpressionData();
+            currentLimitingExpression.variableName = ctx.ID().getText();
+        }
+
+        @Override
+        public void enterPvs_expr(@NotNull VariableParserParser.Pvs_exprContext ctx) {
+            currentLimitingExpression.expression = ctx.PVS_EXPR().getText();
+        }
+
+        @Override
+        public void enterFixed_type(Fixed_typeContext ctx) {
+            boolean signed = (ctx.NAT(0).getText().equals("0"))?false:true;
+            int digits = Integer.parseInt(ctx.NAT(1).getText());
+            int fractionPart = 0;
+            TerminalNode fractionNode;
+            if ((fractionNode = ctx.NAT(2)) != null) {
+                fractionPart = Integer.parseInt(fractionNode.getText());
+            }
+            currentType = new FixedPointVariableType(signed, digits, fractionPart);
+        }
+
+        @Override
+        public void exitVar(VarContext ctx) {
+            m_variables.put(currentName, new Variable(currentName, currentType));
+            if (currentLimitingExpression != null) {
+                m_variableLimitingExpressions.put(currentName, currentLimitingExpression);
+            }
+            currentName = null;
+            currentType = null;
+            currentLimitingExpression = null;
+        }
+
+        @Override
+        public void exitVarlist(@NotNull VariableParserParser.VarlistContext ctx) {
+            m_variableCollection = new VariableCollection(m_variables);
+
+            for(Map.Entry<String, limitingExpressionData> limitingExpression : m_variableLimitingExpressions.entrySet()) {
+                String subtypeVar = limitingExpression.getValue().variableName;
+                String subtypeExpression = limitingExpression.getValue().expression;
+                if (m_variables.containsKey(limitingExpression.getValue().variableName)) {
+                    throw new IllegalStateException("Reused variable name for subtype declaration!");
+                }
+                // Get the variable we are working on, and use it for the variable used in the subtype expression.  This
+                // effectively means the expression can just be emitted into the verification system to limit it.
+                m_variables.put(subtypeVar, m_variables.get(limitingExpression.getKey()));
+
+                m_variables.get(limitingExpression.getKey()).type().setSubtypePredicate(PVSSimpleParser.parsePVSCode(m_variableCollection, subtypeExpression));
+
+                // Undo the variables hack, to avoid having unused variables bleed into the verification scripts!
+                m_variables.remove(subtypeVar);
+            }
+        }
+
+        private Map<String, Variable>  m_variables = new HashMap<String, Variable>();
+        public VariableCollection m_variableCollection;
+
+        private Map<String, limitingExpressionData> m_variableLimitingExpressions = new HashMap<String, limitingExpressionData>();
+    }
+    private static class limitingExpressionData {
+        public String expression;
+        public String variableName;
+    }
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/VariableParserLexer.g4

+lexer grammar VariableParserLexer;
+
+tokens { ID }
+
+fragment IDRule: [a-zA-Z][a-zA-Z0-9]*; //Variable identifier.  Start with letter, then alpha numerical allowed.
+
+REGULAR_ID: IDRule -> type(ID), pushMode(VARIABLE_TYPE);
+
+fragment WS : [ \t\r\n]+; // skip spaces, tabs, newlines
+WS1: WS -> skip ;
+
+
+mode PVS_EXPR_MODE;
+PVS_EXPR: ~[\{\}]+ -> popMode;
+
+
+mode VARIABLE_TYPE;
+VAR_SEPARATOR: ',' -> popMode;
+COLON: ':';
+BOOL_TYPE: 'bool';
+REAL_TYPE: 'real';
+FIXEDT: 'fixedt' -> pushMode(FIXED_TYPE);
+UNKNOWN_TYPE: [a-zA-Z_]+;
+
+OPEN_SUBTYPE: '{' -> pushMode(ID_FETCH);
+PVS_EXPR_BEGIN: '|' -> pushMode(PVS_EXPR_MODE);
+CLOSE_SUBTYPE: '}';
+
+WS2: WS -> skip;
+
+mode FIXED_TYPE;
+NAT_SEPARATOR: ',';
+OPEN_BRACKET: '(';
+CLOSE_BRACKET: ')' -> popMode;
+NAT: [0-9]+;
+
+WS3: WS -> skip;
+
+
+mode ID_FETCH;
+SUBTYPE_ID: IDRule -> type(ID), popMode;
+
+WS4: WS -> skip;

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/VariableParserParser.g4

+parser grammar VariableParserParser;
+options { tokenVocab=VariableParserLexer; }
+
+varlist: var (VAR_SEPARATOR var)*; //Build list of variables
+var:    ID vartype;
+vartype: ':' type_info
+       | defaulttype;
+
+defaulttype: ;
+
+type_info: simple_type_info
+         | '{' subtype '}';
+
+subtype: subtype_var '|' pvs_expr;
+subtype_var:    ID subtype_vartype;
+subtype_vartype: ':' simple_type_info
+       | defaulttype;
+pvs_expr: PVS_EXPR;
+
+simple_type_info: bool_type
+         | real_type
+         | fixed_type
+         | unknown_type;
+
+bool_type: BOOL_TYPE;
+
+real_type: 'real';
+
+fixed_type: 'fixedt' '(' NAT NAT_SEPARATOR NAT ')'
+          | 'fixedt' '(' NAT NAT_SEPARATOR NAT NAT_SEPARATOR NAT ')';
+
+unknown_type: UNKNOWN_TYPE;

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/smtlibchecker/CheckerRunner.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.smtlibchecker;
+
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.SMTLIBGenerator;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Variable;
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableCollection;
+import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchcialGridCheckerWalkerGenerator;
+import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchicalGrid;
+import org.antlr.v4.runtime.ANTLRInputStream;
+import org.antlr.v4.runtime.CommonTokenStream;
+import org.antlr.v4.runtime.misc.NotNull;
+import org.antlr.v4.runtime.tree.ParseTree;
+import org.antlr.v4.runtime.tree.ParseTreeWalker;
+
+import java.io.BufferedReader;
+import java.io.IOException;
+import java.io.InputStreamReader;
+import java.io.OutputStreamWriter;
+import java.io.Reader;
+import java.io.UnsupportedEncodingException;
+import java.io.Writer;
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+
+/**
+ *
+ * @author Matthew Dawson <matthew@mjdsystems.ca>
+ */
+final public class CheckerRunner {
+    public static List<CheckerRunnerResult> RunZ3(HierarchicalGrid grid, VariableCollection vars) {
+        List<CheckerRunnerResult> ret = new ArrayList<CheckerRunnerResult>();
+
+        // Get the queries
+        HierarchicalGridSMTLIBGenerator queryGenerator = new HierarchicalGridSMTLIBGenerator(vars);
+        HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(grid, queryGenerator);
+
+        // Start Z3
+        ProcessBuilder pb;
+        Process p;
+        try {
+            pb = new ProcessBuilder("z3", "-smt2", "-in");
+            p = pb.start();
+        } catch(IOException ex) {
+            throw new RuntimeException("Failed to start Z3!", ex);
+        }
+
+        // Input/Output refer to the direction from Z3's pov.  So output is Z3's stdout.
+        BufferedReader z3Output;
+        Writer z3Input;
+        try {
+            // Sigh ... Java has horrible naming conversions here ...
+            z3Output = new BufferedReader(new InputStreamReader(p.getInputStream(), "ISO-8859-1"));
+            z3Input = new OutputStreamWriter(p.getOutputStream());
+        } catch(UnsupportedEncodingException ex) {
+            throw new RuntimeException("Failed to get ISO-8859-1 charset for talking to Z3!", ex);
+        }
+
+        StringBuilder GetValueRequestBuilder = new StringBuilder();
+        GetValueRequestBuilder.append("(get-value (");
+        for(Variable var:vars.getVariables().values()) {
+            GetValueRequestBuilder.append(var.name()).append(' ');
+        }
+        GetValueRequestBuilder.append("))\n");
+        String GetValueRequestString = GetValueRequestBuilder.toString();
+
+        try {
+            String VarDef = new SMTLIBGenerator().GenerateVariablesDeclaration(vars);
+            z3Input.write(VarDef);
+            for(String query : queryGenerator.getFinalQueries()) {
+                z3Input.write("(push 1)");
+                z3Input.write(query);
+                z3Input.write("(check-sat)\n");
+                z3Input.flush();
+
+                String res = z3Output.readLine();
+                if(res.equals("sat")) { // Failed query.  Get a the result.
+                    z3Input.write(GetValueRequestString);
+                    z3Input.flush();
+
+                    CheckerRunnerResult result = new CheckerRunnerResult();
+                    result.Query = query;
+                    result.SampleValues = parseSMTLIBOutput(z3Output);
+                    ret.add(result);
+                } else if(res.equals("unknown")) {
+                    // Z3 failed to prove.  Throw a failure to check for now.
+                    CheckerRunnerResult result = new CheckerRunnerResult();
+                    result.Query = query;
+                    result.SampleValues = null;
+                    ret.add(result);
+                } else if(!res.equals("unsat")) {
+                    // Something went wrong
+                    throw new IllegalStateException("Z3 outputed something wrong (" + res + ")!");
+                }
+
+                z3Input.write("(pop 1)\r");
+            }
+        } catch(IOException ex) {
+            throw new RuntimeException("Something bad happened ...", ex);
+        } finally {
+            try {
+                z3Input.write("(exit)\n");
+                z3Input.flush();
+
+                p.destroy();
+                z3Input.close();
+                z3Output.close();
+            } catch(Exception e) {
+                // Don't care here, so just print it out.
+                System.out.println(e);
+            }
+        }
+
+        return ret;
+    }
+
+    private static Map<String, String> parseSMTLIBOutput(Reader reader) throws IOException {
+        if(reader.markSupported() == false) {
+            throw new IllegalArgumentException("Reader must support marks!");
+        }
+        final Map<String, String> ret = new HashMap<String, String>();
+
+        StringBuilder input = new StringBuilder();
+
+        int bracketMismatch = 1; // This starts with a (, so we immediately have a a mismatch.
+        char nextChar = getNextChar(reader);
+        if (nextChar != '(') { // Should start with a ( for output.
+            throw new IllegalStateException("Bad input, wanted a ( to start, got " + nextChar);
+        }
+        input.append(nextChar);
+        while(bracketMismatch != 0) {
+            nextChar = getNextChar(reader);
+            switch (nextChar) {
+                case '(':
+                    bracketMismatch++;
+                    break;
+                case ')':
+                    bracketMismatch--;
+                    break;
+            }
+            input.append(nextChar);
+        }
+
+        // Finally, clear the new line, so the output is now clear.
+        do {
+            reader.mark(5);
+            nextChar = getNextChar(reader);
+        } while(isWhitespace(nextChar) && nextChar != '\n');
+        if(!isWhitespace(nextChar)) {
+            reader.reset();
+        }
+
+        ANTLRInputStream antlrInput = new ANTLRInputStream(input.toString());
+
+        // create a lexer that feeds off of input CharStream
+        SMTLibOutParserLexer lexer = new SMTLibOutParserLexer(antlrInput);
+
+        // create a buffer of tokens pulled from the lexer
+        CommonTokenStream tokens = new CommonTokenStream(lexer);
+
+        // create a parser that feeds off the tokens buffer
+        SMTLibOutParserParser parser = new SMTLibOutParserParser(tokens);
+
+        ParseTree tree = parser.valuelist();
+        ParseTreeWalker walker = new ParseTreeWalker();
+        SMTLibOutParserListener listener = new SMTLibOutParserBaseListener() {
+            @Override
+            public void enterValue(@NotNull SMTLibOutParserParser.ValueContext ctx) {
+                id = ctx.ID().getText();
+                value = "";
+            }
+
+            @Override
+            public void enterNegative(@NotNull SMTLibOutParserParser.NegativeContext ctx) {
+                value = "(- ";
+            }
+
+            @Override
+            public void exitSingle(@NotNull SMTLibOutParserParser.SingleContext ctx) {
+                value += ctx.getText();
+            }
+
+            @Override
+            public void exitFraction(@NotNull SMTLibOutParserParser.FractionContext ctx) {
+                value += "(" + ctx.RATIONAL(0).getText() + " / " + ctx.RATIONAL(1).getText() + ")";
+            }
+
+            @Override
+            public void exitNegative(@NotNull SMTLibOutParserParser.NegativeContext ctx) {
+                value += ')';
+            }
+
+            @Override
+            public void exitExpr(@NotNull SMTLibOutParserParser.ExprContext ctx) {
+                ret.put(id, value);
+            }
+
+            String id = "";
+            String value;
+        };
+        walker.walk(listener, tree);
+        return ret;
+    }
+
+    private static char getNextChar(Reader reader) throws IOException {
+        char[] c = new char[1];
+        reader.read(c);
+        return c[0];
+    }
+
+    private static boolean isWhitespace(char toTest) {
+        if(toTest == ' ' ||
+                toTest == '\n' ||
+                toTest == '\r' ||
+                toTest == '\t') {
+            return true;
+        }
+        return false;
+    }
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/smtlibchecker/CheckerRunnerResult.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.smtlibchecker;
+
+import java.util.Map;
+
+/**
+ * @author Matthew Dawson <matthew@mjdsystems.ca>
+ */
+final public class CheckerRunnerResult {
+    public String Query;
+    public Map<String, String> SampleValues;
+
+    public String GenerateMatlabVariableDeclarations() {
+        StringBuilder ret = new StringBuilder();
+        for(Map.Entry<String, String> var: SampleValues.entrySet()) {
+            ret.
+                    append(var.getKey()).
+                    append(" = ").
+                    append(var.getValue()).
+                    append(";\n");
+        }
+        return ret.toString();
+    }
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/smtlibchecker/HierarchicalGridSMTLIBGenerator.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.smtlibchecker;
+
+import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BooleanVariableType;
+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.SMTLIBGenerator;
+import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.Cell;
+import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchcialGridCheckerGenerator;
+import org.apache.commons.lang3.StringUtils;
+
+import java.util.ArrayDeque;
+import java.util.ArrayList;
+import java.util.Deque;
+import java.util.List;
+import java.util.Map;
+
+/**
+ *
+ * @author Matthew Dawson <matthew@mjdsystems.ca>
+ */
+final public class HierarchicalGridSMTLIBGenerator implements HierarchcialGridCheckerGenerator {
+
+    public HierarchicalGridSMTLIBGenerator(VariableCollection variableDefinitions) {
+        m_variableDefinitions = variableDefinitions;
+    }
+
+    private String generateQueryPrefix() {
+        if (!m_parentCellsCVC3Code.isEmpty()){
+            String output = "(and ";
+            output += StringUtils.join(m_parentCellsCVC3Code, " ") + " ";
+            return output;
+        }
+        return "(and true ";
+    }
+
+    private void outputCells() {
+        // First is disjoint testing.
+        m_output += "(push 1)\n";
+
+        String query = "(assert ";
+        query += generateQueryPrefix();
+        if (m_currentDisjointQueries.isEmpty()) {
+            query += "false";
+        } else if (m_currentDisjointQueries.size() == 1) {
+            query += m_currentDisjointQueries.get(0);
+        } else {
+            query += "(or " + StringUtils.join(m_currentDisjointQueries, '\n') + ")";
+        }
+        query += "))";
+        m_queries.add(query);
+        m_output += query + "\n";
+
+        m_output += "(check-sat)\n(pop 1)\n";
+
+        // Next is complete.
+        m_output += "(push 1)\n";
+
+        query = "(assert ";
+        query += generateQueryPrefix();
+        query += "(not ";
+        if (m_currentCompleteQueries.isEmpty()) {
+            query += "true";
+        } else if (m_currentCompleteQueries.size() == 1) {
+            query +=  m_currentCompleteQueries.get(0);
+        } else {
+            query += "(or " + StringUtils.join(m_currentCompleteQueries, " ") + ")";
+        }
+        query += ")))";
+        m_queries.add(query);
+        m_output += query + "\n";
+
+        m_output += "(check-sat)\n(pop 1)\n";
+
+        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 = "(and " + otherCellCode  + " " + 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;
+
+    String m_output = "";
+    List<String> m_queries = new ArrayList<String>();
+
+    // To fix properly.
+    VariableCollection m_variableDefinitions;
+    static BooleanVariableType m_booleanType = new BooleanVariableType();
+    SMTLIBGenerator m_CVC3Generator = new SMTLIBGenerator();
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/smtlibchecker/SMTLibOutParser.g4

+grammar SMTLibOutParser;
+
+valuelist: '(' value+ ')'; //Build list of variables
+value:     '(' ID expr ')';
+
+expr: single |
+      fraction |
+      negative;
+
+negative: '(-' fraction ')' |
+          '(-' single ')';
+single: RATIONAL;
+fraction: '(/' RATIONAL RATIONAL ')';
+
+ID: [a-zA-Z][a-zA-Z0-9]*; //Variable identifier.  Start with letter, then alpha numerical allowed.
+RATIONAL: [0-9]+('.'[0-9]+)?;
+WS : [ \t\r\n]+ -> skip ; // skip spaces, tabs, newlines

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/tablularexpression/Cell.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression;
+
+/**
+ *
+ * @author Matthew Dawson <matthew@mjdsystems.ca>
+ */
+public class Cell {
+    Cell() {}
+    Cell(String initialContents) {
+        m_contents = initialContents;
+    }
+    
+    public void setContents(String contents) {
+        m_contents = contents;
+    }
+    
+    public String contents() {
+        return m_contents;
+    }
+    
+    private String m_contents;
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/tablularexpression/HierarchcialGridCheckerGenerator.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.tablularexpression;
+
+/**
+ *
+ * @author Matthew Dawson <matthew@mjdsystems.ca>
+ */
+public interface HierarchcialGridCheckerGenerator {
+    void descendIntoGridFromCell(Cell cell);
+    void ascendFromGrid();
+    
+    void handleLeafCell(Cell cell);
+    void handleEdgeCell(Cell cell);
+    
+    String getFinalString();
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/tablularexpression/HierarchcialGridCheckerWalkerGenerator.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.tablularexpression;
+
+import java.util.List;
+
+/**
+ *
+ * @author Matthew Dawson <matthew@mjdsystems.ca>
+ */
+public class HierarchcialGridCheckerWalkerGenerator {
+    
+    private static void HandleGrid(SubHierarchyFetcher grid, HierarchcialGridCheckerGenerator generator) {
+        List<HierarchicalCell> cells = grid.getSubHiearchy();
+        for (int i = 0; i < cells.size(); ++i) {
+            HierarchicalCell cell = cells.get(i);
+            
+            if (cell.getSubHiearchy().isEmpty()) {
+                generator.handleLeafCell(cell);
+            } else {
+                generator.handleEdgeCell(cell);
+            }
+        }
+        
+        for (int i = 0; i < cells.size(); ++i) {
+            HierarchicalCell cell = cells.get(i);
+            
+            if (!cell.getSubHiearchy().isEmpty()) {
+                generator.descendIntoGridFromCell(cell);
+                HandleGrid(cell, generator);
+                generator.ascendFromGrid();
+            }
+        }
+    }
+    
+    public static String GenerateCheckerFromGrid(HierarchicalGrid grid, HierarchcialGridCheckerGenerator generator) {
+        HandleGrid(grid, generator);
+        return generator.getFinalString();
+    }
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/tablularexpression/HierarchicalCell.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression;
+
+import java.util.ArrayList;
+import java.util.List;
+
+/**
+ *
+ * @author Matthew Dawson <matthew@mjdsystems.ca>
+ */
+public class HierarchicalCell extends Cell implements SubHierarchyFetcher {
+    public HierarchicalCell() {}
+    public HierarchicalCell(String initialContents) {
+        super(initialContents);
+    }
+
+    @Override
+    public List<HierarchicalCell> getSubHiearchy() {
+        return m_subHiearchy;
+    }
+    
+    private List<HierarchicalCell> m_subHiearchy = new ArrayList<HierarchicalCell>();
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/tablularexpression/HierarchicalGrid.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression;
+
+import java.util.ArrayList;
+import java.util.List;
+
+/**
+ *
+ * @author Matthew Dawson <matthew@mjdsystems.ca>
+ */
+public class HierarchicalGrid implements SubHierarchyFetcher {
+    @Override
+    public List<HierarchicalCell> getSubHiearchy() {
+        return m_subHiearchy;
+    }
+    
+    private List<HierarchicalCell> m_subHiearchy = new ArrayList<HierarchicalCell>();
+}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/tablularexpression/SubHierarchyFetcher.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.tablularexpression;
+
+import java.util.List;
+
+/**
+ *
+ * @author Matthew Dawson <matthew@mjdsystems.ca>
+ */
+public interface SubHierarchyFetcher {
+    List<HierarchicalCell> getSubHiearchy();
+}

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/cvc3generator/HierarchicalGridCVC3GeneratorTest.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.parsers.VariableParser;
+import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchicalCell;
+import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchicalGrid;
+import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchcialGridCheckerWalkerGenerator;
+import java.util.List;
+import static org.junit.Assert.*;
+import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.junit.runners.JUnit4;
+
+/**
+ *
+ * @author Matthew Dawson <matthew@mjdsystems.ca>
+ */
+@RunWith(JUnit4.class)
+public class HierarchicalGridCVC3GeneratorTest {
+
+    // Exercise the cvc3 generator using a table designed in matlab.
+    @Test
+    public void exerciseCVC3Generator() {
+        HierarchicalGrid grid = new HierarchicalGrid();
+        List<HierarchicalCell> topCells = grid.getSubHiearchy();
+
+        topCells.add(new HierarchicalCell("x > 0"));
+        topCells.add(new HierarchicalCell("x == 0"));
+        topCells.add(new HierarchicalCell("0 > x"));
+
+        List<HierarchicalCell> nextGrid = topCells.get(1).getSubHiearchy();
+        nextGrid.add(new HierarchicalCell("z > 0"));
+        nextGrid.add(new HierarchicalCell("z == 0"));
+        nextGrid.add(new HierarchicalCell("0 > z"));
+
+        nextGrid.get(1).getSubHiearchy().add(new HierarchicalCell("z == 0"));
+
+        String out = HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(grid, new HierarchicalGridCVC3Generator(variableParser.parseVariables("x,z"), 1));
+
+        String expected = "ECHO \"begin1\";\n"+
+"PUSH;\n"+
+"QUERY (NOT ( (x > 0) AND (x = 0) ) AND\n"+
+"NOT ( (x > 0) AND (0 > x) ) AND\n"+
+"NOT ( (x = 0) AND (0 > x) ));\n"+
+"POP;\n"+
+"ECHO \"end1\";\n"+
+"ECHO \"begin2\";\n"+
+"PUSH;\n"+
+"QUERY ((x > 0) OR (x = 0) OR (0 > x));\n"+
+"POP;\n"+
+"ECHO \"end2\";\n"+
+"ECHO \"begin3\";\n"+
+"PUSH;\n"+
+"QUERY ((x = 0)) => (NOT ( (z > 0) AND (z = 0) ) AND\n"+
+"NOT ( (z > 0) AND (0 > z) ) AND\n"+
+"NOT ( (z = 0) AND (0 > z) ));\n"+
+"POP;\n"+
+"ECHO \"end3\";\n"+
+"ECHO \"begin4\";\n"+
+"PUSH;\n"+
+"QUERY ((x = 0)) => ((z > 0) OR (z = 0) OR (0 > z));\n"+
+"POP;\n"+
+"ECHO \"end4\";\n"+
+"ECHO \"begin5\";\n"+
+"PUSH;\n"+
+"QUERY ((z = 0) AND (x = 0)) => ();\n"+
+"POP;\n"+
+"ECHO \"end5\";\n"+
+"ECHO \"begin6\";\n"+
+"PUSH;\n"+
+"QUERY ((z = 0) AND (x = 0)) => ((z = 0));\n"+
+"POP;\n"+
+"ECHO \"end6\";\n";
+        assertEquals(expected, out);
+    }
+
+    VariableParser variableParser = new VariableParser();
+}

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/CVC3GeneratorTest.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.junit.runners.JUnit4;
+import static org.junit.Assert.*;
+
+/**
+ *
+ * @author matthew
+ */
+@RunWith(JUnit4.class)
+public class CVC3GeneratorTest {
+    /**
+     * Test of addition operation.
+     */
+    @Test
+    public void testAdditionOpConverstion() {
+        BinaryOperation op = BinaryOperation.Addition;
+        assertEquals("+", CVC3Generator.ConvertToOutputOp(op, new RealVariableType()));
+        assertEquals("BVPLUS(13,", CVC3Generator.ConvertToOutputOp(op, new FixedPointVariableType(true, 13, 5)));
+    }
+    /**
+     * Test of literals containing decimals.
+     *
+     * All decimals must be represented as fractions.  Ensure that this happens.
+     */
+    @Test
+    public void testLiteralRationalsAreFractions() {
+        Literal literal = new Literal("4.56");
+        assertEquals("(456/100)", literal.getCheckerOutput(new CVC3Generator(), new RealVariableType()));
+    }
+}

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/FixedPointVariableTypeTest.java

+/*
+ * To change this template, choose Tools | Templates
+ * and open the template in the editor.
+ */
+package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
+
+import org.junit.Test;
+import static org.junit.Assert.*;
+
+/**
+ *
+ * @author matthew
+ */
+public class FixedPointVariableTypeTest {
+    /**
+     * Test of constructor in class FixedPointType.
+     */
+    @Test
+    public void testConstructor() {
+        FixedPointVariableType instance = new FixedPointVariableType(true, 19, 9);
+        assertEquals(true, instance.isSigned());
+        assertEquals(19, instance.digits());
+        assertEquals(9, instance.fractionPart());
+    }
+    /**
+     * Test of getCVC3Definition method, of class FixedPointType.
+     */
+    @Test
+    public void testGetCVC3Definition() {
+        CVC3Generator generator = new CVC3Generator();
+        FixedPointVariableType instance = new FixedPointVariableType(true, 16, 8);
+        assertEquals("BITVECTOR(16)", generator.GenerateVariableType(instance));
+    }
+
+    /**
+     * Test of canCastToType method, of class FixedPointType.
+     */
+    @Test
+    public void testCanCastToType() {
+        FixedPointVariableType instance = new FixedPointVariableType(true, 16, 8);
+        assertFalse(instance.canCastToType(new RealVariableType()));
+    }
+
+    /**
+     * Test of equals method, of class FixedPointType.
+     */
+    @Test
+    public void testEquals() {
+        FixedPointVariableType instance = new FixedPointVariableType(true, 16, 8);
+        assertEquals(new FixedPointVariableType(true, 16, 8), instance);
+        assertFalse(instance.equals(new FixedPointVariableType(false, 16, 8)));
+        assertFalse(instance.equals(new FixedPointVariableType(true, 15, 8)));
+        assertFalse(instance.equals(new FixedPointVariableType(true, 16, 7)));
+    }
+}