52 IF_DEBUG(
static DebugTimer* pRuntime = NULL;)
56 cerr <<
"\nInterrupted by signal " << signum;
58 cerr <<
" (self-timeout)";
61 IF_DEBUG(
if (pRuntime != NULL) CVC3::debugger.setElapsed(*pRuntime);)
63 if(vc != NULL && vc->
getFlags()[
"stats"].getBool())
75 DWORD WINAPI thread_timeout(PVOID timeout) {
76 Sleep((
int)timeout * 1000);
77 cerr <<
"(self-timeout)." <<
endl;
78 if(vc != NULL && vc->
getFlags()[
"stats"].getBool())
92 int main(
int argc,
char **argv)
94 CLFlags flags(ValidityChecker::createFlags());
96 IF_DEBUG(DebugTimer runtime(CVC3::debugger.timer(
"total runtime"));)
113 cerr <<
"\n\nRun with -help option for usage information." <<
endl;
119 if(flags[
"lang"].getString() !=
"" &&
121 !flags[
"internal::userSetNoSaveModel"].getBool()) {
122 flags.
setFlag(
"no-save-model",
true);
126 int timeout = flags[
"timeout"].getInt();
132 CreateThread(NULL, 0, thread_timeout, (PVOID)timeout, 0, NULL);
142 vc = ValidityChecker::create(flags);
144 cerr <<
"*** Fatal exception: " << e <<
endl;
150 if(!vc->
getFlags()[
"help"].getBool()) {
154 if(!vc->
getFlags()[
"unsupported"].getBool()) {
159 #define VERSION "unknown"
162 if(!vc->
getFlags()[
"version"].getBool()) {
163 cout <<
"This is CVC3 version " <<
VERSION
167 "Copyright (C) 2003-2010 by the Board of Trustees of Leland Stanford Junior\n"
168 "University, New York University, and the University of Iowa.\n\n"
169 "THIS SOFTWARE PROVIDED AS-IS, WITHOUT ANY WARRANTIES. "
170 "USE IT AT YOUR OWN RISK.\n"
180 vc->
getFlags()[
"translate"].getBool() &&
181 !vc->
getFlags()[
"liftITE"].modified()) {
186 IF_DEBUG(CVC3::debugger.setCurrentTime(runtime);)
189 flags[
"interactive"].getBool());
191 cerr <<
"*** Fatal exception: " << e <<
endl;
195 IF_DEBUG(CVC3::debugger.setElapsed(runtime);)
202 TRACE_MSG(
"delete",
"Deleting ValidityChecker [last trace from main.cpp]");
210 cerr <<
"*** Fatal exception: " << e <<
endl;
219 <<
programName <<
" will read the input from STDIN and \n"
220 <<
"print the result on STDOUT.\n"
221 <<
"Boolean (b) options are set 'on' by +option and 'off' by -option\n"
222 <<
"(for instance, +model or -model).\n"
223 <<
"Integer (i), string (s) and vector (v) options \n"
224 <<
"require a parameter, e.g. -width 80\n"
225 <<
"Also, (v) options can appear multiple times setting "
226 <<
"args on and off,\n"
227 <<
"as in +trace \"enable this\" -trace \"disable that\".\n"
228 <<
"Option names can be abbreviated to the "
229 <<
"shortest unambiguous prefix.\n\n"
230 <<
"The options are:\n";
231 vector<string> names;
234 for(
size_t i=0,iend=names.size(); i!=iend; ++i) {
235 const CLFlag& f(flags[names[i]]);
236 if (f.
display() != followDisplay)
continue;
239 string name(names[i]);
244 tpStr =
"(b)"; pref = (f.
getBool())?
"+" :
"-";
250 tpStr =
"(s)"; pref =
"-"; name = name+
" "+f.
getString();
253 tpStr =
"(v)"; pref =
"-"; name = name;
256 DebugAssert(
false,
"printUsage: unknown flag type");
258 cout <<
" " << tpStr <<
" " << pref << setw(25);
260 cout << name <<
" " << f.
getHelp() <<
"\n";
270 bool seenFileName(
false);
272 for( ; argc > 0; argc--, argv++) {
273 if((*argv)[0] ==
'-' || (*argv)[0] ==
'+') {
275 vector<string> names;
276 bool val = ((*argv)[0] ==
'+');
277 size_t n = flags.
countFlags((*argv)+1, names);
279 throw CLException(
string(*argv) +
" does not match any known option");
282 ss << *argv <<
" is ambiguous. Possible matches are:\n";
283 for(
size_t i=0,iend=names.size(); i!=iend; ++i) {
284 ss <<
" " << names[i] <<
"\n";
288 string name = names[0];
289 if(name ==
"no-save-model") {
290 flags.
setFlag(
"internal::userSetNoSaveModel",
true);
300 +
") expects an integer argument.");
303 flags.
setFlag(name, atoi(*argv));
309 +
") expects a string argument.");
317 +
") expects a string argument.");
319 flags.
setFlag(name, pair<string,bool>(*argv,val));
325 }
else if(seenFileName) {
326 throw CLException(
"More than one file name given: "+fileName
327 +
" and "+
string(*argv));
329 fileName = string(*argv);
for output in SPASS format
virtual ExprManager * getEM()=0
Return the ExprManager.
Generic API for a validity checker.
int main(int argc, char **argv)
bool display() const
Return true if flag should be displayed in regular help.
void setFlag(const std::string &name, const CLFlag &f)
InputLanguage
Different input languages.
InputLanguage getInputLang() const
Get the input language for printing.
void sighandler(int signum)
CLFlagType
Different types of command line flags.
static void parse_args(int argc, char **argv, CLFlags &flags, string &fileName)
#define DebugAssert(cond, str)
Description: Counters and flags for collecting run-time statistics.
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
virtual Statistics & getStatistics()=0
Get statistics object.
static void printUsage(const CLFlags &flags, bool followDisplay)
#define TRACE_MSG(flag, msg)
virtual CLFlags & getFlags() const =0
Return the set of command-line flags.
static ValidityChecker * vc
Abstraction over different operating systems.
const std::string & getHelp() const
std::string int2string(int n)
Generic API for a validity checker.
virtual void printStatistics()=0
Print collected statistics to stdout.
const std::string & getString() const
static string programName
virtual void loadFile(const std::string &fileName, InputLanguage lang=PRESENTATION_LANG, bool interactive=false, bool calledFromParser=false)=0
Read and execute the commands from a file given by name ("" means stdin)
const int & getInt() const
InputLanguage getLanguage(const std::string &lang)
const bool & getBool() const
size_t countFlags(const std::string &name) const
CLFlagType getType() const
Return the type of the flag.
InputLanguage getOutputLang() const
Get the output language for printing.