diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-02-27 16:43:48 -0500 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-02-27 17:14:43 -0500 |
| commit | e104d78c5f9f5ee8e931bc4c1b460cfc68a98498 (patch) | |
| tree | 7d9b4e4959917c3ff9cee52011a423f00f942d0c /src/main/command_executor.h | |
| parent | 251fd73a759a8e5e94103e9b76a06491a92e425b (diff) | |
--stats-every-query option: print increment in addition to cumulative value of each stat
the increment is printed in parantheses at the end, e.g.
sat::decisions, 100 (50)
Diffstat (limited to 'src/main/command_executor.h')
| -rw-r--r-- | src/main/command_executor.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/main/command_executor.h b/src/main/command_executor.h index cbc71b075..5395cc804 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -28,6 +28,8 @@ namespace CVC4 { namespace main { class CommandExecutor { +private: + std::string d_lastStatistics; protected: ExprManager& d_exprMgr; |