Yanjun Jiang authored Nov 21, 2014 and Matthew Dawson committed Nov 22, 2014

jTET does not support Boolean comparison now, no matter it is
Equals or NotEquals. This is caused by the BooleanType is not
included in the array list for the Equals and NotEquals cases
in the getInputTypeForOutput function. We fix this by adding
the BooleanType in the array list.

Instead of generating invalid CVC3 code when a grid has a single used cell,
instead simply do not generate a disjoint TCC as it will always be true
anyways.

ExpressionGenerator now has javadoc, and changed the interface's parameter
names to be more logical.  Also update all the generators to match.

Multiple grid tables (with both top and left) now parse correctly.  Unit
tests to help prove this, with the underlying assumption that since no
interface changes happened, all generators are happy.

Note that the breadth first generator doesn't get a notice on grid switch,
which is still planned.

Tables which have only a top grid are now walkable, with unit tests to prove
it.  These tables come out identical to tables with the grid in the left
position, and thus don't require further tests in generators.

Make sure the table walking works as expected.  Currently tests the only
implemented part, which is the left grid breadth/depth first walking.

TableTest didn't have the RunWith annotation.  Fix.

Since the predicate subtype can be set per variable, move that logic to the
Variable class, away from the Type class.  Before, Type disagreed on whether
two instances could be equal, and whether they could be easily duplicated.
This makes the distinction unimportant.  It does neuter the custom type
functionality in VariableParser some, but that can be added back later.

Rename the given function, to match the VariableType change, along with making
the name more descriptive.

SAL's GenerateVariableType is now GenerateType, matching everyone else.

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.