def_static("precompute",&SMTMinimalLabelSetGenerator<double>::precompute,"Precompute input for counterexample generation",py::arg("env"),py::arg("symbolic_model"),py::arg("model"),py::arg("formula")).
py::class_<CexInput>(m,"SMTCounterExampleInput","Precomputed input for counterexample generation")
.def("add_reward_and_threshold",&CexInput::addRewardThresholdCombination,"add another reward structure and threshold",py::arg("reward_name"),py::arg("threshold"));