Packages

o

gapt.examples

CASCEvaluation

object CASCEvaluation

Source
CASCEvaluation.scala
Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. CASCEvaluation
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##: Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. def apply(prefix: String, print_statistics: Boolean = false): CSVFile[String]
  5. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  6. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @native() @IntrinsicCandidate()
  7. def dagRatio[T <: CASCResult](pair: (TstpProofStats[T], RPProofStats[T])): BigDecimal
  8. def depthRatio[T <: CASCResult](pair: (TstpProofStats[T], RPProofStats[T])): BigDecimal
  9. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  10. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  11. def eval[T <: CASCResult](bundle: ResultBundle[T]): CSVFile[String]
  12. def eval_before_after[T <: CASCResult](before_replayed: Seq[(TstpProofStats[T], RPProofStats[T])], ratio: ((TstpProofStats[T], RPProofStats[T])) => BigDecimal, description: String = "", tex: Boolean = true): (Seq[(TstpProofStats[T], RPProofStats[T])], Seq[(TstpProofStats[T], RPProofStats[T])], Seq[(TstpProofStats[T], RPProofStats[T])])
  13. def eval_errors[T <: FileData](p: String, problems: Int, sstats: Set[TstpProofStats[T]], rpstats: Set[RPProofStats[T]], tstp_e_bags: ErrorBags[T], rp_e_bags: ErrorBags[T], tex: Boolean = false): Unit
  14. def eval_rp_stats[T <: FileData](rp_stats: Set[RPProofStats[T]]): (CSVFile[String], Statistic[Int], Statistic[BigInt], Statistic[BigDecimal], Statistic[Int], Statistic[Int])
  15. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @IntrinsicCandidate()
  16. def getProblemStats(prefix: String): List[Either[TstpError[TptpLibraryProblem] with Product, TptpInputStats[TptpLibraryProblem]]]
  17. def getRPstatByProperty[S, T <: FileData](rp_stats: Set[RPProofStats[T]], prop: (RPProofStats[T]) => S)(implicit num: Numeric[S], conv: (S) => BigDecimal): Statistic[S]
  18. def getStatisticSummary[T](s: Seq[Statistic[T]])(implicit num: Numeric[T], conv: (T) => BigDecimal): Statistic[T]
  19. def get_dagsize_to_minddagsize_graph[T <: CASCResult](bundle: ResultBundle[T]): (List[(BigInt, BigInt, Int, Int)], CSVFile[String])
  20. def get_depth_to_mindepth_graph[T <: CASCResult](bundle: ResultBundle[T]): (List[(Int, Int, Int, Int)], CSVFile[String])
  21. def get_prop_to_minprop_graph[T <: CASCResult, U](bundle: ResultBundle[T], prop: (RPProofStats[T]) => U)(implicit num: Numeric[U]): (List[(U, U, Int, Int)], CSVFile[String])
  22. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @IntrinsicCandidate()
  23. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  24. def loadResult[T](filename: String): Option[T]
  25. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  26. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @IntrinsicCandidate()
  27. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @IntrinsicCandidate()
  28. def processFiles[T <: FileData](data: Iterable[T], print_statistics: Boolean = false): ResultBundle[T]
  29. def processLeanCop[T <: FileData](data: Iterable[T], print_statistics: Boolean = false): ParIterable[Either[TstpError[T] with Product, Option[ExpansionSequent]]]
  30. def roundedStatisticCSV[T](s: Statistic[T])(implicit num: Numeric[T], conv: (T) => BigDecimal): CSVRow[String]

    toCSV with truncation after 2 digits

    toCSV with truncation after 2 digits

    T

    the type of data points in the statistic

    s

    the statistic

    num

    implicit numeric object for statistic data

    conv

    implicit converter from statistic data to big decimals

    returns

    a CSVRow with the trincated strings

  31. def saveResult[T](filename: String, bundle: T): Unit
  32. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  33. def toString(): String
    Definition Classes
    AnyRef → Any
  34. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  35. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  36. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated

Inherited from AnyRef

Inherited from Any

Ungrouped