Browse Source

bindings for cex generator stats

refactoring
Sebastian Junges 6 years ago
parent
commit
50f7e054f7
  1. 13
      src/core/counterexample.cpp

13
src/core/counterexample.cpp

@ -12,6 +12,19 @@ void define_counterexamples(py::module& m) {
.def("__str__", [](boost::container::flat_set<uint64_t> const& set) { std::stringstream str; str << "["; for(auto const& i : set) { str << i << ", ";} str << "]"; return str.str(); }) .def("__str__", [](boost::container::flat_set<uint64_t> const& set) { std::stringstream str; str << "["; for(auto const& i : set) { str << i << ", ";} str << "]"; return str.str(); })
.def("__len__", [](boost::container::flat_set<uint64_t> const& set) { return set.size();}) .def("__len__", [](boost::container::flat_set<uint64_t> const& set) { return set.size();})
; ;
using CexGeneratorStats = SMTMinimalLabelSetGenerator<double>::GeneratorStats;
py::class_<CexGeneratorStats>(m, "SMTCounterExampleGeneratorStats", "Stats for highlevel counterexample generation")
.def(py::init<>())
.def_readonly("analysis_time", &CexGeneratorStats::analysisTime)
.def_readonly("setup_time", &CexGeneratorStats::setupTime)
.def_readonly("model_checking_time", &CexGeneratorStats::modelCheckingTime)
.def_readonly("solver_time", &CexGeneratorStats::solverTime);
using CexGeneratorOptions = SMTMinimalLabelSetGenerator<double>::Options; using CexGeneratorOptions = SMTMinimalLabelSetGenerator<double>::Options;
py::class_<CexGeneratorOptions>(m, "SMTCounterExampleGeneratorOptions", "Options for highlevel counterexample generation") py::class_<CexGeneratorOptions>(m, "SMTCounterExampleGeneratorOptions", "Options for highlevel counterexample generation")
.def(py::init<>()) .def(py::init<>())

Loading…
Cancel
Save