Instructions

File contents

Technical instructions for exercise 4 on sheet 7

A current version of SMTInterpol can be found at
https://ultimate.informatik.uni-freiburg.de/smtinterpol/download.html
Download the precompiled binary.
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.

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 check out the git project at https://github.com/ultimate-pa/smtinterpol
and 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 -- there 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)

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

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

To print a term, use toString(), or - probably more convenient - toStringDirect(), which does not insert lets.


To represent linear terms, we often use another class that is not a subclass of Term in SMTInterpol:

SMTAffineTerm: 
self-simplifying, non-nested, linear terms, they are basically a hashmap mapping each variable to its coefficient.

Ways to obtain new SMTAffineTerms:
SMTAffineTerm s = toAffineTerm(term) (contained in the class QuantifierEliminationTQ)
SMTAffineTerm s = new SMTAffineTerm()

Modify existing SMTAffineTerm:
s.add(Rational r)
s.add(SMTAffineTerm t)
s.add(Rational factor, SMTAffineTerm t) -- adds factor*t
s.mul(Rational r)
s.div(Rational r)
s.negate()  -- computes (-s)

Querying SMTAffineTerm:
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
s.toTerm(Sort sort) -- converts an SMTAffineTerm back to a term
                   sort can be obtained from another term t with t.getSort()