summaryrefslogtreecommitdiff
path: root/src/main/command_executor.cpp
diff options
context:
space:
mode:
authorKshitij Bansal <kshitij@cs.nyu.edu>2014-02-21 04:06:40 -0500
committerKshitij Bansal <kshitij@cs.nyu.edu>2014-02-21 08:11:37 -0500
commitabe8f7d24ec4323b44d7b7ecc366f59baa76c214 (patch)
tree1b7fab6135923ba590c8aadbc6da5ff86b351695 /src/main/command_executor.cpp
parent50c26544c83a71e87efa487e4af063b1b5647c0f (diff)
option to print stats after every satisfiability or validity query
Diffstat (limited to 'src/main/command_executor.cpp')
-rw-r--r--src/main/command_executor.cpp4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 485a478d8..601359cea 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -19,6 +19,7 @@
#include "main/main.h"
+#include "main/options.h"
#include "smt/options.h"
namespace CVC4 {
@@ -76,6 +77,9 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
if(q != NULL) {
d_result = res = q->getResult();
}
+ if((cs != NULL || q != NULL) && d_options[options::statsEveryQuery]) {
+ flushStatistics(*d_options[options::err]);
+ }
// dump the model/proof if option is set
if(status) {
if( d_options[options::produceModels] &&
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback