Package io.github.cvc5
Class Statistics
- java.lang.Object
 - 
- io.github.cvc5.Statistics
 
 
- 
- 
Nested Class Summary
Nested Classes Modifier and Type Class Description classStatistics.ConstIterator 
- 
Field Summary
Fields Modifier and Type Field Description protected longpointer 
- 
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description voiddeletePointer()protected voiddeletePointer(long pointer)Statget(java.lang.String name)Retrieve the statistic with the given name.longgetPointer()Statistics.ConstIteratoriterator()Statistics.ConstIteratoriterator(boolean internal, boolean defaulted)java.lang.StringtoString()protected java.lang.StringtoString(long pointer) 
 - 
 
- 
- 
Method Detail
- 
deletePointer
protected void deletePointer(long pointer)
 
- 
getPointer
public long getPointer()
 
- 
toString
protected java.lang.String toString(long pointer)
- Returns:
 - A string representation of this Statistics.
 
 
- 
get
public Stat get(java.lang.String name)
Retrieve the statistic with the given name. Asserts that a statistic with the given name actually exists and throws aCVC5ApiRecoverableExceptionif it does not.- Parameters:
 name- Name of the statistic.- Returns:
 - The statistic with the given name.
 
 
- 
iterator
public Statistics.ConstIterator iterator(boolean internal, boolean defaulted)
 
- 
iterator
public Statistics.ConstIterator iterator()
- Specified by:
 iteratorin interfacejava.lang.Iterable<java.util.Map.Entry<java.lang.String,Stat>>
 
- 
deletePointer
public void deletePointer()
 
- 
toString
public java.lang.String toString()
- Overrides:
 toStringin classjava.lang.Object
 
 - 
 
 -