src/util/options.h

   1 /*********************                                                        */
   2 /*! \file options.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: cconway
   6  ** Minor contributors (to current version): dejan, taking
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Global (command-line, set-option, ...) parameters for SMT.
  15  **
  16  ** Global (command-line, set-option, ...) parameters for SMT.
  17  **/
  18
  19 #include "cvc4_public.h"
  20
  21 #ifndef __CVC4__OPTIONS_H
  22 #define __CVC4__OPTIONS_H
  23
  24 #include <iostream>
  25 #include <fstream>
  26 #include <string>
  27
  28 #include "util/exception.h"
  29 #include "util/language.h"
  30 #include "util/tls.h"
  31
  32 namespace CVC4 {
  33
  34 class ExprStream;
  35
  36 /** Class representing an option-parsing exception. */
  37 class OptionException : public CVC4::Exception {
  38 public:
  39     OptionException(const std::string& s) throw() :
  40       CVC4::Exception("Error in option parsing: " + s) {
  41     }
  42 };/* class OptionException */
  43
  44 struct CVC4_PUBLIC Options {
  45
  46   /** The current Options in effect */
  47   static CVC4_THREADLOCAL(const Options*) s_current;
  48
  49   /** Get the current Options in effect */
  50   static inline const Options* current() {
  51     return s_current;
  52   }
  53
  54   /** The name of the binary (e.g. "cvc4") */
  55   std::string binary_name;
  56
  57   /** Whether to collect statistics during this run */
  58   bool statistics;
  59
  60   std::istream* in; /*< The input stream to use */
  61   std::ostream* out; /*< The output stream to use */
  62   std::ostream* err; /*< The error stream to use */
  63
  64   /* -1 means no output */
  65   /* 0 is normal (and default) -- warnings only */
  66   /* 1 is warnings + notices so the user doesn't get too bored */
  67   /* 2 is chatty, giving statistical things etc. */
  68   /* with 3, the solver is slowed down by all the scrolling */
  69   int verbosity;
  70
  71   /** The input language */
  72   InputLanguage inputLanguage;
  73
  74   /** Enumeration of UF implementation choices */
  75   typedef enum { TIM, MORGAN } UfImplementation;
  76
  77   /** Which implementation of uninterpreted function theory to use */
  78   UfImplementation uf_implementation;
  79
  80   /** Should we print the help message? */
  81   bool help;
  82
  83   /** Should we print the release information? */
  84   bool version;
  85
  86   /** Should we print the language help information? */
  87   bool languageHelp;
  88
  89   /** Should we exit after parsing? */
  90   bool parseOnly;
  91
  92   /** Should the parser do semantic checks? */
  93   bool semanticChecks;
  94
  95   /** Should the TheoryEngine do theory registration? */
  96   bool theoryRegistration;
  97
  98   /** Should the parser memory-map file input? */
  99   bool memoryMap;
 100
 101   /** Should we strictly enforce the language standard while parsing? */
 102   bool strictParsing;
 103
 104   /** Should we expand function definitions lazily? */
 105   bool lazyDefinitionExpansion;
 106
 107   /** Whether we're in interactive mode or not */
 108   bool interactive;
 109
 110   /**
 111    * Whether we're in interactive mode (or not) due to explicit user
 112    * setting (if false, we inferred the proper default setting).
 113    */
 114   bool interactiveSetByUser;
 115
 116   /** Whether we should "spin" on a SIG_SEGV. */
 117   bool segvNoSpin;
 118
 119   /** Whether we support SmtEngine::getValue() for this run. */
 120   bool produceModels;
 121
 122   /** Whether we support SmtEngine::getAssignment() for this run. */
 123   bool produceAssignments;
 124
 125   /** Whether we do typechecking at all. */
 126   bool typeChecking;
 127
 128   /** Whether we do typechecking at Expr creation time. */
 129   bool earlyTypeChecking;
 130
 131   /** Whether incemental solving (push/pop) */
 132   bool incrementalSolving;
 133
 134   /** Replay file to use (for decisions); empty if no replay file. */
 135   std::string replayFilename;
 136
 137   /** Replay stream to use (for decisions); NULL if no replay file. */
 138   ExprStream* replayStream;
 139
 140   /** Log to write replay instructions to; NULL if not logging. */
 141   std::ostream* replayLog;
 142
 143   /** Whether to rewrite equalities in arithmetic theory */
 144   bool rewriteArithEqualities;
 145
 146   /** Turn on and of arithmetic propagation. */
 147   bool arithPropagation;
 148
 149   /**
 150    * Frequency for the sat solver to make random decisions.
 151    * Should be between 0 and 1.
 152    */
 153   double satRandomFreq;
 154
 155   /**
 156    * Seed for Minisat's random decision procedure.
 157    * If this is 0, no random decisions will occur.
 158    **/
 159   double satRandomSeed;
 160
 161   /** The pivot rule for arithmetic */
 162   typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule;
 163   ArithPivotRule pivotRule;
 164
 165   Options();
 166
 167   /**
 168    * Get a description of the command-line flags accepted by
 169    * parseOptions.  The returned string will be escaped so that it is
 170    * suitable as an argument to printf. */
 171   std::string getDescription() const;
 172
 173   /**
 174    * Print overall command-line option usage message, prefixed by
 175    * "msg"---which could be an error message causing the usage
 176    * output in the first place, e.g. "no such option --foo"
 177    */
 178   static void printUsage(const std::string msg, std::ostream& out);
 179
 180   /** Print help for the --lang command line option */
 181   static void printLanguageHelp(std::ostream& out);
 182
 183   /**
 184    * Initialize the options based on the given command-line arguments.
 185    */
 186   int parseOptions(int argc, char* argv[])
 187     throw(OptionException);
 188 };/* struct Options */
 189
 190 inline std::ostream& operator<<(std::ostream& out,
 191                                 Options::UfImplementation uf) {
 192   switch(uf) {
 193   case Options::TIM:
 194     out << "TIM";
 195     break;
 196   case Options::MORGAN:
 197     out << "MORGAN";
 198     break;
 199   default:
 200     out << "UfImplementation:UNKNOWN![" << unsigned(uf) << "]";
 201   }
 202
 203   return out;
 204 }
 205
 206 std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule);
 207
 208 }/* CVC4 namespace */
 209
 210 #endif /* __CVC4__OPTIONS_H */