Added a solver-independent parser-interpreter and code-generator for SMT-LIB2 to JavaSMT

[KJanelle]

Integrating a parser-interpreter and a code-generator for SMT-LIB2 into JavaSMT as well as the usage of the Princess binary as a solver.

Theories supported by parser and generator:

Boolean
Integer
Real
Bitvector
Array
Uninterpreted Functions

Generator does not support modular congruence, because SMT-LIB2 does not (as far as I was able to find out). Parser wraps (define-fun ...) and (let ...) for JavaSMT. (as const ...) is interpreted as regular array, since JavaSMT does not support otherwise.

Value assignments in models from the Princess binary always use (define-fun), their conversion from SMT-LIB2 to JavaSMT is implemented accordingly.

argumentsInterpretation in Model.ValueAssignment is always empty, since it's not possible to gather the necessary information from the model String returned by the Princess binary.

Main source for the supported operators was https://smtlib.cs.uiowa.edu/theories.shtml.

As the existing solvers process constraints differently, not all tests work for all solvers (e.g. the tests for Z3 only succeed if they are carried out individually). The focus was on testing the usage with the Princess binary.