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