You are here: Home Exercises Additional Material … Template File

Template File

Plain Text icon QuantifierEliminationTQ.java — Plain Text, 20 kB (20863 bytes)

File contents

//package de.uni_freiburg.informatik.ultimate.smtinterpol;

import java.math.BigDecimal;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Map.Entry;

import de.uni_freiburg.informatik.ultimate.logic.AnnotatedTerm;
import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm;
import de.uni_freiburg.informatik.ultimate.logic.ConstantTerm;
import de.uni_freiburg.informatik.ultimate.logic.FormulaUnLet;
import de.uni_freiburg.informatik.ultimate.logic.FunctionSymbol;
import de.uni_freiburg.informatik.ultimate.logic.LetTerm;
import de.uni_freiburg.informatik.ultimate.logic.NoopScript;
import de.uni_freiburg.informatik.ultimate.logic.QuantifiedFormula;
import de.uni_freiburg.informatik.ultimate.logic.Rational;
import de.uni_freiburg.informatik.ultimate.logic.SMTLIBException;
import de.uni_freiburg.informatik.ultimate.logic.Sort;
import de.uni_freiburg.informatik.ultimate.logic.Term;
import de.uni_freiburg.informatik.ultimate.logic.TermTransformer;
import de.uni_freiburg.informatik.ultimate.logic.TermVariable;
import de.uni_freiburg.informatik.ultimate.logic.Theory;
import de.uni_freiburg.informatik.ultimate.logic.Theory.SolverSetup;
import de.uni_freiburg.informatik.ultimate.smtinterpol.convert.SMTAffineTerm;
import de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator;
import de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.Substitutor;

public class QuantifierEliminationTQ extends NoopScript {

	Theory mTheory;
	FormulaUnLet mUnletter;
	boolean mDebug = true;

	/**
	 * This is called when the smtlib-script says (simplify ...)
	 */
	@Override
	public Term simplify(Term term) throws SMTLIBException {
		mUnletter = new FormulaUnLet();
		mTheory = this.getTheory();
		
		debug("################ starting fresh simplify command ###############");
		
		debug("input: " + term.toStringDirect());
		HashMap<TermVariable, Term> innerMostQuantifiedFormulas = new HashMap<TermVariable, Term>();
		Term termWithPlaceholders = getInnerMost(term, innerMostQuantifiedFormulas);
		debug("innermost quantified formulas: " + innerMostQuantifiedFormulas.values());
		debug("-------------------");
		
		for (Entry<TermVariable, Term> entry : innerMostQuantifiedFormulas.entrySet()) {
			QuantifiedFormula qf = (QuantifiedFormula) entry.getValue();
			debug("treating subformula: " + qf.toStringDirect());
			
			boolean isForAll = qf.getQuantifier() == QuantifiedFormula.FORALL;
			
			assert qf.getVariables().length == 1;
			TermVariable quantifiedVar = qf.getVariables()[0];
			
			Term bodyInNNF = toNNF(isForAll ? mTheory.not(qf.getSubformula()) : qf.getSubformula(), 0);
			debug("computed NNF of formula without quantifier: " + bodyInNNF.toStringDirect());
			Term bodyNoNegationsOrLeq = eliminateNegatedAndLeq(bodyInNNF);
			debug("eliminated negations and greater/lower equal: " + bodyNoNegationsOrLeq);
			HashSet<SMTAffineTerm> extractedTerms = new HashSet<SMTAffineTerm>();
			Term bodyIsolatedVar = isolateVarAndExtractTerms(bodyNoNegationsOrLeq, extractedTerms, quantifiedVar);
			debug("the formula with " + quantifiedVar + " isolated: " + bodyIsolatedVar.toStringDirect());
			debug("extracted the following terms from the formula after isolating " + quantifiedVar + ": "
					+ extractedTerms);
			
			HashSet<SMTAffineTerm> termSet = computeTermSet(extractedTerms, quantifiedVar.getSort());
			debug("S_F:" + termSet);
			
			Term resultFormula = isForAll ? 
					toNNF(mTheory.not(buildFormula(termSet, bodyIsolatedVar, quantifiedVar)), 0) : 
						buildFormula(termSet, bodyIsolatedVar, quantifiedVar);
			debug("the result of the quantifier elimination: " + resultFormula.toStringDirect());
					
			resultFormula = mUnletter.unlet(resultFormula);
					
			Term simplifiedResult = makeTrivialSimplifications((ApplicationTerm) resultFormula);
			debug("the simplified result: " + simplifiedResult.toStringDirect());
			
			simplifiedResult = mUnletter.unlet(simplifiedResult);
			
			termWithPlaceholders = new Substitutor(entry.getKey(), simplifiedResult).transform(termWithPlaceholders);
		}
		debug("-----------------");
		debug("overall result: " + termWithPlaceholders.toStringDirect());
		return termWithPlaceholders;
	}
	
	void debug(String s) {
		if (mDebug)
			System.out.println("  -- debug: " + s);
	}
	
	/**
	 * Extract the innermost quantified formulas in the given term, return a term where each one is replaced by a fresh
	 * TermVariable.
	 */
	private Term getInnerMost(Term term, HashMap<TermVariable, Term> result) {
		if (term instanceof QuantifiedFormula && 
				!(((QuantifiedFormula) term).getSubformula().toString().contains("exists") ||
						((QuantifiedFormula) term).getSubformula().toString().contains("forall"))) {
			TermVariable t = mTheory.createFreshTermVariable("placeholder", mTheory.getBooleanSort());
			result.put(t, term);
			return t;
		} else if (term instanceof QuantifiedFormula) {
			QuantifiedFormula qf = (QuantifiedFormula) term;
			if (qf.getQuantifier() == 0) {
				return mTheory.exists(qf.getVariables(), getInnerMost(qf.getSubformula(), result));
			} else {
				return mTheory.forall(qf.getVariables(), getInnerMost(qf.getSubformula(), result));
			}
		} else if (term instanceof AnnotatedTerm) {
			return getInnerMost(((AnnotatedTerm) term).getSubterm(), result); //throwing annotations away..
		} else if (term instanceof ApplicationTerm) {
			ApplicationTerm at = (ApplicationTerm) term;
			Term[] newSubterms = new Term[at.getParameters().length];
			for (int i = 0; i < at.getParameters().length; i++)
				newSubterms[i] = getInnerMost(at.getParameters()[i], result);
			return mTheory.term(at.getFunction(), newSubterms);
		}
		return term; 
	}

	/**
	 * Convert a quantifier-free formula to NNF (Step 1).
	 */
	private Term toNNF(Term term, int noNots) {
		if (term instanceof ApplicationTerm) {
			ApplicationTerm at = (ApplicationTerm) term;
			if (at.equals(mTheory.mTrue))
				return noNots % 2 == 0 ? mTheory.mTrue : mTheory.mFalse;
			else if (at.equals(mTheory.mFalse))
				return noNots % 2 == 0 ? mTheory.mFalse : mTheory.mTrue;
			else if (at.getFunction().equals(mTheory.mImplies)) {
				if (noNots % 2 == 0)
					return mTheory.or(toNNF(at.getParameters()[0], noNots + 1), toNNF(at.getParameters()[1], noNots));
				else
					return mTheory.and(toNNF(at.getParameters()[0], noNots + 1), toNNF(at.getParameters()[1], noNots));
			} else if (at.getFunction().equals(mTheory.mNot)) {
				if (noNots == 0)
					return toNNF(at.getParameters()[0], noNots + 1);
				else
					return toNNF(at.getParameters()[0], noNots - 1);
			} else if (at.getFunction().equals(mTheory.mOr)) {
				Term[] newSubterms = new Term[at.getParameters().length];
				for (int i = 0; i < at.getParameters().length; i++)
					newSubterms[i] = toNNF(at.getParameters()[i], noNots);
				if (noNots % 2 == 0)
					return mTheory.term(mTheory.mOr, newSubterms);
				else
					return mTheory.term(mTheory.mAnd, newSubterms);
			} else if (at.getFunction().equals(mTheory.mAnd)) {
				Term[] newSubterms = new Term[at.getParameters().length];
				for (int i = 0; i < at.getParameters().length; i++)
					newSubterms[i] = toNNF(at.getParameters()[i], noNots);
				if (noNots % 2 == 0)
					return mTheory.term(mTheory.mAnd, newSubterms);
				else
					return mTheory.term(mTheory.mOr, newSubterms);
			} else { //past innermost boolean function
				if (noNots % 2 == 0)
					return term;
				else
					return mTheory.term(mTheory.mNot, term);
			}
		} else if (term instanceof LetTerm) {
			Term unletted = mUnletter.unlet(term);
			return toNNF(unletted, noNots);
		}
		return term;
	}

	/**
	 * Eliminate negations and lower/greater equal symbols (Step 2).
	 */
	private Term eliminateNegatedAndLeq(Term formula) {
		if (formula instanceof ApplicationTerm) {
			if (formula.equals(mTheory.mTrue) || formula.equals(mTheory.mFalse))
				return formula;
			
			ApplicationTerm at = (ApplicationTerm) formula;
			if (at.getFunction().equals(mTheory.mAnd)) {
				Term[] newSubterms = new Term[at.getParameters().length];
				for (int i = 0; i < at.getParameters().length; i++)
					newSubterms[i] = eliminateNegatedAndLeq(at.getParameters()[i]);
				return mTheory.and(newSubterms);
			} else if (at.getFunction().equals(mTheory.mOr)) {
				Term[] newSubterms = new Term[at.getParameters().length];
				for (int i = 0; i < at.getParameters().length; i++)
					newSubterms[i] = eliminateNegatedAndLeq(at.getParameters()[i]);
				return mTheory.or(newSubterms);	
			} else if (at.getFunction().equals(mTheory.mNot)) {
				ApplicationTerm negatedAt = (ApplicationTerm) at.getParameters()[0];
				Term s = negatedAt.getParameters()[0];
				Term t = negatedAt.getParameters()[1];
				if (negatedAt.getFunction().getName() == "=") {
					return mTheory.or(
							mTheory.term(">", s, t), 
							mTheory.term(">", t, s));
				} else if (negatedAt.getFunction().getName() == "<=") {
					return	mTheory.term(">", s, t); 					
				} else if (negatedAt.getFunction().getName() == "<") {
					return mTheory.or(
							mTheory.term(">", s, t), 
							mTheory.equals(s, t));
				} else if (negatedAt.getFunction().getName() == ">=") {
					return	mTheory.term(">", t, s); 					
				} else if (negatedAt.getFunction().getName() == ">") {
					return mTheory.or(
							mTheory.term(">", t, s), 
							mTheory.equals(t, s));
				}
			} else { //should have a non-negated (in)equality
				Term s = at.getParameters()[0];
				Term t = at.getParameters()[1];
				if (at.getFunction().getName() == "=") {
					return at;
				} else if (at.getFunction().getName() == "<=") {
					return mTheory.or(
							mTheory.term(">", t, s), 
							mTheory.equals(t, s));
				} else if (at.getFunction().getName() == "<") {
					return	mTheory.term(">", t, s); 					
				} else if (at.getFunction().getName() == ">=") {
					return mTheory.or(
							mTheory.term(">", s, t), 
							mTheory.equals(s, t));
				} else if (at.getFunction().getName() == ">") {
					return	mTheory.term(">", s, t); 					
				}
			}
		} 
		return formula;
	}

	/**
	 * Bring the quantified variable to one side in each (in)equality (Step 3), also pick up the terms on the other
	 * sides.
	 * @param formula the input formula
	 * @param extractedTerms when we have isolated the quantified variable, we can collect the "other" term and write it
	 * here
	 * @param quantifiedVar the variable to isolate
	 * @return the formula where quantifiedVar is isolated
	 */
	private Term isolateVarAndExtractTerms(Term formula, HashSet<SMTAffineTerm> extractedTerms,
			TermVariable quantifiedVar) {
		if (formula instanceof ApplicationTerm) {
			ApplicationTerm at = (ApplicationTerm) formula;
			if (at.getFunction().equals(mTheory.mAnd)) {
				Term[] newSubterms = new Term[at.getParameters().length];
				for (int i = 0; i < at.getParameters().length; i++)
					newSubterms[i] = isolateVarAndExtractTerms(at.getParameters()[i], extractedTerms, quantifiedVar);
				return mTheory.term(mTheory.mAnd, newSubterms);
			} else if (at.getFunction().equals(mTheory.mOr)) {
				Term[] newSubterms = new Term[at.getParameters().length];
				for (int i = 0; i < at.getParameters().length; i++)
					newSubterms[i] = isolateVarAndExtractTerms(at.getParameters()[i], extractedTerms, quantifiedVar);
				return mTheory.term(mTheory.mOr, newSubterms);	
			} else if (at.getFunction().getName() == ">" || at.getFunction().getName() == "=") {
				Term left = at.getParameters()[0];
				Term right = at.getParameters()[1];
				SMTAffineTerm affineTermLeft = toAffineTerm(left);
				SMTAffineTerm affineTermRight = toAffineTerm(right);
				
				// fill in here:
				// the situation is: (functionsymbol affineTermLeft affineTermRight) with functionSymbol in {"=",">"} 
				// you need to isolate quantifiedVar on one side (as in step 2)
				// also remember to fill extractedTerms when you have computed the term on the other side
				// make sure to read about SMTAffineTerms in the readme or in the corresponding class
			} 
		}
		return formula;
	}
	
	/**
	 * Combine all the parts to get the quantifier-free subformula and return it (Step 4).
	 */
	private Term buildFormula(HashSet<SMTAffineTerm> termSet, Term bodyIsolatedVar, TermVariable quantifiedVariable) {
		ArrayList<Term> resultFormulas = new ArrayList<Term>();
		
		//build left and right infinite projections
		resultFormulas.add(buildProjection(bodyIsolatedVar, quantifiedVariable, true));
		resultFormulas.add(buildProjection(bodyIsolatedVar, quantifiedVariable, false));
		
		//build the disjuncts
		for (SMTAffineTerm t : termSet) 
			resultFormulas.add(mTheory.let(quantifiedVariable, t.toTerm(quantifiedVariable.getSort()), bodyIsolatedVar));
		
		Term[] resultFormulasArray = new Term[resultFormulas.size()];
		resultFormulas.toArray(resultFormulasArray);
		return mTheory.or(resultFormulasArray);
	}

	/**
	 * Build the left or right infinite projection.
	 * @param formula the formula F[x]
	 * @param quantifiedVariable the quantifiedVariable "x"
	 * @param left true if we want the left infinite projection, false if we want the right infinite projection
	 * @return the projection formula
	 */
	private Term buildProjection(Term formula,
			TermVariable quantifiedVariable, boolean left) {
		if (formula instanceof ApplicationTerm) {
			if (formula.equals(mTheory.mTrue) || (formula.equals(mTheory.mFalse)))
					return formula;
			
			ApplicationTerm at = (ApplicationTerm) formula;
			if (at.getFunction().equals(mTheory.mAnd)) {
				Term[] newSubterms = new Term[at.getParameters().length];
				for (int i = 0; i < at.getParameters().length; i++)
					newSubterms[i] = buildProjection(at.getParameters()[i], quantifiedVariable, left);
				return mTheory.term(mTheory.mAnd, newSubterms);
			} else if (at.getFunction().equals(mTheory.mOr)) {
				Term[] newSubterms = new Term[at.getParameters().length];
				for (int i = 0; i < at.getParameters().length; i++)
					newSubterms[i] = buildProjection(at.getParameters()[i], quantifiedVariable, left);
				return mTheory.term(mTheory.mOr, newSubterms);	
			} else if (at.getFunction().getName() == ">") {
				//fill in here:
				// you have a term (> at.getParameters[0] at.getParameters()[1]) and you need to
				// compute the left/right infinite projection if the flag "left" is set to true/false

				//TODO return the right term
				return at;
			} else if (at.getFunction().getName() == "=") {

				//TODO return the right term
				return at;
			}
		} else if (formula instanceof LetTerm) {
			Term unletted = mUnletter.unlet(formula);
			return buildProjection(unletted, quantifiedVariable, left);
		}
		assert false; //if we reach this location, the formula did not just contain and, or, >, =
		return null;
	}

	/**
	 * Compute the set S_F of terms from a set of terms that have been extracted from the formula
	 * @param extractedTerms the set of terms
	 * @return the set S_F (without +- infinity)
	 */
	private HashSet<SMTAffineTerm> computeTermSet(HashSet<SMTAffineTerm> extractedTerms, Sort sort) {
		HashSet<SMTAffineTerm> result = new HashSet<>();
		//fill in here:
		// we have the set of terms occurring in the formula, and we need to compute
		// the set S_F from it
		return result;
	}

	
	/**
	 * Try simplifying the formula by resolving (in)equalities over constants, and "or"s and "and"s with true or false
	 * @param formula the formula that is to be simplified
	 * @return the simplified equivalent formula
	 */
	private Term makeTrivialSimplifications(Term formula) {
		if (formula instanceof ApplicationTerm) {
			ApplicationTerm at = (ApplicationTerm) formula;

			if (at.equals(mTheory.mTrue) || at.equals(mTheory.mFalse)) {
				return at;
			} else if (at.getFunction().getName() == "or" || at.getFunction().getName() == "and") {
				boolean isOr = at.getFunction().getName() == "or";
				ArrayList<Term> trueSubTerms = new ArrayList<Term>();
				ArrayList<Term> falseSubTerms = new ArrayList<Term>();
				ArrayList<Term> nonTrivialSubTerms = new ArrayList<Term>();

				for (Term param : at.getParameters()) {
					Term simplified = makeTrivialSimplifications(param);
					if (simplified.equals(mTheory.mTrue)) {
						trueSubTerms.add(simplified);
					} else if (simplified.equals(mTheory.mFalse)) {
						falseSubTerms.add(simplified);
					} else {
						nonTrivialSubTerms.add(simplified);
					}
				}

				if (isOr) {
					if (!trueSubTerms.isEmpty()) {
						return mTheory.mTrue;
					} else {
						Term[] ntsArray = new Term[nonTrivialSubTerms.size()];
						nonTrivialSubTerms.toArray(ntsArray);
						return mTheory.or(ntsArray);
					}
				} else {
					if (!falseSubTerms.isEmpty()) {
						return mTheory.mFalse;
					} else {
						Term[] ntsArray = new Term[nonTrivialSubTerms.size()];
						nonTrivialSubTerms.toArray(ntsArray);
						return mTheory.and(ntsArray);
					}
				}
			} else if (at.getFunction().getName() == "not") {
				return mTheory.not(makeTrivialSimplifications(at.getParameters()[0]));
			} else if (at.getFunction().getName() == ">") {
				SMTAffineTerm left = toAffineTerm(at.getParameters()[0]);
				SMTAffineTerm right = toAffineTerm(at.getParameters()[1]);
				left.add(Rational.MONE, right);
				if (left.isConstant()) {
					if (left.getConstant().signum() > 0) {
						return mTheory.mTrue;
					} else {
						return mTheory.mFalse;
					}
				} else {
					Sort sort = at.getParameters()[0].getSort();
					return mTheory.term(">", left.toTerm(sort), Rational.ZERO.toTerm(sort));
				}
			} else if (at.getFunction().getName() == "=") {
				SMTAffineTerm left = toAffineTerm(at.getParameters()[0]);
				SMTAffineTerm right = toAffineTerm(at.getParameters()[1]);
				left.add(Rational.MONE, right);
				if (left.isConstant()) {
					if (left.getConstant().signum() == 0) {
						return mTheory.mTrue;
					} else {
						return mTheory.mFalse;
					}
				} else {
					Sort sort = at.getParameters()[0].getSort();
					if (sort.isNumericSort()) {
						return mTheory.term("=", left.toTerm(sort), Rational.ZERO.toTerm(sort));
					} else {
						return at;
					}
				}
			}
		} else if (formula instanceof LetTerm) {
			LetTerm lt = (LetTerm) formula;
			Term simplified = makeTrivialSimplifications(lt.getSubTerm());
			if (simplified.equals(mTheory.mTrue) || simplified.equals(mTheory.mFalse)) {
				return simplified;
			} else {
				return formula;
			}
		}
		return formula;
	}
	
	/**
	 * Take a linear arithmetic expression as a term and return an SMTAffineTerm with the same value
	 */
	private SMTAffineTerm toAffineTerm(Term term) {
		if (term instanceof ApplicationTerm) {
			ApplicationTerm at = (ApplicationTerm) term;
			if (at.getFunction().getName() == "+") {
				SMTAffineTerm result = new SMTAffineTerm();
				for (Term param : at.getParameters()) 
					result.add(toAffineTerm(param));
				return result;
			} else if (at.getFunction().getName() == "-") {
				SMTAffineTerm result = new SMTAffineTerm();
				Term[] params = at.getParameters();
				if (params.length == 1 ) {
					result.add(Rational.MONE, toAffineTerm(params[0]));				
				} else {
					result.add(toAffineTerm(params[0]));
					for (int i = 1; i < params.length; i++) {
						// subtract the other parameters
						// Rational.MONE stands for -1.
						result.add(Rational.MONE, toAffineTerm(at.getParameters()[1]));
					}
				}
				return result;
			} else if (at.getFunction().getName() == "*") {
				SMTAffineTerm recResult1 = toAffineTerm(at.getParameters()[0]);
				SMTAffineTerm recResult2 = toAffineTerm(at.getParameters()[1]);
				if (recResult1.isConstant()) {
					recResult2.mul(recResult1.getConstant());
					return recResult2;
				} else if (recResult2.isConstant()) {
					recResult1.mul(recResult2.getConstant());
					return recResult1;
				} else {
					assert false;
				}
			} else if(at.getFunction().getName() == "/") {
				SMTAffineTerm recResult1 = toAffineTerm(at.getParameters()[0]);
				SMTAffineTerm recResult2 = toAffineTerm(at.getParameters()[1]);
				assert recResult2.isConstant();
				recResult1.div(recResult2.getConstant());
				return recResult1;
			} else { //we have a constant
				assert at.getParameters().length == 0;
				return new SMTAffineTerm(at);
			}
		} else if (term instanceof ConstantTerm) {
			return new SMTAffineTerm(term);
		} else if (term instanceof TermVariable) {
			return new SMTAffineTerm(term);
		}
		return null;
	}

}