diff --git a/src/core/counterexample.cpp b/src/core/counterexample.cpp index b3eb054..b4cb1e2 100644 --- a/src/core/counterexample.cpp +++ b/src/core/counterexample.cpp @@ -1,3 +1,5 @@ +#include + #include "counterexample.h" #include "storm/environment/Environment.h" #include "storm-counterexamples/api/counterexamples.h" @@ -11,9 +13,15 @@ void define_counterexamples(py::module& m) { py::class_>(m, "FlatSet", "Container to pass to program") .def(py::init<>()) + .def(py::init>(), "other"_a) .def("insert", [](boost::container::flat_set& flatset, uint64_t value) {flatset.insert(value);}) + .def("is_subset_of", [](boost::container::flat_set const& left, boost::container::flat_set const& right) {return std::includes(right.begin(), right.end(), left.begin(), left.end()); }) + .def("insert_set", [](boost::container::flat_set& left, boost::container::flat_set const& additional) { for(auto const& i : additional) {left.insert(i);}}) .def("__str__", [](boost::container::flat_set const& set) { std::stringstream str; str << "["; for(auto const& i : set) { str << i << ", ";} str << "]"; return str.str(); }) .def("__len__", [](boost::container::flat_set const& set) { return set.size();}) + .def("__iter__", [](boost::container::flat_set &v) { + return py::make_iterator(v.begin(), v.end()); + }, py::keep_alive<0, 1>()) /* Keep vector alive while iterator is used */ ; using CexGeneratorStats = SMTMinimalLabelSetGenerator::GeneratorStats;