Instructions for sheet 6 exercise 3

File contents

Technical instructions for exercise 3 on sheet 6

A current version of SMTInterpol can be found at http://ultimate.informatik.uni-freiburg.de/smtinterpol/download.html. On the exercise page there is a solver file QuantifierEliminationTQ.java. This is the file you should edit. Furthermore there is a test-file with some (very) simple tests -- feel free to write more interesting ones.

To solve this exercise you only need to fill in code in three positions, which are labelled with "fill in here" as well as a description of where you are in the algorithm.
However, feel free to read the whole code, change it if you see room for improvement (there is...).

Having smtinterpol.jar, QuantifierEliminationTQ.java and test.smt2 in the same directory you can compile it with:
javac -cp smtinterpol.jar QuantifierEliminationTQ.java
and run it with:
java -cp "smtinterpol.jar;." de.uni_freiburg.informatik.ultimate.smtinterpol.Main -script QuantifierEliminationTQ test.smt2
(under Linux or similar systems you have to replace the semicolon after smtinterpol.jar with a colon (... -cp smtinterpol.jar:.  ...))

However, you can also unzip the jar, copy the QuantifierElim... file into some directory (set the package accordingly) and work with it from Eclipse for example. -- this might be more convenient but should not be necessary.

We implement Quantifier Elimination as a simplification step -- i.e. in the smtlib script you have a line "(simplify formula)" where formula may contain quantifiers. The result will be the formula with the innermost quantifiers eliminated -- it may be several, but when quantifiers are nested, only the innermost ones are eliminated. To eliminate all, we can then just simplify several times (we need to copy/paste the intermediate results, as simplify is a command, not a function..).

Use the logic "LRA" (Linear Real Arithmetic).  
Starting the smt2 file with (set-option :print-terms-cse false) usually leads to nicer output.

You have to work with the data structures of SMTInterpol, here are the important parts of the API:
(you can also look into the code, of course, it is in the jar, as already mentioned..)

--- Theory, Sorts, Numbers,... ---
A Theory object takes care of building terms, providing sorts and much more, it is referenced by mTheory in our file.
mTheory.term(mTheory.mOr, Term t1, Term2)
mTheory.or(Term t1, Term2) -- convenience function for "or"

FunctionSymbols represent functions of all kinds (see ApplicationTerm...)
examples:
mTheory.mOr, mTheory.mTrue, mTheory.mNot,...

Sorts are the variable domains. We only use the "Boolean" and "Real" sort (in the SMT context people tend to use Reals and Rationals synonymously)
You can obtain Sort objects from the theory
mTheory.getRealSort()
mTheory.getBooleanSort()

We have a special class for rational (real) numbers called Rational.
Constants are for instance Rational.ZERO, Rational.ONE, Rational.MONE (for -1), ...

--- Types of Terms: --- 
For us, pretty much everything is a Term, formulas too, the most interesting ones for you are:

To print a term, use toString(), or - probably more convenient - toStringDirect(), which eliminates most of the lets.

ConstantTerm:
Term representing a number

ApplicationTerm:
Term representing any function application, this may be a boolean function like "or" (Bool, Bool -> Bool), as well as a relation like ">" (Real, Real -> Bool), or an arithmetic operation like "+" (Real, Real -> Real)
ApplicationTerm at = mTheory.term(String functionsymbol, Terms t...)
		   = mTheory.term(FunctionSymbol f, Terms t..)
at.getFunction()  -- returns a FunctionSymbol
at.getFunction().getName() -- the FunctionSymbol as the String in the script, for example ">", "or", useful for checking which function it is
at.getParameters() -- returns a Term[]

TermVariable:
A variable that is a Term, used for quantification and let, also as placeholder for later substitution
mTheory.createFreshTermVariable("anyNamePrefix", Sort s)

QuantifiedFormula:
.. the name says it all
qf.getQuantifier() -- 0 for exists, 1 for forall
qf.getVariables() -- smtlib allows quantification over several variables at once, we don't use this, so there should be only one
qf.getSubformula() -- the inner formula
mTheory.exists(TermVariable[] ts, Term subformula)

SMTAffineTerm: 
self-simplifying, non-nested, linear terms, they are basically a hashmap mapping each variable to its coefficient.
String output does not work when they are nested inside, ">"-ApplicationTerms for instance, so convert them back if you want to debug them.

Ways to obtain new SMTAffineTerms:
SMTAffineTerm s = SMTAffineTerm.create(Rational r, TermVariable t)
		= SMTAffineTerm.create(Rational r, Sort s)
		= SMTAffineTerm.create(ConstantTerm t)
s.add(Rational r)
s.add(SMTAffineTerm t)
s.mul(Rational r)
s.div(Rational r)
s.negated()  -- returns (-s)
SMTAffineTerm.cleanup(Term t) -- converts all SMTAffineTerms back to normal ApplicationTerms inside t
s.getSummands() -- gives a HashMap from the variables to the coefficients of the SMTAffineTerm

s.isConstant() -- returns true iff the term does not contain any variables
s.getConstant() -- returns the constant summand as a Rational