summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r--src/smt/smt_engine.h11
1 files changed, 10 insertions, 1 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 16434d6d7..de3a64ff6 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -247,11 +247,20 @@ class CVC4_EXPORT SmtEngine
* to a state where its options were prior to parsing but after e.g.
* reading command line options.
*/
- void notifyStartParsing(std::string filename) CVC4_EXPORT;
+ void notifyStartParsing(const std::string& filename) CVC4_EXPORT;
/** return the input name (if any) */
const std::string& getFilename() const;
/**
+ * Helper method for the API to put the last check result into the statistics.
+ */
+ void setResultStatistic(const std::string& result) CVC4_EXPORT;
+ /**
+ * Helper method for the API to put the total runtime into the statistics.
+ */
+ void setTotalTimeStatistic(double seconds) CVC4_EXPORT;
+
+ /**
* Get the model (only if immediately preceded by a SAT or NOT_ENTAILED
* query). Only permitted if produce-models is on.
*/
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback