CASCEvaluation

gapt.examples.CASCEvaluation

Attributes

Graph
Supertypes
class Object
trait Matchable
class Any
Self type

Members list

Value members

Concrete methods

def apply(prefix: String, print_statistics: Boolean): CSVFile[String]
def dagRatio[T <: CASCResult](pair: (TstpProofStats[T], RPProofStats[T])): BigDecimal
def depthRatio[T <: CASCResult](pair: (TstpProofStats[T], RPProofStats[T])): BigDecimal
def eval[T <: CASCResult](bundle: ResultBundle[T]): CSVFile[String]
def eval_before_after[T <: CASCResult](before_replayed: Seq[(TstpProofStats[T], RPProofStats[T])], ratio: ((TstpProofStats[T], RPProofStats[T])) => BigDecimal, description: String, tex: Boolean): (Seq[(TstpProofStats[T], RPProofStats[T])], Seq[(TstpProofStats[T], RPProofStats[T])], Seq[(TstpProofStats[T], RPProofStats[T])])
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): Unit
def eval_rp_stats[T <: FileData](rp_stats: Set[RPProofStats[T]]): (CSVFile[String], Statistic[Int], Statistic[BigInt], Statistic[BigDecimal], Statistic[Int], Statistic[Int])
def getProblemStats(prefix: String): List[Either[ReconstructionTimeout[TptpLibraryProblem] | StackOverflow[TptpLibraryProblem], TptpInputStats[TptpLibraryProblem]]]
def getRPstatByProperty[S, T <: FileData](rp_stats: Set[RPProofStats[T]], prop: RPProofStats[T] => S)(implicit num: Numeric[S], conv: S => BigDecimal): Statistic[S]
def getStatisticSummary[T](s: Seq[Statistic[T]])(implicit num: Numeric[T], conv: T => BigDecimal): Statistic[T]
def get_dagsize_to_minddagsize_graph[T <: CASCResult](bundle: ResultBundle[T]): (List[(BigInt, BigInt, Int, Int)], CSVFile[String])
def get_depth_to_mindepth_graph[T <: CASCResult](bundle: ResultBundle[T]): (List[(Int, Int, Int, Int)], CSVFile[String])
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])
def loadResult[T](filename: String): Option[T]
def processFiles[T <: FileData](data: Iterable[T], print_statistics: Boolean): ResultBundle[T]
def processLeanCop[T <: FileData](data: Iterable[T], print_statistics: Boolean): ParIterable[Either[ReconstructionTimeout[T] | StackOverflow[T] | ParsingError[T] | FileNotFound[T], Option[ExpansionSequent]]]
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

Type parameters

T

the type of data points in the statistic

Value parameters

conv

implicit converter from statistic data to big decimals

num

implicit numeric object for statistic data

s

the statistic

Attributes

Returns

a CSVRow with the trincated strings

def saveResult[T](filename: String, bundle: T): Unit