Package io.github.cvc5
Class Statistics
- java.lang.Object
-
- io.github.cvc5.Statistics
-
-
Nested Class Summary
Nested Classes Modifier and Type Class Description class
Statistics.ConstIterator
-
Field Summary
Fields Modifier and Type Field Description protected long
pointer
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description void
deletePointer()
protected void
deletePointer(long pointer)
Stat
get(java.lang.String name)
Retrieve the statistic with the given name.long
getPointer()
Statistics.ConstIterator
iterator()
Statistics.ConstIterator
iterator(boolean internal, boolean defaulted)
java.lang.String
toString()
protected java.lang.String
toString(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 aCVC5ApiRecoverableException
if 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:
iterator
in interfacejava.lang.Iterable<java.util.Map.Entry<java.lang.String,Stat>>
-
deletePointer
public void deletePointer()
-
toString
public java.lang.String toString()
- Overrides:
toString
in classjava.lang.Object
-
-