I tried to have a look at expansion proof deskolemization for my nTapeX proofs. For the nTape2 variant, I get some errors I was looking to fix but when I checked the nTape3 proof, I got a very strange error message:
gapt> deskolemizeET( nTape3.expansion_proof )
java.lang.IllegalArgumentException: Comparison method violates its general contract!
at java.base/java.util.TimSort.mergeLo(TimSort.java:777)
at java.base/java.util.TimSort.mergeAt(TimSort.java:514)
at java.base/java.util.TimSort.mergeForceCollapse(TimSort.java:457)
at java.base/java.util.TimSort.sort(TimSort.java:254)
at java.base/java.util.Arrays.sort(Arrays.java:1440)
at scala.collection.SeqLike.sorted(SeqLike.scala:656)
at scala.collection.SeqLike.sorted$(SeqLike.scala:644)
at scala.collection.AbstractSeq.sorted(Seq.scala:41)
at scala.collection.SeqLike.sortWith(SeqLike.scala:609)
at scala.collection.SeqLike.sortWith$(SeqLike.scala:609)
at scala.collection.AbstractSeq.sortWith(Seq.scala:41)
at scala.collection.SeqViewLike.$anonfun$sortWith$1(SeqViewLike.scala:261)
at scala.collection.SeqViewLike$$anon$1.<init>(SeqViewLike.scala:193)
at scala.collection.SeqViewLike.newForced(SeqViewLike.scala:193)
at scala.collection.SeqViewLike.newForced$(SeqViewLike.scala:193)
at scala.collection.SeqViewLike$AbstractTransformed.newForced(SeqViewLike.scala:37)
at scala.collection.SeqViewLike.sortWith(SeqViewLike.scala:261)
at scala.collection.SeqViewLike.sortWith$(SeqViewLike.scala:260)
at scala.collection.SeqViewLike$AbstractTransformed.sortWith(SeqViewLike.scala:37)
at gapt.proofs.expansion.removeSkolemCongruences$.simplCongrs(removeSkolemCongruences.scala:71)
at gapt.proofs.expansion.removeSkolemCongruences$.remove(removeSkolemCongruences.scala:83)
at gapt.proofs.expansion.removeSkolemCongruences$.apply(removeSkolemCongruences.scala:87)
at gapt.proofs.expansion.deskolemizeET$.apply(deskolemizeET.scala:17)
... 25 elided
Looking into removeSkolemCongruences, the offending function defines:
val lpo = LPO( containedNames( congrs ).collect { case c: Const => c }.toSeq.sortBy( _.name ) )
def lt( a: Expr, b: Expr ): Boolean = lpo.lt( a, b, true )
and later on calls
sortWith( ( c1, c2 ) => lt( c1._1, c2._1 ) )
where the error occurs. I still need to look up if LPOs naturally generalize to higher order terms (which occur in there) but in any case, the compare should be the one throwing an error for cases where the ordering breaks, not the sorting algorithm.
I tried to have a look at expansion proof deskolemization for my nTapeX proofs. For the nTape2 variant, I get some errors I was looking to fix but when I checked the nTape3 proof, I got a very strange error message:
Looking into removeSkolemCongruences, the offending function defines:
and later on calls
where the error occurs. I still need to look up if LPOs naturally generalize to higher order terms (which occur in there) but in any case, the compare should be the one throwing an error for cases where the ordering breaks, not the sorting algorithm.