summaryrefslogtreecommitdiff
path: root/src/util/options.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/options.h')
-rw-r--r--src/util/options.h31
1 files changed, 31 insertions, 0 deletions
diff --git a/src/util/options.h b/src/util/options.h
new file mode 100644
index 000000000..f04b06f10
--- /dev/null
+++ b/src/util/options.h
@@ -0,0 +1,31 @@
+#ifndef __CVC4_OPTIONS_H
+#define __CVC4_OPTIONS_H
+
+namespace CVC4 {
+
+struct Options {
+ std::string binary_name;
+
+ bool smtcomp_mode;
+ bool statistics;
+
+ /* -1 means no output */
+ /* 0 is normal (and default) -- warnings only */
+ /* 1 is warnings + notices so the user doesn't get too bored */
+ /* 2 is chatty, giving statistical things etc. */
+ /* with 3, the solver is slowed down by all the scrolling */
+ int verbosity;
+
+ std::string lang;
+
+ Options() : binary_name(),
+ smtcomp_mode(false),
+ statistics(false),
+ verbosity(0),
+ lang()
+ {}
+};/* struct Options */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_OPTIONS_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback