Skip to content

Commit 947aae8

Browse files
committed
Document limitations of smt_get_value_commandt
So that future maintainers can be made aware of this discrepency between the standards and the capabilities of `smt_get_value_commandt`.
1 parent b371c81 commit 947aae8

File tree

1 file changed

+8
-0
lines changed

1 file changed

+8
-0
lines changed

src/solvers/smt2_incremental/smt_commands.h

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -87,6 +87,14 @@ class smt_get_value_commandt : public smt_commandt,
8787
protected smt_termt::storert<smt_assert_commandt>
8888
{
8989
public:
90+
/// \brief This constructor constructs the `get-value` command, such that it
91+
/// stores a single descriptor for which the solver will be commanded to
92+
/// respond with a value.
93+
/// \note This class currently supports storing a single descriptor only,
94+
/// whereas the SMT-LIB standard version 2.6 supports one or more
95+
/// descriptors. Getting one value at a time is currently sufficient for our
96+
/// requirements. This class could be expanded should there be a need to get
97+
/// multiple values at once.
9098
explicit smt_get_value_commandt(smt_termt descriptor);
9199
const smt_termt &descriptor() const;
92100
};

0 commit comments

Comments
 (0)