public final class SideProofStatistics extends Statistics
Modifier and Type | Field and Description |
---|---|
private int |
sideProofs
Keep track of the amount of side proofs (can also be nested)
|
autoModeTimeInMillis, blockLoopContractApps, branches, dependencyContractApps, interactiveSteps, loopInvApps, mergeRuleApps, nodes, operationContractApps, ossApps, quantifierInstantiations, smtSolverApps, symbExApps, timeInMillis, timePerStepInMillis, totalRuleApps
Modifier | Constructor and Description |
---|---|
private |
SideProofStatistics(int sideProofs,
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 autoModeTime)
Construct new side proof statistics
|
Modifier and Type | Method and Description |
---|---|
(package private) SideProofStatistics |
add(SideProofStatistics stat)
Add side proof statistics to current one.
|
SideProofStatistics |
add(Statistics stat)
Add proof statistics to current side proof statistics object.
|
(package private) static SideProofStatistics |
create(SideProofStatistics stat)
Create a new side proof statistics object from existing side proof statistics.
|
(package private) static SideProofStatistics |
create(Statistics stat)
Create a new side proof statistics object from existing proof statistics.
|
SideProofStatistics |
setAutoModeTime(long autoTime)
Set time spent in auto mode.
|
getInteractiveAppsDetails, getSummary, toString
private final int sideProofs
private SideProofStatistics(int sideProofs, 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 autoModeTime)
sideProofs
- the amount of side proofsnodes
- amount of nodesbranches
- amount of branchesinteractiveSteps
- amount of interactive stepssymbExApps
- amount of symbolic execution stepsquantifierInstantiations
- amount of quantifier instantiationsossApps
- amount of one-step-simplifier applicationsmergeRuleApps
- amount of merge rule applicationstotalRuleApps
- amount of total rule applicationssmtSolverApps
- amount of SMT solver callsdependencyContractApps
- amount of dependency contract applicationsoperationContractApps
- amount of operation contract applicationsblockLoopContractApps
- amount of block or loop contract applicationsloopInvApps
- amount of loop invariant rule applicationsautoModeTime
- accumulated (spent) auto mode timestatic SideProofStatistics create(SideProofStatistics stat)
stat
- side proof statistics object.static SideProofStatistics create(Statistics stat)
stat
- proof statistics object.SideProofStatistics add(SideProofStatistics stat)
stat
- another side proof statistics object.public SideProofStatistics add(Statistics stat)
stat
- a proof statistics object.public SideProofStatistics setAutoModeTime(long autoTime)
autoTime
- auto mode time as long data type.