package statistics
- Alphabetic
- By Inheritance
- statistics
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Type Members
- case class CASCResult(path: String, prover: Prover, problem: String, extension: String) extends FileData with Serializable with Product
A filename that comes from the CASC competition: the prover and TSTP problem name are accessible.
A filename that comes from the CASC competition: the prover and TSTP problem name are accessible. The filename is automatically set to $path/$prover-$problem$extension
- path
The problem path
- prover
The prover produceing the tstp file
- problem
The TSTP library problem (see http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP?TPTPProblem=$problem )
- extension
The file extension
- type ClauseId = String
- abstract class CommonProofStats[T <: FileData] extends Serializable with CSVConvertible[String]
Statistical data for a gapt.proofs.resolution.ResolutionProof proof rp
Statistical data for a gapt.proofs.resolution.ResolutionProof proof rp
- T
a subtype of FileData that represents the location and metadata of a TSTP file
- Annotations
- @SerialVersionUID()
- case class ErrorBags[T <: FileData](nf: Iterable[FileNotFound[T]], mf: Iterable[MalformedFile[T]], pe: Iterable[ParsingError[T]], rg: Iterable[ReconstructionGaveUp[T]], rt: Iterable[ReconstructionTimeout[T]], re: Iterable[ReconstructionError[T]], so: Iterable[StackOverflow[T]]) extends Serializable with Product
Divides a list of TstpError into its sublasses
- abstract class FileData extends InputFile with Serializable with CSVConvertible[String]
Easier representation of file paths data follow a certain schema
- case class FileNotFound[+T <: FileData](file: T) extends TstpError[T] with Product with Serializable
Signifies that the file file.fileName does not exists
Signifies that the file file.fileName does not exists
- T
an instance of FileData
- file
The file with the TSTP proof that was replayed
- Annotations
- @SerialVersionUID()
- case class MalformedFile[+T <: FileData](file: T) extends TstpError[T] with Product with Serializable
Signifies an error in the TSTP DAG
Signifies an error in the TSTP DAG
- T
an instance of FileData
- file
The file with the TSTP proof that was replayed
- Annotations
- @SerialVersionUID()
- case class ParsingError[+T <: FileData](file: T) extends TstpError[T] with Product with Serializable
Signifies other exception that were thrown during sketch construction (e.g.
Signifies other exception that were thrown during sketch construction (e.g. the file is syntactically incorrect)
- T
an instance of FileData
- file
The file with the TSTP proof that was replayed
- Annotations
- @SerialVersionUID()
- type Problem = String
- type Prover = String
- case class RPProofStats[T <: FileData](name: T, dagSize: BigInt, treeSize: BigInt, depth: Int, rule_histogram: Map[RuleName, Int], clause_frequency: Map[ClauseId, Int], reused_axioms: Map[RuleName, (String, Int)], reused_derived: Map[RuleName, (String, Int)], clause_sizes: Statistic[Int], clause_weights: Statistic[Int], subst_term_sizes: Option[Statistic[Int]], subst_term_depths: Option[Statistic[Int]]) extends CommonProofStats[T] with Serializable with Product
Statistical data for a gapt.proofs.resolution.ResolutionProof proof rp
Statistical data for a gapt.proofs.resolution.ResolutionProof proof rp
- T
a subtype of FileData that represents the location and metadata of a TSTP file
- name
the name of the problem
- dagSize
the same as rp.dagSize
- treeSize
the same as rp.treeSize
- depth
the same as sketch.depth
- rule_histogram
map from a rule's name to how often the rule appears in the proof
- clause_frequency
a map from the clause id to how often the clause appears
- reused_axioms
the frequency of all leaf nodes that are used at least once
- reused_derived
the frequency of all inner nodes that are used at least once
- clause_sizes
statistics over the length of clauses in the proof
- subst_term_sizes
statistics about the term sizes occurring in gapt.proofs.resolution.Subst rules
- subst_term_depths
statistics about the term depths occurring in gapt.proofs.resolution.Subst rules
- Annotations
- @SerialVersionUID()
- case class ReconstructionError[+T <: FileData](file: T) extends TstpError[T] with Product with Serializable
Siginifies an exception during proof replay, e.g.
Siginifies an exception during proof replay, e.g. attempting to apply a split where variables in the split clauses are not disjoint
- T
an instance of FileData
- file
The file with the TSTP proof that was replayed
- Annotations
- @SerialVersionUID()
- case class ReconstructionGaveUp[+T <: FileData](file: T) extends TstpError[T] with Product with Serializable
Signifies a termination of
RefutationSketchToResolution.apply()that could not replay a step.Signifies a termination of
RefutationSketchToResolution.apply()that could not replay a step.- T
an instance of FileData
- file
The file with the TSTP proof that was replayed
- Annotations
- @SerialVersionUID()
- case class ReconstructionTimeout[+T <: FileData](file: T) extends TstpError[T] with Product with Serializable
Signifies a timeout from gapt.utils.withTimeout during reconstruction.
Signifies a timeout from gapt.utils.withTimeout during reconstruction.
- T
an instance of FileData
- file
The file with the TSTP proof that was replayed
- Annotations
- @SerialVersionUID()
- case class ResultBundle[T <: FileData](tstp_stats: Map[T, TstpProofStats[T]], rp_stats: Map[T, RPProofStats[T]], tstp_errors: List[TstpError[T]], rp_errors: List[TstpError[T]]) extends Serializable with Product
Collects errors and statistics from proof sketch and resolution proof reconstruction
Collects errors and statistics from proof sketch and resolution proof reconstruction
- T
the type of input files
- tstp_stats
the proof sketch statistics
- rp_stats
the resolution proof statistics
- tstp_errors
the proof sketch errors that occurred
- rp_errors
the replay errors that occurred
- Annotations
- @SerialVersionUID()
- type RuleName = String
- case class StackOverflow[+T <: FileData](file: T) extends TstpError[T] with Product with Serializable
Signifies a stack overflow
Signifies a stack overflow
- T
an instance of FileData
- file
The file with the TSTP proof that was replayed
- Annotations
- @SerialVersionUID()
- case class TptpInputStats[T <: FileData](name: T, axiom_count: Int, input_formula_count: Int, signature_size: Int, constants: Int, unary_funs: Int, binary_funs: Int, contains_equality: Boolean, arity_statistics: Option[Statistic[Int]]) extends CSVConvertible[String] with Product with Serializable
Captures data from a TPTP problem file
Captures data from a TPTP problem file
- name
the file the data comes from
- axiom_count
the number of axioms in the problem (including included files)
- input_formula_count
the number statements asserting an imput formula
- signature_size
the total number of different constants and function symbols
- constants
the number of constants in the problem
- unary_funs
the number of unary functions in the problem
- binary_funs
the number of binary functions in the problem
- arity_statistics
statistical data about the arities of function symbols (may be empty e.g. for ∀xEy.x=y)
- Annotations
- @SerialVersionUID()
- case class TptpLibraryProblem(path: String, problem: Problem) extends FileData with Serializable with Product
Represents a TPTP library problem of a certain category.
Represents a TPTP library problem of a certain category. The problem must be in $path/Problems/XYZ/ - $path/Axioms must contain the axiom files to include.
- path
the path to the TPTP base directory
- problem
a TPTP library problem
- Annotations
- @SerialVersionUID()
- sealed abstract class TstpError[+T <: FileData] extends Serializable
Describes various errors that may occur during proof replay
Describes various errors that may occur during proof replay
- T
an instance of FileData
- Annotations
- @SerialVersionUID()
- case class TstpProofStats[T <: FileData](name: T, dagSize: BigInt, treeSize: BigInt, depth: Int, rule_histogram: Map[RuleName, Int], clause_frequency: Map[ClauseId, Int], reused_axioms: Map[RuleName, (String, Int)], reused_derived: Map[RuleName, (String, Int)], clause_sizes: Statistic[Int], clause_weights: Statistic[Int]) extends CommonProofStats[T] with Serializable with Product
Statistical data for a gapt.proofs.sketch.RefutationSketch sketch
Statistical data for a gapt.proofs.sketch.RefutationSketch sketch
- T
a subtype of FileData that represents the location and metadata of a TSTP file
- name
the name of the problem
- dagSize
the same as sketch.dagSize
- treeSize
the same as sketch.treeSize
- depth
the same as sketch.depth
- rule_histogram
map from a rule's name to how often the rule appears in the proof
- clause_frequency
a map from the clause id to how often the clause appears
- reused_axioms
the frequency of all leaf nodes that are used at least once
- reused_derived
the frequency of all inner nodes that are used at least once
- clause_sizes
statistics over the length of clauses in the proof
- Annotations
- @SerialVersionUID()
Value Members
- object CASCResult extends Serializable
- object ErrorBags extends Serializable
Companion object to ErrorBags
- object RPProofStats extends Serializable
Companion object for RPProofStats
- object TPTPstatistics
- object TstpError extends Serializable
Companion object to TstpError.
- object TstpProofStats extends Serializable
Companion object for TstpProofStats
- object TstpStatistics
Calculates sketch statistics (TstpProofStats) and replay statistics (RPProofStats) from a list of FileData files as well as errors.
Calculates sketch statistics (TstpProofStats) and replay statistics (RPProofStats) from a list of FileData files as well as errors. Provides serialization to a file.
- case object UnknownFile extends FileData with Product with Serializable
This is the API documentation for GAPT.
The main package is gapt.