io.github.cvc5

Class Statistics

java.lang.Object

io.github.cvc5.Statistics

All Implemented Interfaces:

java.lang.Iterable<java.util.Map.Entry<java.lang.String,Stat>>

public class Statistics
extends java.lang.Object
implements java.lang.Iterable<java.util.Map.Entry<java.lang.String,Stat>>

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
class	Statistics.ConstIterator

Field Summary

Fields

Modifier and Type	Field and Description
protected long	pointer

Method Summary

Modifier and Type	Method and 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)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface java.lang.Iterable

forEach, spliterator

Field Detail

pointer

protected long pointer

Method Detail

deletePointer

protected void deletePointer(long pointer)

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 a CVC5ApiRecoverableException 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 interface java.lang.Iterable<java.util.Map.Entry<java.lang.String,Stat>>

getPointer

public long getPointer()

deletePointer

public void deletePointer()

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object