EventB's GenerateVariableType is now GenerateType.  Also narrow its visibility
to private, as it doesn't need to be public.

Along the same pattern, SMTLIB has one kicking around.

Along the same theme, more VariableType renames.

Similar to the VariableType to Type change, update VariableTypeMarker.

With the upcoming changes to VariableType, it is really no longer tied to
variables at all.  Thus rename to Type to better represent its role.

Expression had a non-existent license header.  Fix.  Also improve its
documentation.

Accidently left VariableTypeMarker as package private, for no good reason.
Fix to be public.  Discovered when when writing its documentation.

VariableTypeMarker gains javadoc strings.  Also fix the parameter of its
method, to match coding styles.

Slightly style change to getName.  Since we are in a table, we have to be
fetching the table name.  Reinforcing the fact doesn't help anything.

Since all details about n-dimensional tables are now internal to the Table
class and (eventually) the generators themselves, there is no longer a use
case for adjusting the TCC numbering offset in CVC3.  Thus just remove the
constructor, making everything simpler.

Provide a set of simpler PartialVariableCollection constructors.  These take
a list and work from there.  Note that the original Map version still exists
for VariableParser.

SMTLIB's test suite ignored the Query parameter.  To avoid possible failures
in the future, stick a quick set of tests in for that.

Cause its useless.

Correct stupid spelling mistake that slipped through.  This avoids writing
a bunch of MATLAB code that will only fail later.

Moving from the previous function, move the single event generation work to
a single function, reducing duplication.  Also move some other duplicated
lines to single places, reuse common variables, and start actionNo at 1,
avoiding an unnecessary addition on each loop iteration.

This was just a cleanup, building on the previous commit.

When preforming a loop with direct string concatenations, use a StringBuilder
instead.  Note function calls inside those loops may still use concatenations.
The whole class is not converted to avoid huge changes.

Avoid concating several strings together in the EventB variable generator.
While a complete optimization, the number of concatenations required makes
it worth it.

CVC3's fixed point literal generator used a ton of string appending to do its
work in a loop.  This could grow expensive easily, thus move to a StringBuilder.

When reading from Z3's output, make sure that the reader actually does a read.
Otherwise we may get back a useless character which will break things.

readLine can return a null.  To avoid an NPE, compare the string constant to
the output.  If null is returned, just throw an exception specifically about
this.

There is no need to use ISO-8859-1 when we can use UTF-8 for talking to Z3,
so use that for both input/output.  Also move the UTF-8 string constant to
a constant, allowing for easy changing later.

Similarly for the reading, make sure the write path always uses an appropriate
character set.  Use UTF-8, since it's always good.

decrementLevel should never cause m_level to go below 0.  This ensures a
bug in ANTLR won't cause random NPE's elsewhere in the code.

When the single argument constructor was used, PartialVariableCollection
made the assumption that no enumeration types were used, which made the
unit tests harder to write as they had to explicitly deal with the extraction.
Since the two argument constructor is an optimization, make the single
argument constructor attempt to pull out the enumeration types from the given
variables, making unit tests easier.

Javadoc on outputName "worked", but was incorrectly formatted.  Fix.

VariableCollection can now retrieve all the types used, and report them for
use with the TypeDeclarationGenerator interface.

By making the interface of VariableDeclarationGenerator use VariableCollection,
it becomes very hard to figure out of a particular language needs all variables
(both input and output) generated.  This makes testing all these classes less
practical (the point of the interface).  By moving this logic out of a
generator, higher level logic for the language can decide how to use the
generator, without impacting the tests.

As this function is only used for parsers (and some tests), and they only
ever care about the input variables, make the fucntion only return input
variables.  Enumerated values returned remain the same (containing all constants
from both inputs and outputs).

The table is no longer used inside the EventB grid generator, so remove it.
A field that was also there, but otherwise unused, is now removed as well.

All the walkers now use expressions internally, instead of Cells.  This allows
the parsing to be used into the Table class, avoiding having the walkers
needing the VariableCollection for a given table, simplifying their constructors
more.

Also clean up the imports, as they could be simplified due to this change.
Some imports may have not been necessary before this as well.

The EventB generator code can now fetch output cells using the value passed
in.  It also gains support for multiple output tables in the process, since
it's easier to support that now, then include funky hacks for to support only
single variable tables.

Also bring back the momThreeLayer table for testing EventB's multiple output
feature.

The SAL generator now uses the passed in output variables to get the output
expression for the given variable.  Due to limitiations with SAL syntax,
the generator needs to be run once per variable, so the generator takes in
the variable to output for.

To avoid having each generator contain the knowledge of how to grab the output
cell's contents, add a parameter to each walker that exposes this information
when hitting the leaf cells of the hierarchy.

In preparation for the walkers to internalize the various details of tables,
move them inside the Table class.  This forces code generating grids to get
a proper table instance, pushing the table into more places, making things
more organized.

Since VariableCollection now handles both input and output variables, move
Table to have both stored under that as well.  This involves killing the
split input/output variables functions.  Generator relying on how that split
worked are reworked to handle this reality.

VariableCollection now holds both the input and output variables.  To construct
a VariableCollection, two PartialVariableCollections are used that hold the
input and output variables.  The two are appropriately combined, while still
allowing the inputs and outputs to be separately pulled.

A single PartialVariableCollection also works, to allow for an input only
collection, which is useful for testing.

The CheckerWalkers have grown in numbers, while duplicating their logic.  As
well, fix the naming to be consistent and easily identifiable.

Yanjun Jiang authored Oct 01, 2014 and Matthew Dawson committed Oct 13, 2014

This refactor is corresponding to split the VariablesDeclarationGenerator
interface from ExpressionGenerator interface commit.

Yanjun Jiang authored Oct 01, 2014 and Matthew Dawson committed Oct 13, 2014

This commit is used to keep the changes history clean so that the
modification is easy to see.

Yanjun Jiang authored Oct 01, 2014 and Matthew Dawson committed Oct 13, 2014

This refactor is corresponding to split the VariablesDeclarationGenerator
interface from ExpressionGenerator interface commit.