This PR adds Solver.getStatistics() to the python API. To make the usage a bit more pythonic, we do not expose the iterator interface of api::Statistics but instead offer .get() which returns the whole range as a dictionary. The ::get() method to obtain a single statistic value is instead implemented via __getitem__().
The PR also includes the corresponding unit tests.
StatData() : data() {}
};
+Stat::Stat() {}
Stat::~Stat() {}
Stat::Stat(const Stat& s)
: d_internal(s.d_internal),
bool Stat::isInt() const
{
+ if (!d_data) return false;
return std::holds_alternative<int64_t>(d_data->data);
}
int64_t Stat::getInt() const
{
CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_RECOVERABLE_CHECK(static_cast<bool>(d_data)) << "Stat holds no value";
CVC5_API_RECOVERABLE_CHECK(isInt()) << "Expected Stat of type int64_t.";
return std::get<int64_t>(d_data->data);
CVC5_API_TRY_CATCH_END;
}
bool Stat::isDouble() const
{
+ if (!d_data) return false;
return std::holds_alternative<double>(d_data->data);
}
double Stat::getDouble() const
{
CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_RECOVERABLE_CHECK(static_cast<bool>(d_data)) << "Stat holds no value";
CVC5_API_RECOVERABLE_CHECK(isDouble()) << "Expected Stat of type double.";
return std::get<double>(d_data->data);
CVC5_API_TRY_CATCH_END;
}
bool Stat::isString() const
{
+ if (!d_data) return false;
return std::holds_alternative<std::string>(d_data->data);
}
const std::string& Stat::getString() const
{
CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_RECOVERABLE_CHECK(static_cast<bool>(d_data)) << "Stat holds no value";
CVC5_API_RECOVERABLE_CHECK(isString())
<< "Expected Stat of type std::string.";
return std::get<std::string>(d_data->data);
}
bool Stat::isHistogram() const
{
+ if (!d_data) return false;
return std::holds_alternative<HistogramData>(d_data->data);
}
const Stat::HistogramData& Stat::getHistogram() const
{
CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_RECOVERABLE_CHECK(static_cast<bool>(d_data)) << "Stat holds no value";
CVC5_API_RECOVERABLE_CHECK(isHistogram())
<< "Expected Stat of type histogram.";
return std::get<HistogramData>(d_data->data);
friend std::ostream& operator<<(std::ostream& os, const Stat& sv);
/** Representation of a histogram: maps names to frequencies. */
using HistogramData = std::map<std::string, uint64_t>;
- /** Can only be obtained from a `Statistics` object. */
- Stat() = delete;
+ /**
+ * Create an empty statistics object. On such an object all ``isX()`` return
+ * false and all ``getX()`` throw an API exception. It solely exists because
+ * it makes implementing bindings for other languages much easier.
+ */
+ Stat();
/** Copy constructor */
Stat(const Stat& s);
/** Destructor */
{
public:
friend class Statistics;
+ iterator() = default;
BaseType::const_reference operator*() const;
BaseType::const_pointer operator->() const;
iterator& operator++();
bool d_showDefault = false;
};
+ /** Creates an empty statistics object. */
+ Statistics() = default;
+
/**
* Retrieve the statistic with the given name.
* Asserts that a statistic with the given name actually exists and throws
iterator end() const;
private:
- Statistics() = default;
Statistics(const StatisticsRegistry& reg);
/** Internal data */
BaseType d_stats;
from cython.operator cimport dereference as deref, preincrement as inc
from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t
from libc.stddef cimport wchar_t
+from libcpp.map cimport map as c_map
from libcpp.set cimport set
from libcpp.string cimport string
from libcpp.vector cimport vector
void blockModel() except +
void blockModelValues(const vector[Term]& terms) except +
string getInstantiations() except +
+ Statistics getStatistics() except +
cdef cppclass Grammar:
Grammar() except +
SortHashFunction() except +
size_t operator()(const Sort & s) except +
+ cdef cppclass Stat:
+ bint isInternal() except +
+ bint isDefault() except +
+ bint isInt() except +
+ int64_t getInt() except +
+ bint isDouble() except +
+ double getDouble() except +
+ bint isString() except +
+ string getString() except +
+ bint isHistogram() except +
+ c_map[string,uint64_t] getHistogram() except +
+
+ cdef cppclass Statistics:
+ Statistics() except +
+ cppclass iterator:
+ iterator() except +
+ bint operator!=(const iterator& it) except +
+ iterator& operator++() except +
+ pair[string, Stat]& operator*() except +;
+ iterator begin(bint internal, bint defaulted) except +
+ iterator end() except +
+ Stat get(string name) except +
+
cdef cppclass Term:
Term()
bint operator==(const Term&) except +
from functools import wraps
import sys
+from cython.operator cimport dereference, preincrement
+
from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t
from libc.stddef cimport wchar_t
from cvc5 cimport UnknownExplanation as c_UnknownExplanation
from cvc5 cimport Op as c_Op
from cvc5 cimport Solver as c_Solver
+from cvc5 cimport Statistics as c_Statistics
+from cvc5 cimport Stat as c_Stat
from cvc5 cimport Grammar as c_Grammar
from cvc5 cimport Sort as c_Sort
from cvc5 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE
"""
return self.csolver.getInstantiations()
+ def getStatistics(self):
+ """
+ Returns a snapshot of the current state of the statistic values of this
+ solver. The returned object is completely decoupled from the solver and
+ will not change when the solver is used again.
+ """
+ res = Statistics()
+ res.cstats = self.csolver.getStatistics()
+ return res
+
cdef class Sort:
"""
return tuple_sorts
+cdef class Statistics:
+ """
+ The cvc5 Statistics.
+ Wrapper class for :cpp:class:`cvc5::api::Statistics`.
+ Obtain a single statistic value using ``stats["name"]`` and a dictionary
+ with all (visible) statistics using ``stats.get(internal=False, defaulted=False)``.
+ """
+ cdef c_Statistics cstats
+
+ cdef __stat_to_dict(self, const c_Stat& s):
+ res = None
+ if s.isInt():
+ res = s.getInt()
+ elif s.isDouble():
+ res = s.getDouble()
+ elif s.isString():
+ res = s.getString().decode()
+ elif s.isHistogram():
+ res = { h.first.decode(): h.second for h in s.getHistogram() }
+ return {
+ 'defaulted': s.isDefault(),
+ 'internal': s.isInternal(),
+ 'value': res
+ }
+
+ def __getitem__(self, str name):
+ """Get the statistics information for the statistic called ``name``."""
+ return self.__stat_to_dict(self.cstats.get(name.encode()))
+
+ def get(self, bint internal = False, bint defaulted = False):
+ """Get all statistics. See :cpp:class:`cvc5::api::Statistics::begin()` for more information."""
+ cdef c_Statistics.iterator it = self.cstats.begin(internal, defaulted)
+ cdef pair[string,c_Stat]* s
+ res = {}
+ while it != self.cstats.end():
+ s = &dereference(it)
+ res[s.first.decode()] = self.__stat_to_dict(s.second)
+ preincrement(it)
+ return res
+
+
cdef class Term:
"""
A cvc5 Term.
solver.checkSat()
solver.blockModelValues([x])
+def test_get_statistics(solver):
+ intSort = solver.getIntegerSort()
+ x = solver.mkConst(intSort, "x")
+ y = solver.mkConst(intSort, "y")
+ zero = solver.mkInteger(0)
+ ten = solver.mkInteger(10)
+ f0 = solver.mkTerm(Kind.Geq, x, ten)
+ f1 = solver.mkTerm(Kind.Or, solver.mkTerm(Kind.Geq, zero, x), solver.mkTerm(Kind.Geq, y, zero))
+ solver.assertFormula(f0)
+ solver.assertFormula(f1)
+ solver.checkSat()
+ s = solver.getStatistics()
+ assert s['api::TERM'] == {'defaulted': False, 'internal': False, 'value': {'GEQ': 3, 'OR': 1}}
+ assert s.get(True, False) != {}
+
def test_set_info(solver):
with pytest.raises(RuntimeError):
solver.setInfo("cvc5-lagic", "QF_BV")
projects / cvc5.git / commitdiff