Skip to content

Commit fb42b06

Browse files
committed
Implement smt2 get_number_of_solver_calls function
Because it is fairly straight forward to implement and doesn't depend on anything else. It isn't testable until the implementation can go through a complete call to `dec_solve`, at which point we should add tests of the count.
1 parent 9c60ccd commit fb42b06

File tree

2 files changed

+4
-3
lines changed

2 files changed

+4
-3
lines changed

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66

77
smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
88
std::string solver_command)
9-
: solver_command{std::move(solver_command)}
9+
: solver_command{std::move(solver_command)}, number_of_solver_calls{0}
1010
{
1111
}
1212

@@ -37,8 +37,7 @@ smt2_incremental_decision_proceduret::decision_procedure_text() const
3737
std::size_t
3838
smt2_incremental_decision_proceduret::get_number_of_solver_calls() const
3939
{
40-
UNIMPLEMENTED;
41-
return 0;
40+
return number_of_solver_calls;
4241
}
4342

4443
void smt2_incremental_decision_proceduret::set_to(const exprt &expr, bool value)
@@ -64,6 +63,7 @@ void smt2_incremental_decision_proceduret::pop()
6463

6564
decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
6665
{
66+
++number_of_solver_calls;
6767
UNIMPLEMENTED;
6868
return decision_proceduret::resultt::D_SATISFIABLE;
6969
}

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ class smt2_incremental_decision_proceduret final
3535

3636
/// This is where we store the solver command for reporting the solver used.
3737
std::string solver_command;
38+
size_t number_of_solver_calls;
3839
};
3940

4041
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H

0 commit comments

Comments
 (0)