Add a test for CVC3 fixed point support, and get fixed point working again.
This implements support for the fixed point marker, and make use of it.

The only problem is that literals by default fall down to Reals, so not all
operations are tested.  This needs to be fixed.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10709 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Now that Matlab parsing is pretty much all done, remove extra output.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10708 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Real operators are now added for CVC3 generation.  Fixed point is still left
out.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10707 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Implement other operators for SMTLIB.  Also implement a test for it.  The test
is parameterized, so CVC3 support is easy to add.  Due to the parameterization,
a newer version of JUnit is required, so bump the version in the pom.xml file.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10706 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

When dealing with expressions, and generating output for them, types have
to be exactly known.  However, when two literals are added together (like:
5+5), the type to use for that is unknown.  To fix this issue, type information
has to be forced down the pipe.  So know the addition operation now knows it
needs to produce a particular type (ex Real or Fixed Point), and then tests
what the subexpressions can produce (for literals, they can produce either,
but a variable can only be what it is).

For Real, that is fine.  However a fixed point can take an infinite number of
different possibilities, and one cannot test for every combination.  So instead
a type "marker" is introduced.  This marker instead identifies that a fixed
point type is generally wanted, but specifics are unknown.  The system will
query for an appropriate type, and requires the specific type is returned, and
not a marker.  All types are also markers for themselves, so Reals, for instance,
don't need anything special.

While the marker system sounds good in theory, it currently is fully implemented,
so fixed point is currently broken.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10705 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Binary ops now includes:
-
/
>=
<
<=
Unary:
-
YAY!

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10704 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Test that each operator is parsed in properly.  Currently only tests implemented
operators, with more to follow.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10703 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

The java code now loads into Matlab automatically, but it uses a differnt
jar file location now.  Things work though.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10668 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Show an option for checking against Z3, and also hook it up to the matlab
code for use.  Everything should be working now.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10667 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Do to the way the matlab code works, the GenerateMatlabVariableDeclarations
is actually useless.  Thus, make SampleValues public so that the matlab code
can still do what it needs to do.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10666 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

When walking an empty grid, no queries for either complete or disjoint are
generated.  Disjoint handled this fine, but complete did not.  Fix this.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10665 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Due to some copy+paste errors, cvc3 was mentioned in smtlib test code.  Rename
the references as appropriate.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10664 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Add a CheckerRunner class with a single static method to run z3.  It uses
the smtlib generators, and the logic can be extended to other smtlib2 compliant
smt solvers.  It uses the copy of z3 in your path for now.

Note that it is very brittle, and if z3 has issue can potentially lock the
thread it is running on, as Java has no easy way to add timeouts to reads
on the stdout of z3.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10663 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Add a simple class to hold the results of a failed query to a SMT checker.
Also, it has a utility function to easily generate a matlab expression for
the failed test's counter-model.  Also test.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10662 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

The grammar file requires Matlab expressions, it expects the expression to end
with a newline.  However, lots of generated code doesn't.  Thus force this to be
always correct.  Note that any extra newlines shouldn't cause issues.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10661 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

To stay at least a little consistent, use smtlibchecker for the smtlib
package name.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10660 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

The cvc3generator package was moved out of tablularexpression.  Matlab code
wasn't updated, and thus broke.  Fix this mistake.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10659 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Implement a first run (with simple non-exhaustive test) of the SMT-LIB generator
for hierarchical tables.  This generates the same information as the cvc3
generator, but using the appropriate syntax.  Note that the generated script
can't be directly run, due to how SMT-LIB verifiers work regarding reading of
values, so the queries need to be piped directly across one by one for
verification.

Also, since SMT-LIB doesn't have an equivalent to CVC3's QUERY command, all
queries have a not placed in front.  This lead to a few changes to the queries:
 - Disjoint queries now had a format of: (not (and (not (and e1 e2)))).  This
can be simplified with De Morgan's law to (or (and e1 e2)) (by removing the
(not (and (not to the more simple (or).
 - Complete queries now have an extra (not in front.  No further optimization
is possible.
 - For the parent part of any query, instead of using (not (=> (p e)), which
removes the potential disjoint optimization, the not is pushed down so the
format is now (and p (not e)).  Also, for simplification p is always defined,
and is true when no parent cells exist.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10658 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

In SMT-LIB, any real literal *must* have a decimal point, otherwise various
parsers may explode.  Since I know if a literal is supposed to be real, fix
this issue by appending a harmless ".0" to the string of the number.  Fix
tests to verify this.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10657 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

The system can now generate SMT-LIB code from the parsed Matlab code.  It doesn't
deal with tables (yet), but that is next.  Also use the MatlabParser tests to
verify the generated SMT-LIB code.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10656 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Start with the SMTLIBGenerator class.  To start with, deal with variable
definitions!

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10655 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

GenerateVariableType was an unused function outside of some internal pieces.
Thus remove it from the CheckerGenerator interface, as it doesn't need to be
exposed.  Update a few internal uses of it to use an explicit instance of a
CheckerGenerator for when it was used (inside of tests).

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10654 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Some debug output was left in and committed.  Remove the extra junk.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10653 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

The cvc3generator package was originally put in tablularexpression while
I was fighting with maven.  Since it doesn't have to be in the package, remove
it to clean up the layout of packages.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10652 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Now the full contents of the CVC3 file are generated inside of Java, but the
actual saving and running of CVC3 still happen inside of matlab.  For now.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10651 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Parse the hierarchy for the tables to generate the necessary bits of CVC3
code.  It generates equivalent code for CVC3 now to what matlab would.  Some
excess brackets are removed, making things neater.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10650 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Add parsing for the && operator.  However, the grammar file doesn't have an
explicit node for it.  To avoid having to create a node per such operations,
instead add a method so that they are automatically created as necessary.  Since
each one is used (repeatedly), as the level decrements stick the appropriate
operator in place.   The system will then pick up on this and handle the situation
appropriately.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10564 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Start adding support for the boolean and operation.  Currently it works if
parsed correctly, but the next commit is necessary so it can be parsed.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10563 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10540 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

CVC3 uses the '=' operator for equality, not '=='.  Fix this to ensure it
is correct.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10539 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Since expression's outputs now generally work with their type correctly, make
use of this to try and ensure an expression is evaluated correctly.  Also
make sure that the requested type does match the type outputted, and test
that this occurs (for now, just in BinaryExpression and Variable).

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10538 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Since binary expressions can actually change the type (for instance, comparisions
switch the type for the number input to boolean), handle this so calls further
up the chain don't break (for instance, boolean operators, ex AND).

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10471 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

For some reason, the equals infix operator disappeared.  Fix that ...

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10470 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Now add the actual prefix unary operation support.  For now, just deal with
negation (~), and cheat the code gen appropriately.  But for the future,
things are ready for use.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10469 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Various classes/functions (ex MatlabOperation) are not preapred to deal with
unary operations, and realistically probably never will.  Thus just rename
to include binary in the name (ex MatlabBinaryOperation).  Also push the
changes down so everything still works.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10468 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Add the necessary pieces to the boolean type, so that the CVC3 code can
generate for it.  Currently the only failing issue is some operators to actually
make use of it.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10467 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

CVC3Generator is now tied to the CheckerGenerator interface, allowing for
PVS and SMTLIB to move in.  This caused a huge set of changes in other files,
to push the generator through various places.  Also, the matlab code needed
updating to work with the new functions and CheckerGenerator.  In theory it
should all be fine now.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10466 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Move all CVC3 code into CVC3Generator.  Currently it is just static methods,
next is to make implement an interface!

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10465 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Start with basic changes for generator.  First step, try moving the operation
generation piece to a new class.  For now, just use static methods.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10327 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Instead of assuming the number is always at a certain position, use a regexp
to find it.  It basically looks for "PVS Version 0.0", and only uses the 0.0.


git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@10203 57e6efec-57d4-0310-aeb1-a6c144bb1a8b