From 81eb37c14982676242779547349984931e99f110 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 23 Mar 2022 23:59:23 +0100 Subject: [PATCH] Add API unit tests for statistics (#8341) This PR adds some unit tests that cover getStatistics() and the api::Stat class. --- docs/statistics.rst | 2 +- examples/api/java/Statistics.java | 12 ++-- .../java/io/github/cvc5/api/Statistics.java | 21 ++++-- src/api/java/jni/statistics.cpp | 18 ++++- src/options/mkoptions.py | 2 +- test/unit/api/cpp/solver_black.cpp | 72 +++++++++++++++++++ test/unit/api/java/SolverTest.java | 46 ++++++++++++ 7 files changed, 159 insertions(+), 14 deletions(-) diff --git a/docs/statistics.rst b/docs/statistics.rst index ea4410df4..263104978 100644 --- a/docs/statistics.rst +++ b/docs/statistics.rst @@ -41,7 +41,7 @@ A statistic value can be any of the following types: 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``) diff --git a/examples/api/java/Statistics.java b/examples/api/java/Statistics.java index 635be65f6..a09127fe8 100644 --- a/examples/api/java/Statistics.java +++ b/examples/api/java/Statistics.java @@ -37,25 +37,25 @@ public class Statistics System.out.println("Long version:"); // long version - for (Pair pair : stats) + for (Map.Entry 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 entry : stat.getHistogram().entrySet()) { System.out.println(entry.getKey() + " = " + entry.getValue()); diff --git a/src/api/java/io/github/cvc5/api/Statistics.java b/src/api/java/io/github/cvc5/api/Statistics.java index 0c64370c0..df7a82c58 100644 --- a/src/api/java/io/github/cvc5/api/Statistics.java +++ b/src/api/java/io/github/cvc5/api/Statistics.java @@ -17,8 +17,10 @@ package io.github.cvc5.api; import java.util.Iterator; import java.util.NoSuchElementException; +import java.util.Map; +import java.util.AbstractMap; -public class Statistics extends AbstractPointer implements Iterable> +public class Statistics extends AbstractPointer implements Iterable> { // region construction and destruction Statistics(Solver solver, long pointer) @@ -63,6 +65,7 @@ public class Statistics extends AbstractPointer implements Iterable> + public class ConstIterator implements Iterator> { private long iteratorPointer = 0; + public ConstIterator(boolean internal, boolean defaulted) + { + iteratorPointer = getIteratorOpts(pointer, internal, defaulted); + } public ConstIterator() { iteratorPointer = getIterator(pointer); @@ -88,14 +95,14 @@ public class Statistics extends AbstractPointer implements Iterable next() + @Override public Map.Entry next() { try { Pair 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) { @@ -109,7 +116,11 @@ public class Statistics extends AbstractPointer implements Iterable> iterator() + public ConstIterator iterator(boolean internal, boolean defaulted) + { + return new ConstIterator(internal, defaulted); + } + @Override public ConstIterator iterator() { return new ConstIterator(); } diff --git a/src/api/java/jni/statistics.cpp b/src/api/java/jni/statistics.cpp index dfea8bf9d..f76fd8e46 100644 --- a/src/api/java/jni/statistics.cpp +++ b/src/api/java/jni/statistics.cpp @@ -69,6 +69,22 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Statistics_get(JNIEnv* env, 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(pointer); + Statistics::iterator* it = + new Statistics::iterator(current->begin(internal, defaulted)); + return reinterpret_cast(it); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + /* * Class: io_github_cvc5_api_Statistics * Method: getIterator @@ -80,7 +96,7 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Statistics_getIterator( CVC5_JAVA_API_TRY_CATCH_BEGIN; Statistics* current = reinterpret_cast(pointer); Statistics::iterator* it = - new Statistics::iterator(current->begin(true, true)); + new Statistics::iterator(current->begin()); return reinterpret_cast(it); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index de76dbe52..03e190d96 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -818,7 +818,7 @@ def generate_sphinx_output_tags(modules, src_dir, build_dir): 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('') diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 7c28fde12..7e6c113eb 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -14,6 +14,7 @@ */ #include +#include #include "base/output.h" #include "test_api.h" @@ -1580,6 +1581,77 @@ TEST_F(TestApiBlackSolver, getOptionInfo) } } +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"); diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index ba93ed102..cc94600f5 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -1552,6 +1552,52 @@ class SolverTest 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 s : stats) {} + for (Statistics.ConstIterator it = stats.iterator(true, true); it.hasNext();) + { + Map.Entry elem = it.next(); + if (elem.getKey() == "api::CONSTANT") + { + assertFalse(elem.getValue().isInternal()); + assertFalse(elem.getValue().isDefault()); + assertTrue(elem.getValue().isHistogram()); + Map 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"); -- 2.30.2