1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
|
/******************************************************************************
* Top contributors (to current version):
* Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* The cvc5 java API.
*/
package cvc5;
import java.util.Iterator;
import java.util.NoSuchElementException;
public class Statistics extends AbstractPointer implements Iterable<Pair<String, Stat>>
{
// region construction and destruction
Statistics(Solver solver, long pointer)
{
super(solver, pointer);
}
protected static native void deletePointer(long pointer);
public long getPointer()
{
return pointer;
}
@Override
public void finalize()
{
deletePointer(pointer);
}
// endregion
/**
* @return a string representation of this Statistics
*/
protected native String toString(long pointer);
/**
* 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.
* @param name Name of the statistic.
* @return The statistic with the given name.
*/
public Stat get(String name)
{
long statPointer = get(pointer, name);
return new Stat(solver, statPointer);
}
private native long get(long pointer, String name);
/**
* Begin iteration over the statistics values.
* By default, only entries that are public (non-expert) and have been set
* are visible while the others are skipped.
* @param expert If set to true, expert statistics are shown as well.
* @param defaulted If set to true, defaulted statistics are shown as well.
*/
private native long getIterator(long pointer);
private native boolean hasNext(long pointer, long iteratorPointer);
private native Pair<String, Long> getNext(long pointer, long iteratorPointer) throws CVC5ApiException;
private native long increment(long pointer, long iteratorPointer) throws CVC5ApiException;
private native void deleteIteratorPointer(long iteratorPointer);
public class ConstIterator implements Iterator<Pair<String, Stat>>
{
private long iteratorPointer = 0;
public ConstIterator()
{
iteratorPointer = getIterator(pointer);
}
@Override
public boolean hasNext()
{
return Statistics.this.hasNext(pointer, iteratorPointer);
}
@Override
public Pair<String, Stat> next()
{
try
{
Pair<String, Long> pair = Statistics.this.getNext(pointer, iteratorPointer);
Stat stat = new Stat(solver, pair.second);
this.iteratorPointer = Statistics.this.increment(pointer, iteratorPointer);
return new Pair<>(pair.first, stat);
}
catch(CVC5ApiException e)
{
throw new NoSuchElementException(e.getMessage());
}
}
@Override
public void finalize()
{
deleteIteratorPointer(iteratorPointer);
}
}
@Override
public Iterator<Pair<String, Stat>> iterator()
{
return new ConstIterator();
}
};
|
