Treat nonlinear multiplication as only a warning when Z3 is used (closes #16).

In this case Z3 may return 'unknown' but I was not able to find any
simple examples that illustrated this. Currently such a response would
cause an exception in JKind. When we find an example, we can give it
better behavior.
Disable division checker for non-constant divisions (fixes #16).
Add real <-> int casting with the functions real(x) and floor(x). Closes #17.
Pass rewrite-divk option to cvc4 to enable division by a constant
Added nonlinear example
Add arrays which get expanded to scalars. See testing/array.lus for examples.
Bug fix due to array changes
Fix grammar to allow single element array literals
Bug fix, off-by-one error in bounds checking
added tuple expressions to allow multiple value node calls within a sub expression

(fixes #18)
Merge pull request #19 from lgwagner/master

add tuple expressions to allow multiple value node calls within a sub ...
Remove debugging code
Uninterpreted functions