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.
/** Whether the option was explicitly set by the user */
bool setByUser;
/** The option value information */
- std::variant<VoidInfo,
- ValueInfo<bool>,
- ValueInfo<std::string>,
- NumberInfo<int64_t>,
- NumberInfo<uint64_t>,
- NumberInfo<double>,
- ModeInfo>
- valueInfo;
+ using OptionInfoVariant = std::variant<VoidInfo,
+ ValueInfo<bool>,
+ ValueInfo<std::string>,
+ NumberInfo<int64_t>,
+ NumberInfo<uint64_t>,
+ NumberInfo<double>,
+ ModeInfo>;
+ OptionInfoVariant valueInfo;
/** Obtain the current value as a bool. Asserts that valueInfo holds a bool.
*/
bool boolValue() const;
hash()
size_t operator()(T t)
+cdef extern from "<optional>" 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 "<string>" namespace "std":
cdef cppclass wstring:
wstring() except +
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 "<variant>" 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 +
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 +
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
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
: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):
"""
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)
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())
projects / cvc5.git / commitdiff