Template File
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; } }