File tree Expand file tree Collapse file tree 1 file changed +8
-0
lines changed
src/solvers/smt2_incremental Expand file tree Collapse file tree 1 file changed +8
-0
lines changed Original file line number Diff line number Diff line change @@ -87,6 +87,14 @@ class smt_get_value_commandt : public smt_commandt,
8787 protected smt_termt::storert<smt_assert_commandt>
8888{
8989public:
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};
You can’t perform that action at this time.
0 commit comments