From 774b08351672eedee89e8cb4eba41e3c012bb777 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 23 Mar 2022 20:53:18 +0100 Subject: [PATCH] Add `getOptionInfo()` and `getOptionNames()` to python API (#8342) These extended options operations were still missing from the python API and are added with this PR. To simplify the integration (and also provide a reasonably pythonic interface) we return a dictionary from getOptionInfo() instead of exposing a std::variant-like interface. The PR also includes the corresponding unit tests. --- src/api/cpp/cvc5.h | 16 +++--- src/api/python/cvc5.pxd | 49 ++++++++++++++++- src/api/python/cvc5.pxi | 84 ++++++++++++++++++++++++++++- test/unit/api/python/CMakeLists.txt | 16 +++--- test/unit/api/python/test_solver.py | 73 ++++++++++++++++++++++++- 5 files changed, 219 insertions(+), 19 deletions(-) diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 6480a7b75..9adae1337 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -2774,14 +2774,14 @@ struct CVC5_EXPORT OptionInfo /** Whether the option was explicitly set by the user */ bool setByUser; /** The option value information */ - std::variant, - ValueInfo, - NumberInfo, - NumberInfo, - NumberInfo, - ModeInfo> - valueInfo; + using OptionInfoVariant = std::variant, + ValueInfo, + NumberInfo, + NumberInfo, + NumberInfo, + ModeInfo>; + OptionInfoVariant valueInfo; /** Obtain the current value as a bool. Asserts that valueInfo holds a bool. */ bool boolValue() const; diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index ed11921b8..5f7b61cb5 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -21,6 +21,14 @@ cdef extern from "" namespace "std" nogil: hash() size_t operator()(T t) +cdef extern from "" namespace "std" nogil: + # The std::optional wrapper would be available as cpplib.optional with + # cython 3.0.0a10 (Jan 2022). Until this version is widely available, we + # wrap it manually. + cdef cppclass optional[T]: + bint has_value() + T& value() + cdef extern from "" namespace "std": cdef cppclass wstring: wstring() except + @@ -136,7 +144,44 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": OpHashFunction() except + size_t operator()(const Op & o) except + + cdef cppclass OptionInfo: + string name + vector[string] aliases + bint setByUser + bint boolValue() except + + string stringValue() except + + int intValue() except + + int uintValue() except + + float doubleValue() except + + cppclass VoidInfo: + pass + cppclass ValueInfo[T]: + T defaultValue + T currentValue + cppclass NumberInfo[T]: + T defaultValue + T currentValue + optional[T] minimum + optional[T] maximum + cppclass ModeInfo: + string defaultValue + string currentValue + vector[string] modes + + cppclass OptionInfoVariant: + pass + + OptionInfoVariant valueInfo + string toString() except + + +cdef extern from "" namespace "std": + # cython has no support for variadic templates yet, see + # https://github.com/cython/cython/issues/1611 + bint holds "std::holds_alternative"[T](OptionInfo.OptionInfoVariant v) except + + T getVariant "std::get"[T](OptionInfo.OptionInfoVariant v) except + + +cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": cdef cppclass Result: Result() except+ bint isNull() except + @@ -274,7 +319,9 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": vector[Term] getLearnedLiterals() except + vector[Term] getAssertions() except + string getInfo(const string& flag) except + - string getOption(string& option) except + + string getOption(const string& option) except + + vector[string] getOptionNames() except + + OptionInfo getOptionInfo(const string& option) except + vector[Term] getUnsatAssumptions() except + vector[Term] getUnsatCore() except + Term getValue(Term term) except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 46fd480cb..9ef53b86b 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -8,6 +8,7 @@ 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 libcpp cimport bool as c_bool from libcpp.pair cimport pair from libcpp.set cimport set as c_set from libcpp.string cimport string @@ -23,6 +24,9 @@ from cvc5 cimport Result as c_Result from cvc5 cimport RoundingMode as c_RoundingMode from cvc5 cimport UnknownExplanation as c_UnknownExplanation from cvc5 cimport Op as c_Op +from cvc5 cimport OptionInfo as c_OptionInfo +from cvc5 cimport holds as c_holds +from cvc5 cimport getVariant as c_getVariant from cvc5 cimport Solver as c_Solver from cvc5 cimport Statistics as c_Statistics from cvc5 cimport Stat as c_Stat @@ -1979,7 +1983,85 @@ cdef class Solver: :param option: the option for which the value is queried :return: a string representation of the option value """ - return self.csolver.getOption(option.encode()) + return self.csolver.getOption(option.encode()).decode() + + def getOptionNames(self): + """Get all option names that can be used with `setOption`, `getOption` and `getOptionInfo`. + + :return: all option names + """ + return [s.decode() for s in self.csolver.getOptionNames()] + + def getOptionInfo(self, str option): + """Get some information about the given option. Check the `OptionInfo` + class for more details on which information is available. + + :return: information about the given option + """ + # declare all the variables we may need later + cdef c_OptionInfo.ValueInfo[c_bool] vib + cdef c_OptionInfo.ValueInfo[string] vis + cdef c_OptionInfo.NumberInfo[int64_t] nii + cdef c_OptionInfo.NumberInfo[uint64_t] niu + cdef c_OptionInfo.NumberInfo[double] nid + cdef c_OptionInfo.ModeInfo mi + + oi = self.csolver.getOptionInfo(option.encode()) + # generic information + res = { + 'name': oi.name.decode(), + 'aliases': [s.decode() for s in oi.aliases], + 'setByUser': oi.setByUser, + } + + # now check which type is actually in the variant + if c_holds[c_OptionInfo.VoidInfo](oi.valueInfo): + # it's a void + res['type'] = None + elif c_holds[c_OptionInfo.ValueInfo[c_bool]](oi.valueInfo): + # it's a bool + res['type'] = bool + vib = c_getVariant[c_OptionInfo.ValueInfo[c_bool]](oi.valueInfo) + res['current'] = vib.currentValue + res['default'] = vib.defaultValue + elif c_holds[c_OptionInfo.ValueInfo[string]](oi.valueInfo): + # it's a string + res['type'] = str + vis = c_getVariant[c_OptionInfo.ValueInfo[string]](oi.valueInfo) + res['current'] = vis.currentValue.decode() + res['default'] = vis.defaultValue.decode() + elif c_holds[c_OptionInfo.NumberInfo[int64_t]](oi.valueInfo): + # it's an int64_t + res['type'] = int + nii = c_getVariant[c_OptionInfo.NumberInfo[int64_t]](oi.valueInfo) + res['current'] = nii.currentValue + res['default'] = nii.defaultValue + res['minimum'] = nii.minimum.value() if nii.minimum.has_value() else None + res['maximum'] = nii.maximum.value() if nii.maximum.has_value() else None + elif c_holds[c_OptionInfo.NumberInfo[uint64_t]](oi.valueInfo): + # it's a uint64_t + res['type'] = int + niu = c_getVariant[c_OptionInfo.NumberInfo[uint64_t]](oi.valueInfo) + res['current'] = niu.currentValue + res['default'] = niu.defaultValue + res['minimum'] = niu.minimum.value() if niu.minimum.has_value() else None + res['maximum'] = niu.maximum.value() if niu.maximum.has_value() else None + elif c_holds[c_OptionInfo.NumberInfo[double]](oi.valueInfo): + # it's a double + res['type'] = float + nid = c_getVariant[c_OptionInfo.NumberInfo[double]](oi.valueInfo) + res['current'] = nid.currentValue + res['default'] = nid.defaultValue + res['minimum'] = nid.minimum.value() if nid.minimum.has_value() else None + res['maximum'] = nid.maximum.value() if nid.maximum.has_value() else None + elif c_holds[c_OptionInfo.ModeInfo](oi.valueInfo): + # it's a mode + res['type'] = 'mode' + mi = c_getVariant[c_OptionInfo.ModeInfo](oi.valueInfo) + res['current'] = mi.currentValue.decode() + res['default'] = mi.defaultValue.decode() + res['modes'] = [s.decode() for s in mi.modes] + return res def getUnsatAssumptions(self): """ diff --git a/test/unit/api/python/CMakeLists.txt b/test/unit/api/python/CMakeLists.txt index 3c1a811f8..a322bbcc2 100644 --- a/test/unit/api/python/CMakeLists.txt +++ b/test/unit/api/python/CMakeLists.txt @@ -30,11 +30,11 @@ macro(cvc5_add_python_api_unit_test name filename) endmacro() # add specific test files -cvc5_add_python_api_unit_test(pytest_solver test_solver.py) -cvc5_add_python_api_unit_test(pytest_sort test_sort.py) -cvc5_add_python_api_unit_test(pytest_term test_term.py) -cvc5_add_python_api_unit_test(pytest_datatype_api test_datatype_api.py) -cvc5_add_python_api_unit_test(pytest_grammar test_grammar.py) -cvc5_add_python_api_unit_test(pytest_to_python_obj test_to_python_obj.py) -cvc5_add_python_api_unit_test(pytest_op test_op.py) -cvc5_add_python_api_unit_test(pytest_result test_result.py) +cvc5_add_python_api_unit_test(test_solver test_solver.py) +cvc5_add_python_api_unit_test(test_sort test_sort.py) +cvc5_add_python_api_unit_test(test_term test_term.py) +cvc5_add_python_api_unit_test(test_datatype_api test_datatype_api.py) +cvc5_add_python_api_unit_test(test_grammar test_grammar.py) +cvc5_add_python_api_unit_test(test_to_python_obj test_to_python_obj.py) +cvc5_add_python_api_unit_test(test_op test_op.py) +cvc5_add_python_api_unit_test(test_result test_result.py) diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index a05421ab2..e47ee8f6f 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -1176,11 +1176,82 @@ def test_get_op(solver): def test_get_option(solver): - solver.getOption("incremental") + solver.setOption("incremental", "true") + assert solver.getOption("incremental") == "true" with pytest.raises(RuntimeError): solver.getOption("asdf") +def test_get_option_names(solver): + opts = solver.getOptionNames() + assert len(opts) > 100 + assert "verbose" in opts + assert "foobar" not in opts + + +def test_get_option_info(solver): + with pytest.raises(RuntimeError): + solver.getOptionInfo("asdf-invalid") + + info = solver.getOptionInfo("verbose") + assert info['name'] == "verbose" + assert info['aliases'] == [] + assert not info['setByUser'] + assert info['type'] is None + + info = solver.getOptionInfo("print-success") + assert info['name'] == "print-success" + assert info['aliases'] == [] + assert not info['setByUser'] + assert info['type'] is bool + assert info['current'] == False + assert info['default'] == False + + info = solver.getOptionInfo("verbosity") + assert info['name'] == "verbosity" + assert info['aliases'] == [] + assert not info['setByUser'] + assert info['type'] is int + assert info['current'] == 0 + assert info['default'] == 0 + assert info['minimum'] is None and info['maximum'] is None + + info = solver.getOptionInfo("rlimit") + assert info['name'] == "rlimit" + assert info['aliases'] == [] + assert not info['setByUser'] + assert info['type'] is int + assert info['current'] == 0 + assert info['default'] == 0 + assert info['minimum'] is None and info['maximum'] is None + + info = solver.getOptionInfo("random-freq") + assert info['name'] == "random-freq" + assert info['aliases'] == ["random-frequency"] + assert not info['setByUser'] + assert info['type'] is float + assert info['current'] == 0.0 + assert info['default'] == 0.0 + assert info['minimum'] == 0.0 and info['maximum'] == 1.0 + + info = solver.getOptionInfo("force-logic") + assert info['name'] == "force-logic" + assert info['aliases'] == [] + assert not info['setByUser'] + assert info['type'] is str + assert info['current'] == "" + assert info['default'] == "" + + info = solver.getOptionInfo("simplification") + assert info['name'] == "simplification" + assert info['aliases'] == ["simplification-mode"] + assert not info['setByUser'] + assert info['type'] == 'mode' + assert info['current'] == 'batch' + assert info['default'] == 'batch' + assert info['modes'] == ['batch', 'none'] + + def test_get_unsat_assumptions1(solver): solver.setOption("incremental", "false") solver.checkSatAssuming(solver.mkFalse()) -- 2.30.2