TIP import: handle primitive Int type

[jvierling]

Running TipSmtParser.fixupAndParse on the file tip2015/sort_MSortTDPermutes.smt2 from the TIP-Library produces a java.util.NoSuchElementException exception.

Example:

import at.logic.gapt.formats.tip.TipSmtParser
import better.files._

object Bug {
  def main(args: Array[String]): Unit = {
    TipSmtParser fixupAndParse "./../benchmarks/benchmarks/tip2015/sort_MSortTDPermutes.smt2".toFile
  }
}

Output:

Exception in thread "main" java.util.NoSuchElementException: key not found: Int
	at scala.collection.MapLike$class.default(MapLike.scala:228)
	at scala.collection.AbstractMap.default(Map.scala:59)
	at scala.collection.mutable.HashMap.apply(HashMap.scala:65)
	at at.logic.gapt.formats.tip.TipSmtParser.parseField(tipsmt.scala:78)
	at at.logic.gapt.formats.tip.TipSmtParser$$anonfun$7.apply(tipsmt.scala:71)
	at at.logic.gapt.formats.tip.TipSmtParser$$anonfun$7.apply(tipsmt.scala:71)
	at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
	at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
	at scala.collection.Iterator$class.foreach(Iterator.scala:893)
	at scala.collection.AbstractIterator.foreach(Iterator.scala:1336)
	at scala.collection.IterableLike$class.foreach(IterableLike.scala:72)
	at scala.collection.AbstractIterable.foreach(Iterable.scala:54)
	at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
	at scala.collection.AbstractTraversable.map(Traversable.scala:104)
	at at.logic.gapt.formats.tip.TipSmtParser.parseConstructor(tipsmt.scala:71)
	at at.logic.gapt.formats.tip.TipSmtParser$$anonfun$2.apply(tipsmt.scala:38)
	at at.logic.gapt.formats.tip.TipSmtParser$$anonfun$2.apply(tipsmt.scala:38)
	at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
	at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
	at scala.collection.Iterator$class.foreach(Iterator.scala:893)
	at scala.collection.AbstractIterator.foreach(Iterator.scala:1336)
	at scala.collection.IterableLike$class.foreach(IterableLike.scala:72)
	at scala.collection.AbstractIterable.foreach(Iterable.scala:54)
	at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
	at scala.collection.AbstractTraversable.map(Traversable.scala:104)
	at at.logic.gapt.formats.tip.TipSmtParser.parse(tipsmt.scala:38)
	at at.logic.gapt.formats.tip.TipSmtParser$$anonfun$parse$4.apply(tipsmt.scala:156)
	at at.logic.gapt.formats.tip.TipSmtParser$$anonfun$parse$4.apply(tipsmt.scala:156)
	at scala.collection.immutable.List.foreach(List.scala:381)
	at at.logic.gapt.formats.tip.TipSmtParser$.parse(tipsmt.scala:156)
	at at.logic.gapt.formats.tip.TipSmtParser$.fixupAndParse(tipsmt.scala:161)

A similar behaviour occurs when running TipSmtParser.fixupAndParse on the following files:

benchmarks/tip2015/sort_MSortTDPermutes.smt2 : java.util.NoSuchElementException: key not found: Int
benchmarks/tip2015/sort_MSortBU2Count.smt2 : java.util.NoSuchElementException: key not found: match
benchmarks/tip2015/sort_StoogeSort2Permutes.smt2 : java.util.NoSuchElementException: key not found: Int
benchmarks/tip2015/sort_StoogeSort2Sorts.smt2 : java.util.NoSuchElementException: key not found: Int
benchmarks/tip2015/sort_StoogeSort2Count.smt2 : java.util.NoSuchElementException: key not found: Int
benchmarks/tip2015/mccarthy91_M1.smt2 : java.util.NoSuchElementException: key not found: Int
benchmarks/tip2015/sort_MSortTDSorts.smt2 : java.util.NoSuchElementException: key not found: Int
benchmarks/tip2015/sort_StoogeSortIsSort.smt2 : java.util.NoSuchElementException: key not found: Int
benchmarks/tip2015/sort_BubSortCount.smt2 : java.util.NoSuchElementException: key not found: match
benchmarks/tip2015/sort_BubSortPermutes.smt2 : java.util.NoSuchElementException: key not found: match
benchmarks/tip2015/sort_MSortBU2Sorts.smt2 : java.util.NoSuchElementException: key not found: match
benchmarks/tip2015/polyrec_seq_index.smt2 : java.util.NoSuchElementException: key not found: Int
benchmarks/tip2015/fermat_last.smt2 : java.util.NoSuchElementException: key not found: distinct
benchmarks/tip2015/sort_StoogeSort2IsSort.smt2 : java.util.NoSuchElementException: key not found: Int
benchmarks/tip2015/sort_StoogeSortCount.smt2 : java.util.NoSuchElementException: key not found: Int
benchmarks/tip2015/subst_SubstFreeNo.smt2 : java.util.NoSuchElementException: key not found: Int
benchmarks/tip2015/sort_MSortBU2Permutes.smt2 : java.util.NoSuchElementException: key not found: match
benchmarks/tip2015/sort_MSortTDIsSort.smt2 : java.util.NoSuchElementException: key not found: Int
benchmarks/tip2015/subst_SubstFreeYes.smt2 : java.util.NoSuchElementException: key not found: Int
benchmarks/tip2015/sort_MSortBU2IsSort.smt2 : java.util.NoSuchElementException: key not found: match
benchmarks/tip2015/sort_MSortTDCount.smt2 : java.util.NoSuchElementException: key not found: Int
benchmarks/tip2015/sort_BubSortIsSort.smt2 : java.util.NoSuchElementException: key not found: match
benchmarks/tip2015/sort_BubSortSorts.smt2 : java.util.NoSuchElementException: key not found: match
benchmarks/tip2015/mccarthy91_M2.smt2 : java.util.NoSuchElementException: key not found: Int
benchmarks/tip2015/sort_StoogeSortPermutes.smt2 : java.util.NoSuchElementException: key not found: Int
benchmarks/tip2015/sort_StoogeSortSorts.smt2 : java.util.NoSuchElementException: key not found: Int

[loewenheim]

The reason for this error is this: In the original smt file, there's a declaration of a parametric datatype list. When we call the tip tool on the file, types are monomorphized, which means that type parameters are replaced with "Int", but the declaration of the Int type is not added to the file. I can't say whether that is a problem with our code or with the tip tool.

[jvierling]

The --int-to-nat option is not always able to replace integers by natural numbers. In such cases we need to interpret or define the type Int, its functions, constants and predicates. We could do this by reducing the integers to pairs of natural numbers but I don't know if this is a viable approach.

@gebner What do you think about this?