erasure reduction: handle Skolemization inferences

[jvierling]

I'm not sure if this is a bug or if it is due to some unsatisfied precondition in the input of the reduction.

import at.logic.gapt.expr._
import at.logic.gapt.formats.tip.TipSmtParser
import at.logic.gapt.proofs.Sequent
import at.logic.gapt.proofs.reduction.{ErasureReductionET, PredicateReductionET}
import at.logic.gapt.provers.spass.SPASS
import better.files._

import scalaz.Success

object Example {
  def main( args: Array[String] ): Unit = {
    val reduction = PredicateReductionET |> ErasureReductionET
    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.getExpansionProof(folProblem) map back
      }
    }
  }
}

The output is:

Exception in thread "main" scala.MatchError: (∀x_0 (P_is_Nat(x_0) ⊃
      f_pow(f_S(f_Z), x_0) = f_S(f_Z) ⊃
      f_pow(f_S(f_Z), f_S(x_0)) = f_S(f_Z)) +sk^{s_0}
  (P_is_Nat(s_0)- ⊃
    ((f_pow(f_S(f_Z), s_0) = f_S(f_Z))- ⊃
      (f_pow(f_S(f_Z), f_S(s_0)) = f_S(f_Z))+)),∀x_0 (is_Nat(x_0:Nat) ⊃
    (pow(S(#c(Z: Nat)): Nat, x_0): Nat) = S(#c(Z: Nat)) ⊃
    pow(S(#c(Z: Nat)), S(x_0)) = S(#c(Z: Nat)))) (of class scala.Tuple2)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.back(manySorted.scala:201)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.back(manySorted.scala:207)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.back(manySorted.scala:209)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.back(manySorted.scala:207)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.back(manySorted.scala:207)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.back(manySorted.scala:207)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.back(manySorted.scala:207)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.back(manySorted.scala:207)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.back(manySorted.scala:207)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.back(manySorted.scala:207)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.back(manySorted.scala:207)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.back(manySorted.scala:207)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.back(manySorted.scala:209)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper$$anonfun$back$8$$anonfun$apply$4.apply(manySorted.scala:227)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper$$anonfun$back$8$$anonfun$apply$4.apply(manySorted.scala:225)
	at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:683)
	at scala.collection.immutable.List.foreach(List.scala:381)
	at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:682)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper$$anonfun$back$8.apply(manySorted.scala:225)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper$$anonfun$back$8.apply(manySorted.scala:224)
	at scala.collection.TraversableLike$$anonfun$flatMap$1.apply(TraversableLike.scala:241)
	at scala.collection.TraversableLike$$anonfun$flatMap$1.apply(TraversableLike.scala:241)
	at scala.collection.mutable.ResizableArray$class.foreach(ResizableArray.scala:59)
	at scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:48)
	at scala.collection.TraversableLike$class.flatMap(TraversableLike.scala:241)
	at scala.collection.AbstractTraversable.flatMap(Traversable.scala:104)
	at at.logic.gapt.proofs.Sequent.flatMap(sequents.scala:233)
	at at.logic.gapt.proofs.Sequent.flatMap(sequents.scala:217)
	at at.logic.gapt.proofs.reduction.ErasureReductionHelper.back(manySorted.scala:224)
	at at.logic.gapt.proofs.reduction.ErasureReductionET$$anonfun$forward$8.apply(manySorted.scala:270)
	at at.logic.gapt.proofs.reduction.ErasureReductionET$$anonfun$forward$8.apply(manySorted.scala:270)
	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:24)
	at at.logic.gapt.provers.viper.Example.main(Bug.scala)

[gebner]

Ah, looks like erasure reduction does not handle Skolemization. As a quick fix you could start with CNFReductionExpRes instead, then the further reductions will not see the strong quantifiers.