//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 m_theory; FormulaUnLet m_unletter; boolean m_debug = true; /** * this is called when the smtlib-script says (simplify ...) */ @Override public Term simplifyTerm(Term term) throws SMTLIBException { m_unletter = new FormulaUnLet(); m_theory = this.getTheory(); debug("################ starting fresh simplify command ###############"); debug("input: " + term.toStringDirect()); HashMap innerMostQuantifiedFormulas = new HashMap(); Term termWithPlaceholders = getInnerMost(term, innerMostQuantifiedFormulas); debug("innermost quantified formulas: " + innerMostQuantifiedFormulas.values()); debug("-------------------"); for (Entry 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 ? m_theory.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 extractedTerms = new HashSet(); Term bodyIsolatedVar = SMTAffineTerm.cleanup(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 termSet = computeTermSet(extractedTerms); debug("S_F:" + termSet); Term resultFormula = isForAll ? toNNF(m_theory.not(buildFormula(termSet, bodyIsolatedVar, quantifiedVar)), 0) : buildFormula(termSet, bodyIsolatedVar, quantifiedVar); debug("the result of the quantifier elimination: " + resultFormula.toStringDirect()); resultFormula = m_unletter.unlet(resultFormula); Term simplifiedResult = makeTrivialSimplifications((ApplicationTerm) resultFormula); debug("the simplified result: " + simplifiedResult.toStringDirect()); simplifiedResult = m_unletter.unlet(simplifiedResult); termWithPlaceholders = new Substitutor(entry.getKey(), simplifiedResult).transform(termWithPlaceholders); } debug("-----------------"); debug("overall result: " + termWithPlaceholders.toStringDirect()); return termWithPlaceholders; } void debug(String s) { if (m_debug) 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 result) { if (term instanceof QuantifiedFormula && !(((QuantifiedFormula) term).getSubformula().toString().contains("exists") || ((QuantifiedFormula) term).getSubformula().toString().contains("forall"))) { TermVariable t = m_theory.createFreshTermVariable("placeholder", m_theory.getBooleanSort()); result.put(t, term); return t; } else if (term instanceof QuantifiedFormula) { QuantifiedFormula qf = (QuantifiedFormula) term; if (qf.getQuantifier() == 0) { return m_theory.exists(qf.getVariables(), getInnerMost(qf.getSubformula(), result)); } else { return m_theory.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 m_theory.term(at.getFunction(), newSubterms); } return term; } /** * converts 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(m_theory.TRUE)) return noNots % 2 == 0 ? m_theory.TRUE : m_theory.FALSE; else if (at.equals(m_theory.FALSE)) return noNots % 2 == 0 ? m_theory.FALSE : m_theory.TRUE; else if (at.getFunction().equals(m_theory.m_Implies)) { if (noNots % 2 == 0) return m_theory.or(toNNF(at.getParameters()[0], noNots + 1), toNNF(at.getParameters()[1], noNots)); else return m_theory.and(toNNF(at.getParameters()[0], noNots + 1), toNNF(at.getParameters()[1], noNots)); } else if (at.getFunction().equals(m_theory.m_Not)) { if (noNots == 0) return toNNF(at.getParameters()[0], noNots + 1); else return toNNF(at.getParameters()[0], noNots - 1); } else if (at.getFunction().equals(m_theory.m_Or)) { 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 m_theory.term(m_theory.m_Or, newSubterms); else return m_theory.term(m_theory.m_And, newSubterms); } else if (at.getFunction().equals(m_theory.m_And)) { 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 m_theory.term(m_theory.m_And, newSubterms); else return m_theory.term(m_theory.m_Or, newSubterms); } else { //past innermost boolean function if (noNots % 2 == 0) return term; else return m_theory.term(m_theory.m_Not, term); } } else if (term instanceof LetTerm) { Term unletted = m_unletter.unlet(term); return toNNF(unletted, noNots); } return term; } /** * Eliminate Negations and lower/greater equal symbols (step2) */ private Term eliminateNegatedAndLeq(Term formula) { if (formula instanceof ApplicationTerm) { if (formula.equals(m_theory.TRUE) || formula.equals(m_theory.FALSE)) return formula; ApplicationTerm at = (ApplicationTerm) formula; if (at.getFunction().equals(m_theory.m_And)) { Term[] newSubterms = new Term[at.getParameters().length]; for (int i = 0; i < at.getParameters().length; i++) newSubterms[i] = eliminateNegatedAndLeq(at.getParameters()[i]); return m_theory.and(newSubterms); } else if (at.getFunction().equals(m_theory.m_Or)) { Term[] newSubterms = new Term[at.getParameters().length]; for (int i = 0; i < at.getParameters().length; i++) newSubterms[i] = eliminateNegatedAndLeq(at.getParameters()[i]); return m_theory.or(newSubterms); } else if (at.getFunction().equals(m_theory.m_Not)) { ApplicationTerm negatedAt = (ApplicationTerm) at.getParameters()[0]; Term s = negatedAt.getParameters()[0]; Term t = negatedAt.getParameters()[1]; if (negatedAt.getFunction().getName() == "=") { return m_theory.or( m_theory.term(">", s, t), m_theory.term(">", t, s)); } else if (negatedAt.getFunction().getName() == "<=") { return m_theory.term(">", s, t); } else if (negatedAt.getFunction().getName() == "<") { return m_theory.or( m_theory.term(">", s, t), m_theory.equals(s, t)); } else if (negatedAt.getFunction().getName() == ">=") { return m_theory.term(">", t, s); } else if (negatedAt.getFunction().getName() == ">") { return m_theory.or( m_theory.term(">", t, s), m_theory.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 m_theory.or( m_theory.term(">", t, s), m_theory.equals(t, s)); } else if (at.getFunction().getName() == "<") { return m_theory.term(">", t, s); } else if (at.getFunction().getName() == ">=") { return m_theory.or( m_theory.term(">", s, t), m_theory.equals(s, t)); } else if (at.getFunction().getName() == ">") { return m_theory.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 extractedTerms, TermVariable quantifiedVar) { if (formula instanceof ApplicationTerm) { ApplicationTerm at = (ApplicationTerm) formula; if (at.getFunction().equals(m_theory.m_And)) { 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 m_theory.term(m_theory.m_And, newSubterms); } else if (at.getFunction().equals(m_theory.m_Or)) { 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 m_theory.term(m_theory.m_Or, 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 at return it. (step 4) */ private Term buildFormula(HashSet termSet, Term bodyIsolatedVar, TermVariable quantifiedVariable) { ArrayList resultFormulas = new ArrayList(); //build left and right infinite projections resultFormulas.add(buildProjection(bodyIsolatedVar, quantifiedVariable, true)); resultFormulas.add(buildProjection(bodyIsolatedVar, quantifiedVariable, false)); //build the disjuncts for (Term t : termSet) resultFormulas.add(m_theory.let(quantifiedVariable, t, bodyIsolatedVar)); Term[] resultFormulasArray = new Term[resultFormulas.size()]; resultFormulas.toArray(resultFormulasArray); return m_theory.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(m_theory.TRUE) || (formula.equals(m_theory.FALSE))) return formula; ApplicationTerm at = (ApplicationTerm) formula; if (at.getFunction().equals(m_theory.m_And)) { 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 m_theory.term(m_theory.m_And, newSubterms); } else if (at.getFunction().equals(m_theory.m_Or)) { 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 m_theory.term(m_theory.m_Or, newSubterms); } else if (at.getFunction().getName() == ">") { //fill in here: //you are 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 } else if (at.getFunction().getName() == "=") { return m_theory.FALSE; } } else if (formula instanceof LetTerm) { Term unletted = m_unletter.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 computeTermSet(HashSet extractedTerms) { HashSet 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(m_theory.TRUE) || at.equals(m_theory.FALSE)) return at; else if (at.getFunction().getName() == "or" || at.getFunction().getName() == "and") { boolean isOr = at.getFunction().getName() == "or"; ArrayList trueSubTerms = new ArrayList(); ArrayList falseSubTerms = new ArrayList(); ArrayList nonTrivialSubTerms = new ArrayList(); for (Term param : at.getParameters()) { Term simplified = makeTrivialSimplifications(param); if (simplified.equals(m_theory.TRUE)) trueSubTerms.add(simplified); else if (simplified.equals(m_theory.FALSE)) falseSubTerms.add(simplified); else nonTrivialSubTerms.add(simplified); } if (isOr) { if (!trueSubTerms.isEmpty()) return m_theory.TRUE; else { Term[] ntsArray = new Term[nonTrivialSubTerms.size()]; nonTrivialSubTerms.toArray(ntsArray); return m_theory.or(ntsArray); } } else { if (!falseSubTerms.isEmpty()) return m_theory.FALSE; else { Term[] ntsArray = new Term[nonTrivialSubTerms.size()]; nonTrivialSubTerms.toArray(ntsArray); return m_theory.or(ntsArray); } } } else if (at.getFunction().getName() == ">") { if (at.getParameters()[0] instanceof ConstantTerm && at.getParameters()[1] instanceof ConstantTerm) { SMTAffineTerm s1 = SMTAffineTerm.create(at.getParameters()[0]); SMTAffineTerm s2 = SMTAffineTerm.create(at.getParameters()[1]); int compResult = (s1.getConstant()).compareTo((s2.getConstant())); if (compResult == 1) return m_theory.TRUE; else return m_theory.FALSE; } else return at; } else if (at.getFunction().getName() == "=") { if (at.getParameters()[0] instanceof ConstantTerm && at.getParameters()[1] instanceof ConstantTerm) { SMTAffineTerm s1 = SMTAffineTerm.create(at.getParameters()[0]); SMTAffineTerm s2 = SMTAffineTerm.create(at.getParameters()[1]); int compResult = (s1.getConstant()).compareTo((s2.getConstant())); if (compResult == 0) return m_theory.TRUE; else return m_theory.FALSE; } else return at; } } else if (formula instanceof LetTerm) { LetTerm lt = (LetTerm) formula; Term simplified = makeTrivialSimplifications(lt.getSubTerm()); if (simplified.equals(m_theory.TRUE) || simplified.equals(m_theory.FALSE)) return simplified; else return formula; } return formula; } /** * takes a linear arithmetic expression as a term and returns 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 = SMTAffineTerm.create(Rational.ZERO, m_theory.getRealSort()); for (Term param : at.getParameters()) result = result.add(toAffineTerm(param)); return result; } else if (at.getFunction().getName() == "-") { SMTAffineTerm result = SMTAffineTerm.create(Rational.ZERO, m_theory.getRealSort()); result = result.add(toAffineTerm(at.getParameters()[0])); result = result.add(toAffineTerm(at.getParameters()[1]).negate()); return result; } else if (at.getFunction().getName() == "*") { SMTAffineTerm recResult1 = toAffineTerm(at.getParameters()[0]); SMTAffineTerm recResult2 = toAffineTerm(at.getParameters()[1]); if (recResult1.isConstant()) return recResult2.mul(recResult1.getConstant()); else if (recResult2.isConstant()) return recResult1.mul(recResult2.getConstant()); else assert false; } else if(at.getFunction().getName() == "/") { SMTAffineTerm recResult1 = toAffineTerm(at.getParameters()[0]); SMTAffineTerm recResult2 = toAffineTerm(at.getParameters()[1]); assert recResult2.isConstant(); return recResult1.div(recResult2.getConstant()); } else { //we have a constant assert at.getParameters().length == 0; return SMTAffineTerm.create(Rational.ONE, at); } } else if (term instanceof ConstantTerm) { return SMTAffineTerm.create(term); } else if (term instanceof TermVariable) { return SMTAffineTerm.create(Rational.ONE, term); } return null; } }