1 /********************* */
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
14 ** \brief Global (command-line, set-option, ...) parameters for SMT.
16 ** Global (command-line, set-option, ...) parameters for SMT.
19 #include "cvc4_public.h"
21 #ifndef __CVC4__OPTIONS_H
22 #define __CVC4__OPTIONS_H
28 #include "util/exception.h"
29 #include "util/language.h"
36 /** Class representing an option-parsing exception. */
37 class OptionException
: public CVC4::Exception
{
39 OptionException(const std::string
& s
) throw() :
40 CVC4::Exception("Error in option parsing: " + s
) {
42 };/* class OptionException */
44 struct CVC4_PUBLIC Options
{
46 /** The current Options in effect */
47 static CVC4_THREADLOCAL(const Options
*) s_current
;
49 /** Get the current Options in effect */
50 static inline const Options
* current() {
54 /** The name of the binary (e.g. "cvc4") */
55 std::string binary_name
;
57 /** Whether to collect statistics during this run */
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 */
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 */
71 /** The input language */
72 InputLanguage inputLanguage
;
74 /** Enumeration of UF implementation choices */
75 typedef enum { TIM
, MORGAN
} UfImplementation
;
77 /** Which implementation of uninterpreted function theory to use */
78 UfImplementation uf_implementation
;
80 /** Should we print the help message? */
83 /** Should we print the release information? */
86 /** Should we print the language help information? */
89 /** Should we exit after parsing? */
92 /** Should the parser do semantic checks? */
95 /** Should the TheoryEngine do theory registration? */
96 bool theoryRegistration
;
98 /** Should the parser memory-map file input? */
101 /** Should we strictly enforce the language standard while parsing? */
104 /** Should we expand function definitions lazily? */
105 bool lazyDefinitionExpansion
;
107 /** Whether we're in interactive mode or not */
111 * Whether we're in interactive mode (or not) due to explicit user
112 * setting (if false, we inferred the proper default setting).
114 bool interactiveSetByUser
;
116 /** Whether we should "spin" on a SIG_SEGV. */
119 /** Whether we support SmtEngine::getValue() for this run. */
122 /** Whether we support SmtEngine::getAssignment() for this run. */
123 bool produceAssignments
;
125 /** Whether we do typechecking at all. */
128 /** Whether we do typechecking at Expr creation time. */
129 bool earlyTypeChecking
;
131 /** Whether incemental solving (push/pop) */
132 bool incrementalSolving
;
134 /** Replay file to use (for decisions); empty if no replay file. */
135 std::string replayFilename
;
137 /** Replay stream to use (for decisions); NULL if no replay file. */
138 ExprStream
* replayStream
;
140 /** Log to write replay instructions to; NULL if not logging. */
141 std::ostream
* replayLog
;
143 /** Whether to rewrite equalities in arithmetic theory */
144 bool rewriteArithEqualities
;
146 /** Turn on and of arithmetic propagation. */
147 bool arithPropagation
;
150 * Frequency for the sat solver to make random decisions.
151 * Should be between 0 and 1.
153 double satRandomFreq
;
156 * Seed for Minisat's random decision procedure.
157 * If this is 0, no random decisions will occur.
159 double satRandomSeed
;
161 /** The pivot rule for arithmetic */
162 typedef enum { MINIMUM
, BREAK_TIES
, MAXIMUM
} ArithPivotRule
;
163 ArithPivotRule pivotRule
;
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;
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"
178 static void printUsage(const std::string msg
, std::ostream
& out
);
180 /** Print help for the --lang command line option */
181 static void printLanguageHelp(std::ostream
& out
);
184 * Initialize the options based on the given command-line arguments.
186 int parseOptions(int argc
, char* argv
[])
187 throw(OptionException
);
188 };/* struct Options */
190 inline std::ostream
& operator<<(std::ostream
& out
,
191 Options::UfImplementation uf
) {
196 case Options::MORGAN
:
200 out
<< "UfImplementation:UNKNOWN![" << unsigned(uf
) << "]";
206 std::ostream
& operator<<(std::ostream
& out
, Options::ArithPivotRule rule
);
208 }/* CVC4 namespace */
210 #endif /* __CVC4__OPTIONS_H */