public class Statistics
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
private class |
Statistics.TemporaryStatistics
Helper class to add up all rule applications for some nodes
|
Modifier and Type | Field and Description |
---|---|
long |
autoModeTimeInMillis |
int |
blockLoopContractApps |
int |
branches |
int |
dependencyContractApps |
private java.util.HashMap<java.lang.String,java.lang.Integer> |
interactiveAppsDetails |
int |
interactiveSteps |
int |
loopInvApps |
int |
mergeRuleApps |
int |
nodes |
int |
operationContractApps |
int |
ossApps |
int |
quantifierInstantiations |
int |
smtSolverApps |
private java.util.List<Pair<java.lang.String,java.lang.String>> |
summaryList |
int |
symbExApps |
long |
timeInMillis |
float |
timePerStepInMillis |
int |
totalRuleApps |
Modifier | Constructor and Description |
---|---|
protected |
Statistics(int nodes,
int branches,
int interactiveSteps,
int symbExApps,
int quantifierInstantiations,
int ossApps,
int mergeRuleApps,
int totalRuleApps,
int smtSolverApps,
int dependencyContractApps,
int operationContractApps,
int blockLoopContractApps,
int loopInvApps,
long autoModeTimeInMillis,
long timeInMillis,
float timePerStepInMillis) |
(package private) |
Statistics(Node startNode) |
(package private) |
Statistics(Proof proof) |
Modifier and Type | Method and Description |
---|---|
(package private) static Statistics |
create(Statistics side,
long creationTime) |
private void |
generateSummary(Proof proof) |
java.util.HashMap<java.lang.String,java.lang.Integer> |
getInteractiveAppsDetails() |
java.util.List<Pair<java.lang.String,java.lang.String>> |
getSummary() |
java.lang.String |
toString() |
public final int nodes
public final int branches
public final int interactiveSteps
public final int symbExApps
public final int quantifierInstantiations
public final int ossApps
public final int mergeRuleApps
public final int totalRuleApps
public final int smtSolverApps
public final int dependencyContractApps
public final int operationContractApps
public final int blockLoopContractApps
public final int loopInvApps
public final long autoModeTimeInMillis
public final long timeInMillis
public final float timePerStepInMillis
private java.util.List<Pair<java.lang.String,java.lang.String>> summaryList
private final java.util.HashMap<java.lang.String,java.lang.Integer> interactiveAppsDetails
protected Statistics(int nodes, int branches, int interactiveSteps, int symbExApps, int quantifierInstantiations, int ossApps, int mergeRuleApps, int totalRuleApps, int smtSolverApps, int dependencyContractApps, int operationContractApps, int blockLoopContractApps, int loopInvApps, long autoModeTimeInMillis, long timeInMillis, float timePerStepInMillis)
Statistics(Node startNode)
Statistics(Proof proof)
static Statistics create(Statistics side, long creationTime)
private void generateSummary(Proof proof)
public java.util.List<Pair<java.lang.String,java.lang.String>> getSummary()
public java.util.HashMap<java.lang.String,java.lang.Integer> getInteractiveAppsDetails()
public java.lang.String toString()
toString
in class java.lang.Object