From 2ac815b8269378d400ae108b2ed458d6b9e0715a Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Fri, 8 Jun 2018 13:17:56 +0200
Subject: [PATCH] extended wrapper for counterexamples:

---
 src/core/counterexample.cpp | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

diff --git a/src/core/counterexample.cpp b/src/core/counterexample.cpp
index 6fbb6a1..7f8be55 100644
--- a/src/core/counterexample.cpp
+++ b/src/core/counterexample.cpp
@@ -5,11 +5,22 @@ using namespace storm::counterexamples;
 
 // Define python bindings
 void define_counterexamples(py::module& m) {
-    py::class_<boost::container::flat_set<uint_fast64_t>>(m, "FlatSet", "Container to pass to program");
-
-
+    py::class_<boost::container::flat_set<uint_fast64_t>>(m, "FlatSet", "Container to pass to program")
+            .def(py::init<>())
+            .def("insert", [](boost::container::flat_set<uint_fast64_t>& flatset, uint64_t value) {flatset.insert(value);})
+            .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();})
+            ;
+    using CexGeneratorOptions =  SMTMinimalLabelSetGenerator<double>::Options;
+            py::class_<CexGeneratorOptions>(m, "SMTCounterExampleGeneratorOptions", "Options for highlevel counterexample generation")
+                    .def(py::init<>())
+                    .def_readwrite("check_threshold_feasible", &CexGeneratorOptions::checkThresholdFeasible)
+                    .def_readwrite("encode_reachability", &CexGeneratorOptions::encodeReachability)
+                    .def_readwrite("silent", &CexGeneratorOptions::silent)
+                    .def_readwrite("use_dynamic_constraints", &CexGeneratorOptions::useDynamicConstraints)
+            ;
             py::class_<SMTMinimalLabelSetGenerator<double>>(m, "SMTCounterExampleGenerator", "Highlevel Counterexample Generator with SMT as backend").
-            def_static("build", &SMTMinimalLabelSetGenerator<double>::computeCounterexampleLabelSet)
+            def_static("build", &SMTMinimalLabelSetGenerator<double>::computeCounterexampleLabelSet, "Compute counterexample", py::arg("env"), py::arg("symbolic_model"), py::arg("model"), py::arg("formula"), py::arg("dontcare"), py::arg("options"))
             ;