Exercise 7 -- readmeEx7.txt

File contents

ReadMe file for exercise 2 from sheet 7

as for the last sheet, you can compile your code with

javac -cp smtinterpol.jar LraSolver.java

java -cp "smtinterpol.jar;." de.uni_freiburg.informatik.ultimate.smtinterpol.Main -script LraSolver testDDM1.smt2
.

Of course you can also import everything to eclipse after unpacking the jar file, again.

The framework given ist such that you work with precise rational numbers (i.e. no floating point arithmetic). You have seen the Rational class last exercise, but here are the most important methods again:

Rational r
r.add(Rational r1) -- yields a Rational with the value r + r1
r.mul(Rational r1) -- yields a Rational with the value r * r1
r.div(Rational r1) -- yields a Rational with the value r / r1
r.inverse() -- yields a Rational with the value 1/r
r.isNegative() -- yields a boolean
r.compareTo(Rational r1) -- yields an int with value -1 if r<r1, 0 if r=r1, 1 if r>r1


Rational.valueOf(long nominator, long denominator) -- yields a Rational with given (de)nominator
Rational.ONE
Rational.MONE
Rational.ZERO

you can always look inside the source code in the jar file if you miss something..
update (11.6.2013): the source code is not in the jar file, but there is a separate zip file on the website containing it