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 rr1
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