1 files changed, 101 insertions, 0 deletions
diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h
new file mode 100644
index 000000000..e607e13ce
--- /dev/null
+++ b/src/main/options_handlers.h
@@ -0,0 +1,101 @@
+/*********************                                                        */
+/*! \file options_handlers.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Custom handlers and predicates for main driver options
+ **
+ ** Custom handlers and predicates for main driver options.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__MAIN__OPTIONS_HANDLERS_H
+#define __CVC4__MAIN__OPTIONS_HANDLERS_H
+
+namespace CVC4 {
+namespace main {
+
+inline void showConfiguration(std::string option, SmtEngine* smt) {
+  fputs(Configuration::about().c_str(), stdout);
+  printf("\n");
+  printf("version    : %s\n", Configuration::getVersionString().c_str());
+  if(Configuration::isSubversionBuild()) {
+    printf("subversion : yes [%s r%u%s]\n",
+           Configuration::getSubversionBranchName(),
+           Configuration::getSubversionRevision(),
+           Configuration::hasSubversionModifications() ?
+             " (with modifications)" : "");
+  } else {
+    printf("subversion : %s\n", Configuration::isSubversionBuild() ? "yes" : "no");
+  }
+  printf("\n");
+  printf("library    : %u.%u.%u\n",
+         Configuration::getVersionMajor(),
+         Configuration::getVersionMinor(),
+         Configuration::getVersionRelease());
+  printf("\n");
+  printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no");
+  printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no");
+  printf("replay     : %s\n", Configuration::isReplayBuild() ? "yes" : "no");
+  printf("tracing    : %s\n", Configuration::isTracingBuild() ? "yes" : "no");
+  printf("dumping    : %s\n", Configuration::isDumpingBuild() ? "yes" : "no");
+  printf("muzzled    : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no");
+  printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no");
+  printf("proof      : %s\n", Configuration::isProofBuild() ? "yes" : "no");
+  printf("coverage   : %s\n", Configuration::isCoverageBuild() ? "yes" : "no");
+  printf("profiling  : %s\n", Configuration::isProfilingBuild() ? "yes" : "no");
+  printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no");
+  printf("\n");
+  printf("cudd       : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no");
+  printf("cln        : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no");
+  printf("gmp        : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no");
+  printf("tls        : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no");
+  exit(0);
+}
+
+inline void showDebugTags(std::string option, SmtEngine* smt) {
+  if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
+    printf("available tags:");
+    unsigned ntags = Configuration::getNumDebugTags();
+    char const* const* tags = Configuration::getDebugTags();
+    for(unsigned i = 0; i < ntags; ++ i) {
+      printf(" %s", tags[i]);
+    }
+    printf("\n");
+  } else if(! Configuration::isDebugBuild()) {
+    throw OptionException("debug tags not available in non-debug builds");
+  } else {
+    throw OptionException("debug tags not available in non-tracing builds");
+  }
+  exit(0);
+}
+
+inline void showTraceTags(std::string option, SmtEngine* smt) {
+  if(Configuration::isTracingBuild()) {
+    printf("available tags:");
+    unsigned ntags = Configuration::getNumTraceTags();
+    char const* const* tags = Configuration::getTraceTags();
+    for (unsigned i = 0; i < ntags; ++ i) {
+      printf(" %s", tags[i]);
+    }
+    printf("\n");
+  } else {
+    throw OptionException("trace tags not available in non-tracing build");
+  }
+  exit(0);
+}
+
+
+}/* CVC4::main namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__MAIN__OPTIONS_HANDLERS_H */