This PR adds some unit tests that cover getStatistics() and the api::Stat class.
Printing statistics on the command line looks like this:
-.. run-command:: bin/cvc5 --stats ../test/regress/regress0/auflia/bug336.smt2
+.. run-command:: bin/cvc5 --stats ../test/regress/cli/regress0/auflia/bug336.smt2
Public statistics include some general information about the input file
(``driver::filename`` and ``api::*``), the overall runtime (``global::totalTime``)
System.out.println("Long version:");
// long version
- for (Pair<String, Stat> pair : stats)
+ for (Map.Entry<String, Stat> pair : stats)
{
- Stat stat = pair.second;
+ Stat stat = pair.getValue();
if (stat.isInt())
{
- System.out.println(pair.first + " = " + stat.getInt());
+ System.out.println(pair.getKey() + " = " + stat.getInt());
}
else if (stat.isDouble())
{
- System.out.println(pair.first + " = " + stat.getDouble());
+ System.out.println(pair.getKey() + " = " + stat.getDouble());
}
else if (stat.isString())
{
- System.out.println(pair.first + " = " + stat.getString());
+ System.out.println(pair.getKey() + " = " + stat.getString());
}
else if (stat.isHistogram())
{
System.out.println("-------------------------------------------------------");
- System.out.println(pair.first + " : Map");
+ System.out.println(pair.getKey() + " : Map");
for (Map.Entry<String, Long> entry : stat.getHistogram().entrySet())
{
System.out.println(entry.getKey() + " = " + entry.getValue());
import java.util.Iterator;
import java.util.NoSuchElementException;
+import java.util.Map;
+import java.util.AbstractMap;
-public class Statistics extends AbstractPointer implements Iterable<Pair<String, Stat>>
+public class Statistics extends AbstractPointer implements Iterable<Map.Entry<String, Stat>>
{
// region construction and destruction
Statistics(Solver solver, long pointer)
* @param defaulted If set to true, defaulted statistics are shown as well.
*/
+ private native long getIteratorOpts(long pointer, boolean internal, boolean defaulted);
private native long getIterator(long pointer);
private native boolean hasNext(long pointer, long iteratorPointer);
private native void deleteIteratorPointer(long iteratorPointer);
- public class ConstIterator implements Iterator<Pair<String, Stat>>
+ public class ConstIterator implements Iterator<Map.Entry<String, Stat>>
{
private long iteratorPointer = 0;
+ public ConstIterator(boolean internal, boolean defaulted)
+ {
+ iteratorPointer = getIteratorOpts(pointer, internal, defaulted);
+ }
public ConstIterator()
{
iteratorPointer = getIterator(pointer);
return Statistics.this.hasNext(pointer, iteratorPointer);
}
- @Override public Pair<String, Stat> next()
+ @Override public Map.Entry<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);
+ return new AbstractMap.SimpleImmutableEntry(pair.first, stat);
}
catch (CVC5ApiException e)
{
}
}
- @Override public Iterator<Pair<String, Stat>> iterator()
+ public ConstIterator iterator(boolean internal, boolean defaulted)
+ {
+ return new ConstIterator(internal, defaulted);
+ }
+ @Override public ConstIterator iterator()
{
return new ConstIterator();
}
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
+/*
+ * Class: io_github_cvc5_api_Statistics
+ * Method: getIterator
+ * Signature: (JZZ)J
+ */
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Statistics_getIteratorOpts(
+ JNIEnv* env, jobject, jlong pointer, jboolean internal, jboolean defaulted)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Statistics* current = reinterpret_cast<Statistics*>(pointer);
+ Statistics::iterator* it =
+ new Statistics::iterator(current->begin(internal, defaulted));
+ return reinterpret_cast<jlong>(it);
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
/*
* Class: io_github_cvc5_api_Statistics
* Method: getIterator
CVC5_JAVA_API_TRY_CATCH_BEGIN;
Statistics* current = reinterpret_cast<Statistics*>(pointer);
Statistics::iterator* it =
- new Statistics::iterator(current->begin(true, true));
+ new Statistics::iterator(current->begin());
return reinterpret_cast<jlong>(it);
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
res.append(info['description'])
if 'example-file' in info:
res.append('')
- res.append('.. command-output:: bin/cvc5 -o {} ../test/regress/{}'.format(info['name'], info['example-file']))
+ res.append('.. command-output:: bin/cvc5 -o {} ../test/regress/cli/{}'.format(info['name'], info['example-file']))
res.append(' :cwd: {}'.format(cwd))
res.append('')
res.append('')
*/
#include <algorithm>
+#include <cmath>
#include "base/output.h"
#include "test_api.h"
}
}
+TEST_F(TestApiBlackSolver, getStatistics)
+{
+ // do some array reasoning to make sure we have a double statistics
+ {
+ Sort s1 = d_solver.getIntegerSort();
+ Sort s2 = d_solver.mkArraySort(s1, s1);
+ Term t1 = d_solver.mkConst(s1, "i");
+ Term t2 = d_solver.mkVar(s2, "a");
+ Term t3 = d_solver.mkTerm(Kind::SELECT, {t2, t1});
+ d_solver.checkSat();
+ }
+ cvc5::api::Statistics stats = d_solver.getStatistics();
+ {
+ std::stringstream ss;
+ ss << stats;
+ }
+ {
+ auto s = stats.get("global::totalTime");
+ EXPECT_FALSE(s.isInternal());
+ EXPECT_FALSE(s.isDefault());
+ EXPECT_TRUE(s.isString());
+ std::string time = s.getString();
+ EXPECT_TRUE(time.rfind("ms") == time.size() - 2); // ends with "ms"
+ EXPECT_FALSE(s.isDouble());
+ s = stats.get("resource::resourceUnitsUsed");
+ EXPECT_TRUE(s.isInternal());
+ EXPECT_FALSE(s.isDefault());
+ EXPECT_TRUE(s.isInt());
+ EXPECT_TRUE(s.getInt() >= 0);
+ }
+ for (const auto& s: stats)
+ {
+ EXPECT_FALSE(s.first.empty());
+ }
+ for (auto it = stats.begin(true, true); it != stats.end(); ++it)
+ {
+ {
+ auto tmp1 = it, tmp2 = it;
+ ++tmp1;
+ tmp2++;
+ EXPECT_EQ(tmp1, tmp2);
+ --tmp1;
+ tmp2--;
+ EXPECT_EQ(tmp1, tmp2);
+ EXPECT_EQ(tmp1, it);
+ EXPECT_EQ(it, tmp2);
+ }
+ const auto& s = *it;
+ // check some basic utility methods
+ EXPECT_TRUE(!(it == stats.end()));
+ EXPECT_EQ(s.first, it->first);
+ if (s.first == "api::CONSTANT")
+ {
+ EXPECT_FALSE(s.second.isInternal());
+ EXPECT_FALSE(s.second.isDefault());
+ EXPECT_TRUE(s.second.isHistogram());
+ auto hist = s.second.getHistogram();
+ EXPECT_FALSE(hist.empty());
+ std::stringstream ss;
+ ss << s.second;
+ EXPECT_EQ(ss.str(), "{ integer type: 1 }");
+ }
+ else if (s.first == "theory::arrays::avgIndexListLength")
+ {
+ EXPECT_TRUE(s.second.isInternal());
+ EXPECT_TRUE(s.second.isDouble());
+ EXPECT_TRUE(std::isnan(s.second.getDouble()));
+ }
+ }
+}
+
TEST_F(TestApiBlackSolver, getUnsatAssumptions1)
{
d_solver.setOption("incremental", "false");
assertAll(assertions);
}
+ @Test void getStatistics()
+ {
+ // do some array reasoning to make sure we have a double statistics
+ {
+ Sort s1 = d_solver.getIntegerSort();
+ Sort s2 = d_solver.mkArraySort(s1, s1);
+ Term t1 = d_solver.mkConst(s1, "i");
+ Term t2 = d_solver.mkVar(s2, "a");
+ Term t3 = d_solver.mkTerm(Kind.SELECT, t2, t1);
+ d_solver.checkSat();
+ }
+ Statistics stats = d_solver.getStatistics();
+ stats.toString();
+ {
+ Stat s = stats.get("global::totalTime");
+ assertFalse(s.isInternal());
+ assertFalse(s.isDefault());
+ assertTrue(s.isString());
+ assertTrue(s.getString().endsWith("ms"));
+ s = stats.get("resource::resourceUnitsUsed");
+ assertTrue(s.isInternal());
+ assertFalse(s.isDefault());
+ assertTrue(s.isInt());
+ assertTrue(s.getInt() >= 0);
+ }
+ for (Map.Entry<String, Stat> s : stats) {}
+ for (Statistics.ConstIterator it = stats.iterator(true, true); it.hasNext();)
+ {
+ Map.Entry<String, Stat> elem = it.next();
+ if (elem.getKey() == "api::CONSTANT")
+ {
+ assertFalse(elem.getValue().isInternal());
+ assertFalse(elem.getValue().isDefault());
+ assertTrue(elem.getValue().isHistogram());
+ Map<String, Long> hist = elem.getValue().getHistogram();
+ assertFalse(hist.isEmpty());
+ assertEquals(elem.getValue().toString(), "{ integer type: 1 }");
+ }
+ else if (elem.getKey() == "theory::arrays::avgIndexListLength")
+ {
+ assertTrue(elem.getValue().isInternal());
+ assertTrue(elem.getValue().isDefault());
+ }
+ }
+ }
+
@Test void getUnsatAssumptions1()
{
d_solver.setOption("incremental", "false");
projects / cvc5.git / commitdiff