Support splitting in erasure reduction

[jvierling]

Example:

  def main( args: Array[String] ): Unit = {
    val reduction = CNFReductionLKRes |> PredicateReductionCNF |> ErasureReductionCNF
    val tip     = TipSmtParser.fixupAndParse("./../benchmarks/benchmarks/tip2015/nat_pow_one.smt2".toFile)
    val problem = tip.toSequent
    implicit val context = tip.context
    sequentialInductionAxioms.inductionAxioms(problem.succedent.head, List(hov"x:Nat")) match {
      case Success(axioms) => {
        val sequent            = axioms ++: problem
        val (folProblem, back) = reduction forward (Sequent() :+ sequent.toImplication)
        SPASS.getResolutionProof(folProblem) map back
      }
    }
  }
}

Output:

Exception in thread "main" java.util.NoSuchElementException: key not found: _split2_0:o
	at scala.collection.MapLike$class.default(MapLike.scala:228)
	at scala.collection.AbstractMap.default(Map.scala:59)
	at scala.collection.MapLike$class.apply(MapLike.scala:141)
	at scala.collection.AbstractMap.apply(Map.scala:59)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.at$logic$gapt$proofs$reduction$ErasureReductionHelper$$i$1(manySorted.scala:111)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.infer(manySorted.scala:134)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.infer(manySorted.scala:95)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper$$anonfun$g$1$1.apply(manySorted.scala:179)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper$$anonfun$g$1$1.apply(manySorted.scala:150)
	at scala.collection.mutable.MapLike$class.getOrElseUpdate(MapLike.scala:194)
	at scala.collection.mutable.AbstractMap.getOrElseUpdate(Map.scala:80)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.g$1(manySorted.scala:150)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.at$logic$gapt$proofs$reduction$ErasureReductionHelper$$f$1(manySorted.scala:147)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.back(manySorted.scala:198)
	at at.logic.gapt.proofs.reduction.ErasureReductionCNF$$anonfun$forward$7.apply(manySorted.scala:258)
	at at.logic.gapt.proofs.reduction.ErasureReductionCNF$$anonfun$forward$7.apply(manySorted.scala:258)
	at at.logic.gapt.proofs.reduction.CombinedReduction$$anonfun$forward$1.apply(manySorted.scala:46)
	at scala.Option.map(Option.scala:146)
	at at.logic.gapt.provers.viper.Example$.main(Bug.scala:25)
	at at.logic.gapt.provers.viper.Example.main(Bug.scala)

[gebner]

Yeah, splitting is not really supported in the back-translation. Can you try eliminateSplitting on the resolution proof first? We might want to add that call to ErasureReductionCNF then.

[jvierling]

Applying eliminateSplitting on the resolution proof worked.