Skip to content

Commit fd2cf39

Browse files
committed
Document existing decision_procedure_test_environmentt
In order to make it easier to reuse when writing new tests.
1 parent 8067e1b commit fd2cf39

File tree

1 file changed

+8
-0
lines changed

1 file changed

+8
-0
lines changed

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,14 @@ class smt_mock_solver_processt : public smt_base_solver_processt
8585
~smt_mock_solver_processt() override = default;
8686
};
8787

88+
/// \brief Data structures and their initialisation shared between tests.
89+
/// \details
90+
/// Instantiates a `smt2_incremental_decision_proceduret` using a mock of the
91+
/// solver process to direct communication with the solver to collections of
92+
/// `sent_commands` and `mock_responses`. The `mock_respones` must be
93+
/// populated by the test, before the decision procedure expects them. The
94+
/// `sent_commands` should be checked by the test after the decision procedure
95+
/// has sent them.
8896
struct decision_procedure_test_environmentt final
8997
{
9098
void send(const smt_commandt &smt_command);

0 commit comments

Comments
 (0)