Skip to content

Commit db32d02

Browse files
HeizmannHeizmann
committed
centralized exception handling in array PQE
1 parent 72227a9 commit db32d02

File tree

3 files changed

+112
-72
lines changed

3 files changed

+112
-72
lines changed

‎trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/smt/DerPreprocessor.java‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@
3838

3939
import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger;
4040
import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider;
41+
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.ElimStorePlain.ElimStorePlainException;
4142
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.arrays.ArrayIndex;
4243
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.arrays.MultiDimensionalNestedStore;
4344
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.arrays.MultiDimensionalSelect;
@@ -91,7 +92,7 @@ private enum DerCase {
9192

9293
public DerPreprocessor(final IUltimateServiceProvider services, final ManagedScript mgdScript, final int quantifier,
9394
final TermVariable eliminatee, final Term input, final List<BinaryEqualityRelation> bers,
94-
final ArrayIndexEqualityManager aiem) {
95+
final ArrayIndexEqualityManager aiem) throws ElimStorePlainException {
9596
final HashRelation<DerCase, BinaryEqualityRelation> classification = classify(mgdScript.getScript(), bers,
9697
eliminatee);
9798
boolean existsEqualityThatIsNotOnTopLevel = false;
@@ -185,7 +186,7 @@ private static Term constructDerEnabler(final BinaryEqualityRelation someTopLeve
185186
}
186187

187188
private static HashRelation<DerCase, BinaryEqualityRelation> classify(final Script script,
188-
final List<BinaryEqualityRelation> bers, final TermVariable eliminatee) {
189+
final List<BinaryEqualityRelation> bers, final TermVariable eliminatee) throws ElimStorePlainException {
189190
final HashRelation<DerCase, BinaryEqualityRelation> result = new HashRelation<>();
190191
for (final BinaryEqualityRelation ber : bers) {
191192
final Term otherSide = getOtherSide(ber, eliminatee);
@@ -207,9 +208,9 @@ private static Term getOtherSide(final BinaryEqualityRelation ber, final TermVar
207208
return otherSide;
208209
}
209210

210-
private static DerCase classify(final Script script, final Term otherSide, final TermVariable eliminatee) {
211+
private static DerCase classify(final Script script, final Term otherSide, final TermVariable eliminatee) throws ElimStorePlainException {
211212
if (!Arrays.asList(otherSide.getFreeVars()).contains(eliminatee)) {
212-
throw new AssertionError("This case should habe been handled by DER");
213+
throw new ElimStorePlain.ElimStorePlainException("This case should habe been handled by DER");
213214
}
214215
final MultiDimensionalNestedStore mdns = MultiDimensionalNestedStore.convert(script, otherSide);
215216
if (mdns != null) {

‎trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/smt/ElimStorePlain.java‎

Lines changed: 106 additions & 67 deletions
Original file line numberDiff line numberDiff line change
@@ -53,8 +53,8 @@
5353
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.arrays.MultiDimensionalSort;
5454
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.linearterms.PrenexNormalForm;
5555
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.linearterms.QuantifierPusher;
56-
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.linearterms.QuantifierSequence;
5756
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.linearterms.QuantifierPusher.PqeTechniques;
57+
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.linearterms.QuantifierSequence;
5858
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.linearterms.QuantifierSequence.QuantifiedVariables;
5959
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.managedscript.ManagedScript;
6060
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.normalforms.NnfTransformer;
@@ -120,6 +120,7 @@ public class ElimStorePlain {
120120

121121
private static final boolean RETURN_AFTER_SOS = false;
122122
private static final boolean TRANSFORM_TO_XNF_ON_SPLIT = false;
123+
private static final boolean THROW_ELIMINATION_EXCEPTIONS = false;
123124
private final ManagedScript mMgdScript;
124125
private final IUltimateServiceProvider mServices;
125126
private final ILogger mLogger;
@@ -139,69 +140,84 @@ public ElimStorePlain(final ManagedScript mgdScript, final IUltimateServiceProvi
139140
* Old, iterative elimination. Is sound but if we cannot eliminate all
140141
* quantifiers it sometimes produces a large number of similar
141142
* disjuncts/conjuncts that is too large for simplification.
143+
* @throws ElimStorePlainException
142144
*
143145
*/
144146
public EliminationTask elimAll(final EliminationTask eTask) {
147+
try {
145148

146-
final Stack<EliminationTask> taskStack = new Stack<>();
147-
final ArrayList<Term> resultDisjuncts = new ArrayList<>();
148-
final Set<TermVariable> resultEliminatees = new LinkedHashSet<>();
149-
{
150-
final EliminationTask eliminationTask = new EliminationTask(eTask.getQuantifier(), eTask.getEliminatees(),
151-
eTask.getTerm());
152-
pushTaskOnStack(eliminationTask, taskStack);
153-
}
154-
int numberOfRounds = 0;
155-
while (!taskStack.isEmpty()) {
156-
final EliminationTask currentETask = taskStack.pop();
157-
final TreeRelation<Integer, TermVariable> tr = classifyEliminatees(currentETask.getEliminatees());
149+
final Stack<EliminationTask> taskStack = new Stack<>();
150+
final ArrayList<Term> resultDisjuncts = new ArrayList<>();
151+
final Set<TermVariable> resultEliminatees = new LinkedHashSet<>();
152+
{
153+
final EliminationTask eliminationTask = new EliminationTask(eTask.getQuantifier(),
154+
eTask.getEliminatees(), eTask.getTerm());
155+
pushTaskOnStack(eliminationTask, taskStack);
156+
}
157+
int numberOfRounds = 0;
158+
while (!taskStack.isEmpty()) {
159+
final EliminationTask currentETask = taskStack.pop();
160+
final TreeRelation<Integer, TermVariable> tr = classifyEliminatees(currentETask.getEliminatees());
158161

159-
final LinkedHashSet<TermVariable> arrayEliminatees = getArrayTvSmallDimensionsFirst(tr);
162+
final LinkedHashSet<TermVariable> arrayEliminatees = getArrayTvSmallDimensionsFirst(tr);
160163

161-
if (arrayEliminatees.isEmpty()) {
162-
// no array eliminatees left
163-
resultDisjuncts.add(currentETask.getTerm());
164-
resultEliminatees.addAll(currentETask.getEliminatees());
165-
} else {
166-
TermVariable thisIterationEliminatee;
167-
{
168-
final Iterator<TermVariable> it = arrayEliminatees.iterator();
169-
thisIterationEliminatee = it.next();
170-
it.remove();
171-
}
172-
final EliminationTaskWithContext etwc = new EliminationTaskWithContext(currentETask.getQuantifier(),
173-
Collections.singleton(thisIterationEliminatee), currentETask.getTerm(), null);
174-
final EliminationTask ssdElimRes = new Elim1Store(mMgdScript, mServices, mSimplificationTechnique,
175-
eTask.getQuantifier()).elim1(etwc);
176-
arrayEliminatees.addAll(ssdElimRes.getEliminatees());
177-
// also add non-array eliminatees
178-
arrayEliminatees.addAll(tr.getImage(0));
179-
final EliminationTaskWithContext eliminationTask1 = new EliminationTaskWithContext(ssdElimRes.getQuantifier(),
180-
arrayEliminatees, ssdElimRes.getTerm(), null);
181-
final EliminationTaskWithContext eliminationTask2 = applyNonSddEliminations(mServices, mMgdScript,
182-
eliminationTask1, PqeTechniques.ALL_LOCAL);
183-
if (mLogger.isInfoEnabled()) {
184-
mLogger.info("Start of round: " + printVarInfo(tr) + " End of round: "
185-
+ printVarInfo(classifyEliminatees(eliminationTask2.getEliminatees())) + " and "
186-
+ QuantifierUtils.getXjunctsOuter(eTask.getQuantifier(), eliminationTask2.getTerm()).length
187-
+ " xjuncts.");
188-
}
189-
// assert (!maxSizeIncrease(tr, classifyEliminatees(eliminationTask2.getEliminatees()))) : "number of max-dim elements increased!";
164+
if (arrayEliminatees.isEmpty()) {
165+
// no array eliminatees left
166+
resultDisjuncts.add(currentETask.getTerm());
167+
resultEliminatees.addAll(currentETask.getEliminatees());
168+
} else {
169+
TermVariable thisIterationEliminatee;
170+
{
171+
final Iterator<TermVariable> it = arrayEliminatees.iterator();
172+
thisIterationEliminatee = it.next();
173+
it.remove();
174+
}
175+
final EliminationTaskWithContext etwc = new EliminationTaskWithContext(currentETask.getQuantifier(),
176+
Collections.singleton(thisIterationEliminatee), currentETask.getTerm(), null);
177+
final EliminationTask ssdElimRes = new Elim1Store(mMgdScript, mServices, mSimplificationTechnique,
178+
eTask.getQuantifier()).elim1(etwc);
179+
arrayEliminatees.addAll(ssdElimRes.getEliminatees());
180+
// also add non-array eliminatees
181+
arrayEliminatees.addAll(tr.getImage(0));
182+
final EliminationTaskWithContext eliminationTask1 = new EliminationTaskWithContext(
183+
ssdElimRes.getQuantifier(), arrayEliminatees, ssdElimRes.getTerm(), null);
184+
final EliminationTaskWithContext eliminationTask2 = applyNonSddEliminations(mServices, mMgdScript,
185+
eliminationTask1, PqeTechniques.ALL_LOCAL);
186+
if (mLogger.isInfoEnabled()) {
187+
mLogger.info("Start of round: " + printVarInfo(tr) + " End of round: "
188+
+ printVarInfo(classifyEliminatees(eliminationTask2.getEliminatees())) + " and "
189+
+ QuantifierUtils.getXjunctsOuter(eTask.getQuantifier(),
190+
eliminationTask2.getTerm()).length
191+
+ " xjuncts.");
192+
}
193+
// assert (!maxSizeIncrease(tr,
194+
// classifyEliminatees(eliminationTask2.getEliminatees()))) : "number of max-dim
195+
// elements increased!";
190196

191-
pushTaskOnStack(eliminationTask2, taskStack);
197+
pushTaskOnStack(eliminationTask2, taskStack);
198+
}
199+
numberOfRounds++;
200+
}
201+
mLogger.info("Needed " + numberOfRounds + " rounds to eliminate " + eTask.getEliminatees().size()
202+
+ " variables, produced " + resultDisjuncts.size() + " xjuncts");
203+
// return term and variables that we could not eliminate
204+
return new EliminationTask(eTask.getQuantifier(), resultEliminatees,
205+
QuantifierUtils.applyCorrespondingFiniteConnective(mMgdScript.getScript(), eTask.getQuantifier(),
206+
resultDisjuncts));
207+
} catch (final ElimStorePlainException e) {
208+
if (THROW_ELIMINATION_EXCEPTIONS) {
209+
throw new UnsupportedOperationException(e);
210+
} else {
211+
return new EliminationTask(eTask.getQuantifier(), new HashSet<>(eTask.getEliminatees()),
212+
eTask.getTerm());
192213
}
193-
numberOfRounds++;
194214
}
195-
mLogger.info("Needed " + numberOfRounds + " rounds to eliminate " + eTask.getEliminatees().size()
196-
+ " variables, produced " + resultDisjuncts.size() + " xjuncts");
197-
// return term and variables that we could not eliminate
198-
return new EliminationTask(eTask.getQuantifier(), resultEliminatees, QuantifierUtils
199-
.applyCorrespondingFiniteConnective(mMgdScript.getScript(), eTask.getQuantifier(), resultDisjuncts));
200215
}
201216

202217
/**
203218
* New recursive elimination. Public method for starting the algorithm, not
204219
* suitable for recursive calls.
220+
* @throws ElimStorePlainException
205221
*/
206222
public EliminationTask startRecursiveElimination(final EliminationTask eTask) {
207223
final TreeRelation<Integer, TermVariable> tr = classifyEliminatees(eTask.getEliminatees());
@@ -213,19 +229,28 @@ public EliminationTask startRecursiveElimination(final EliminationTask eTask) {
213229
final long inputSize = new DAGSize().treesize(eTask.getTerm());
214230
// Initially, the context is "true" (context is independent quantifier)
215231
final Term initialContext = mMgdScript.getScript().term("true");
216-
final EliminationTask result = doElimAllRec(new EliminationTaskWithContext(eTask.getQuantifier(),
217-
eTask.getEliminatees(), eTask.getTerm(), initialContext));
218-
final long outputSize = new DAGSize().treesize(result.getTerm());
219-
// TODO 2019-02-20 Matthias: If implementation is more matured then show this
220-
// output only if there was a big increase in the size of the formula.
221-
mLogger.info(String.format(
222-
"Needed %s recursive calls to eliminate %s variables, input treesize:%s, output treesize:%s",
223-
mRecursiveCallCounter, eTask.getEliminatees().size(), inputSize, outputSize));
224-
return result;
232+
EliminationTask result;
233+
try {
234+
result = doElimAllRec(new EliminationTaskWithContext(eTask.getQuantifier(),
235+
eTask.getEliminatees(), eTask.getTerm(), initialContext));
236+
final long outputSize = new DAGSize().treesize(result.getTerm());
237+
// TODO 2019-02-20 Matthias: If implementation is more matured then show this
238+
// output only if there was a big increase in the size of the formula.
239+
mLogger.info(String.format(
240+
"Needed %s recursive calls to eliminate %s variables, input treesize:%s, output treesize:%s",
241+
mRecursiveCallCounter, eTask.getEliminatees().size(), inputSize, outputSize));
242+
return result;
243+
} catch (final ElimStorePlainException e) {
244+
if (THROW_ELIMINATION_EXCEPTIONS) {
245+
throw new UnsupportedOperationException(e);
246+
} else {
247+
return new EliminationTask(eTask.getQuantifier(), new HashSet<>(eTask.getEliminatees()), eTask.getTerm());
248+
}
249+
}
225250
}
226251

227252

228-
private EliminationTaskWithContext doElimOneRec(final EliminationTaskWithContext eTask) {
253+
private EliminationTaskWithContext doElimOneRec(final EliminationTaskWithContext eTask) throws ElimStorePlainException {
229254
if (QuantifierUtils.getXjunctsOuter(eTask.getQuantifier(),eTask.getTerm()).length != 1) {
230255
throw new AssertionError("Input not split");
231256
}
@@ -272,15 +297,15 @@ private EliminationTaskWithContext doElimOneRec(final EliminationTaskWithContext
272297
resultOfRecursiveCall.getEliminatees(), resultTerm, eTask.getContext());
273298
}
274299

275-
private EliminationTaskWithContext applyComplexEliminationRules(final EliminationTaskWithContext eTask) {
300+
private EliminationTaskWithContext applyComplexEliminationRules(final EliminationTaskWithContext eTask) throws ElimStorePlainException {
276301
final TermVariable eliminatee;
277302
if (eTask.getEliminatees().size() != 1) {
278303
throw new AssertionError("need exactly one eliminatee");
279304
} else {
280305
eliminatee = eTask.getEliminatees().iterator().next();
281306
}
282307
if (!QuantifierUtils.isQuantifierFree(eTask.getTerm())) {
283-
throw new AssertionError("Alternating quantifiers not yet supported");
308+
throw new ElimStorePlainException("Alternating quantifiers not yet supported");
284309
}
285310
final Term polarizedContext = QuantifierUtils.negateIfUniversal(mServices, mMgdScript,
286311
eTask.getQuantifier(), eTask.getContext());
@@ -384,7 +409,8 @@ private boolean varOccurs(final TermVariable var, final Term term) {
384409
return Arrays.stream(term.getFreeVars()).anyMatch(x -> (x == var));
385410
}
386411

387-
private EliminationTaskWithContext doElimAllRec(final EliminationTaskWithContext eTask) {
412+
private EliminationTaskWithContext doElimAllRec(final EliminationTaskWithContext eTask)
413+
throws ElimStorePlainException {
388414
mRecursiveCallCounter++;
389415
final int thisRecursiveCallNumber = mRecursiveCallCounter;
390416

@@ -534,7 +560,7 @@ private ArrayIndexBasedCostEstimation computeCostEstimation(final EliminationTas
534560
return costs;
535561
}
536562

537-
private EliminationTaskWithContext eliminateOne(final EliminationTaskWithContext eTaskForVar) {
563+
private EliminationTaskWithContext eliminateOne(final EliminationTaskWithContext eTaskForVar) throws ElimStorePlainException {
538564
final TermVariable eliminatee = eTaskForVar.getEliminatees().iterator().next();
539565
final Set<TermVariable> newElimnateesForVar = new LinkedHashSet<>();
540566
final Term[] correspondingJunctiveNormalForm;
@@ -667,7 +693,8 @@ private void pushTaskOnStack(final EliminationTask eTask, final Stack<Eliminatio
667693
}
668694

669695
public static EliminationTaskWithContext applyNonSddEliminations(final IUltimateServiceProvider services,
670-
final ManagedScript mgdScript, final EliminationTaskWithContext eTask, final PqeTechniques techniques) {
696+
final ManagedScript mgdScript, final EliminationTaskWithContext eTask, final PqeTechniques techniques)
697+
throws ElimStorePlainException {
671698
final Term quantified = SmtUtils.quantifier(mgdScript.getScript(), eTask.getQuantifier(),
672699
eTask.getEliminatees(), eTask.getTerm());
673700
final Term pushed = new QuantifierPusher(mgdScript, services, true, techniques).transform(quantified);
@@ -683,10 +710,10 @@ public static EliminationTaskWithContext applyNonSddEliminations(final IUltimate
683710
} else if (qvs.size() == 1) {
684711
eliminatees1 = qvs.get(0).getVariables();
685712
if (qvs.get(0).getQuantifier() != eTask.getQuantifier()) {
686-
throw new UnsupportedOperationException("alternation not yet supported");
713+
throw new ElimStorePlainException("alternation not yet supported");
687714
}
688715
} else if (qvs.size() > 1) {
689-
throw new UnsupportedOperationException("alternation not yet supported: " + pnf);
716+
throw new ElimStorePlainException("alternation not yet supported: " + pnf);
690717
} else {
691718
throw new AssertionError();
692719
}
@@ -739,4 +766,16 @@ private static boolean maxSizeIncrease(final TreeRelation<Integer, TermVariable>
739766

740767
}
741768

769+
public static class ElimStorePlainException extends Exception {
770+
private static final long serialVersionUID = 7719170889993834143L;
771+
private final String mMessage;
772+
private final TermVariable mEliminatee;
773+
774+
public ElimStorePlainException(final String message) {
775+
super(message);
776+
mEliminatee = null;
777+
mMessage = message;
778+
}
779+
}
780+
742781
}

‎trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/smt/PartialQuantifierElimination.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,8 +42,8 @@
4242
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.SmtUtils.XnfConversionTechnique;
4343
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.linearterms.PrenexNormalForm;
4444
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.linearterms.QuantifierPusher;
45-
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.linearterms.QuantifierSequence;
4645
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.linearterms.QuantifierPusher.PqeTechniques;
46+
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.linearterms.QuantifierSequence;
4747
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.linearterms.QuantifierSequence.QuantifiedVariables;
4848
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.managedscript.ManagedScript;
4949
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.normalforms.NnfTransformer;

0 commit comments

Comments
 (0)