Princess: Unknown abbreviation symbols

[daniel-raffler]

Hello

We're seeing a lot of NoSuchElementException when using Princess in CPAchecker:

Exception in thread "main" java.util.NoSuchElementException: key not found: abbrev_57/0
	at scala.collection.immutable.BitmapIndexedMapNode.apply(HashMap.scala:674)
	at scala.collection.immutable.BitmapIndexedMapNode.apply(HashMap.scala:672)
	at scala.collection.immutable.HashMap.apply(HashMap.scala:132)
	at ap.util.FastImmutableMap.apply(FastImmutableMap.scala:72)
	at ap.terfor.TermOrder.compare(TermOrder.scala:452)
	at ap.terfor.preds.PredConj$.$anonfun$sort$4(PredConj.scala:53)
	at ap.terfor.preds.PredConj$.$anonfun$sort$4$adapted(PredConj.scala:53)
	at scala.math.Ordering$$anon$4.compare(Ordering.scala:316)
	at java.base/java.util.TimSort.countRunAndMakeAscending(TimSort.java:355)
	at java.base/java.util.TimSort.sort(TimSort.java:220)
	at java.base/java.util.Arrays.sort(Arrays.java:1307)
	at scala.util.Sorting$.stableSort(Sorting.scala:240)
	at ap.util.Seqs$.filterAndSort(Seqs.scala:620)
	at ap.terfor.preds.PredConj$.sort(PredConj.scala:51)
	at ap.terfor.preds.PredConj$.apply(PredConj.scala:75)
	at ap.terfor.preds.PredConj$.$anonfun$conj$1(PredConj.scala:132)
	at ap.terfor.Formula$.conj(Formula.scala:69)
	at ap.terfor.preds.PredConj$.conj(PredConj.scala:121)
	at ap.terfor.conjunctions.Conjunction$.segregateFormulas(Conjunction.scala:143)
	at ap.terfor.conjunctions.Conjunction$.apply(Conjunction.scala:66)
	at ap.terfor.conjunctions.Conjunction$.apply(Conjunction.scala:79)
	at ap.terfor.conjunctions.Conjunction$.conj(Conjunction.scala:156)
	at ap.terfor.conjunctions.AndLazyConjunction.toConjunction(LazyConjunction.scala:233)
	at ap.terfor.conjunctions.NegLazyConjunction.toFormula(LazyConjunction.scala:176)
	at ap.terfor.conjunctions.NegLazyConjunction.$amp(LazyConjunction.scala:187)
	at ap.terfor.conjunctions.LazyConjunction.$bar(LazyConjunction.scala:96)
	at ap.parser.InputAbsy2Internal.ap$parser$InputAbsy2Internal$$translateFor(InputAbsy2Internal.scala:221)
	at ap.parser.InputAbsy2Internal$.apply(InputAbsy2Internal.scala:59)
	at ap.api.SimpleAPI.toInternal(SimpleAPI.scala:4363)
	at ap.api.SimpleAPI.flushTodo(SimpleAPI.scala:4108)
	at ap.api.SimpleAPI.checkSatHelp(SimpleAPI.scala:2034)
	at ap.api.SimpleAPI.checkSat(SimpleAPI.scala:2020)
	at org.sosy_lab.java_smt.solvers.princess.PrincessAbstractProver.isUnsatImpl(PrincessAbstractProver.java:82)

Some of these were caused by an issue in Princess. However, this has now been fixed, and the remaining crashes are caused by JavaSMT

The problem is, that we're using abbrevSharedExpressions before pushing assertions. This adds additional internal symbols to the term, which can then "leak" into interpolants, and cause the NoSuchElementException later on when the term is used with a different prover

There are several ways to fix it. The easiest solution would be to simply not use abbrevSharedExpressions. However, this may make Princess slower, especially on more complex problems. A better solution may be to track the introduced symbols and then export them to other solvers. Alternatively, we could try to eliminate all abbreviation symbols from interpolants before they can be used anywhere else

[PhilippWendler]

cause the NoSuchElementException later on when the term is used with a different prover

This is a red hering, and "exporting" additional symbols to other solvers is not the right solution and not something that JavaSMT can even do (or are you going to insert arbitrary stuff into every future solver context that a user creates just because they happened to have performed some interpolation with Princess before?).

The real problem is that interpolants that contain additional internal symbols (apart from let terms and similar stuff) are not valid interpolants because they do not fulfill the third condition of interpolants (only symbols that are present in both A and B are allowed in the interpolant). And this is what needs to be fixed, likely by expanding abbreviations.