CVC3  2.4.1
main.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file main.cpp
4  * \brief Main program for cvc3
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Wed Dec 4 17:21:10 2002
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #include <signal.h>
23 #include <fstream>
24 #include <iomanip>
25 
26 #include "os.h"
27 #include "vc.h"
28 #include "parser.h"
29 #include "vc_cmd.h"
30 #include "command_line_flags.h"
31 #include "statistics.h"
32 
33 #ifdef _MSC_VER
34 #include <windows.h>
35 #else
36 #include <unistd.h>
37 #endif
38 
39 
40 using namespace std;
41 using namespace CVC3;
42 
43 
44 static void parse_args(int argc, char **argv, CLFlags &flags,
45  string& fileName);
46 static void printUsage(const CLFlags& flags, bool followDisplay);
47 
48 // Our own name
49 static string programName;
50 
51 static ValidityChecker* vc = NULL;
52 IF_DEBUG(static DebugTimer* pRuntime = NULL;)
53 
54 #ifndef _MSC_VER
55 void sighandler(int signum) {
56  cerr << "\nInterrupted by signal " << signum;
57  if(signum == SIGALRM)
58  cerr << " (self-timeout)";
59  cerr << ". " << programName << " is aborting.\n";
60  // Print the debugging info
61  IF_DEBUG(if (pRuntime != NULL) CVC3::debugger.setElapsed(*pRuntime);)
62  IF_DEBUG(debugger.printAll();)
63  if(vc != NULL && vc->getFlags()["stats"].getBool())
64  cout << vc->getStatistics() << endl;
65  if(vc != NULL) {
66  // If deletion causes another signal, don't keep trying.
67  // This is here to ensure that logs are dumped, etc.
68  ValidityChecker* toDelete = vc;
69  vc = NULL;
70  delete toDelete;
71  }
72  abort();
73 }
74 #else
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())
79  cout << vc->getStatistics() << endl;
80  if(vc != NULL) {
81  // If deletion causes another signal, don't keep trying.
82  // This is here to ensure that logs are dumped, etc.
83  ValidityChecker* toDelete = vc;
84  vc = NULL;
85  delete toDelete;
86  }
87  ExitProcess(1);
88 }
89 #endif
90 
91 
92 int main(int argc, char **argv)
93 {
94  CLFlags flags(ValidityChecker::createFlags());
95  programName = string(argv[0]);
96  IF_DEBUG(DebugTimer runtime(CVC3::debugger.timer("total runtime"));)
97  IF_DEBUG(pRuntime = &runtime;)
98 
99 #ifndef _MSC_VER
100  signal(SIGINT, sighandler);
101  signal(SIGTERM, sighandler);
102  signal(SIGQUIT, sighandler);
103  signal(SIGALRM, sighandler);
104  signal(SIGSEGV, sighandler);
105 #endif
106 
107  string fileName("");
108 
109  try {
110  parse_args(argc, argv, flags, fileName);
111  } catch(Exception& e) {
112  cerr << "*** " << e;
113  cerr << "\n\nRun with -help option for usage information." << endl;
114  exit(1);
115  }
116 
117  // In SMT-LIBv2, don't save the model between distinct check-sats
118  // (unless user specifically requested it)
119  if(flags["lang"].getString() != "" &&
120  getLanguage(flags["lang"].getString()) == SMTLIB_V2_LANG &&
121  !flags["internal::userSetNoSaveModel"].getBool()) {
122  flags.setFlag("no-save-model", true);
123  }
124 
125  // Set the timeout, if given in the command line options
126  int timeout = flags["timeout"].getInt();
127  if(timeout > 0) {
128 #ifndef _MSC_VER
129  alarm(timeout);
130 #else
131  // http://msdn2.microsoft.com/en-us/library/ms682453.aspx
132  CreateThread(NULL, 0, thread_timeout, (PVOID)timeout, 0, NULL);
133 #endif
134  }
135 
136  /*
137  * Create and run the validity checker
138  */
139 
140  // Debugging code may throw an exception
141  try {
142  vc = ValidityChecker::create(flags);
143  } catch(Exception& e) {
144  cerr << "*** Fatal exception: " << e << endl;
145  exit(1);
146  }
147 
148  // -h flag sets "help" to false (+h would make it true, but that's
149  // not what the user normally types in).
150  if(!vc->getFlags()["help"].getBool()) {
151  printUsage(vc->getFlags(), true);
152  return 0;
153  }
154  if(!vc->getFlags()["unsupported"].getBool()) {
155  printUsage(vc->getFlags(), false);
156  return 0;
157  }
158 #ifndef VERSION
159 #define VERSION "unknown"
160 #endif
161  // Similarly, -version sets the flag "version" to false
162  if(!vc->getFlags()["version"].getBool()) {
163  cout << "This is CVC3 version " << VERSION
164  IF_DEBUG( << " (debug build)")
165  << "\n\n";
166  cout <<
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"
171  << endl;
172  return 0;
173  }
174 
175  try {
176  // Calling getOutputLang() tests if the output language is
177  // correctly specified; if not, an exception will be thrown
178  InputLanguage outlang = vc->getEM()->getOutputLang();
179  if(outlang == SPASS_LANG &&
180  vc->getFlags()["translate"].getBool() &&
181  !vc->getFlags()["liftITE"].modified()) {
182  // SPASS doesn't support ITE; make sure there are none
183  vc->getFlags().setFlag("liftITE", true);
184  }
185  // Set the timer
186  IF_DEBUG(CVC3::debugger.setCurrentTime(runtime);)
187  // Read the input file
188  vc->loadFile(fileName, vc->getEM()->getInputLang(),
189  flags["interactive"].getBool());
190  } catch(Exception& e) {
191  cerr << "*** Fatal exception: " << e << endl;
192  exit(1);
193  }
194 
195  IF_DEBUG(CVC3::debugger.setElapsed(runtime);)
196 
197  // Print the debugging info
198  IF_DEBUG(debugger.printAll();)
199  // Print statistics
200  if(vc->getFlags()["stats"].getBool()) vc->printStatistics();
201  // Destruct the system
202  TRACE_MSG("delete", "Deleting ValidityChecker [last trace from main.cpp]");
203  try {
204  // The signal handler deletes the vc. If deletion segfaults, we don't
205  // want to try it again.
206  ValidityChecker* toDelete = vc;
207  vc = NULL;
208  delete toDelete;
209  } catch(Exception& e) {
210  cerr << "*** Fatal exception: " << e << endl;
211  exit(1);
212  }
213 
214  return 0;
215 }
216 
217 void printUsage(const CLFlags& flags, bool followDisplay) {
218  cout << "Usage: " << programName << " [options]\n"
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;
232  // Get all the names of options (they all match the empty string)
233  flags.countFlags("", 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;
237  string tpStr; // Print type of the option
238  string pref; // Print + or - in front of the option
239  string name(names[i]); // Print name and optionally the value
240  CLFlagType tp = f.getType();
241  switch(tp) {
242  case CLFLAG_NULL: tpStr = "(null)"; break;
243  case CLFLAG_BOOL:
244  tpStr = "(b)"; pref = (f.getBool())? "+" : "-";
245  break;
246  case CLFLAG_INT:
247  tpStr = "(i)"; pref = "-"; name = name+" "+int2string(f.getInt());
248  break;
249  case CLFLAG_STRING:
250  tpStr = "(s)"; pref = "-"; name = name+" "+f.getString();
251  break;
252  case CLFLAG_STRVEC:
253  tpStr = "(v)"; pref = "-"; name = name;
254  break;
255  default:
256  DebugAssert(false, "printUsage: unknown flag type");
257  }
258  cout << " " << tpStr << " " << pref << setw(25);
259  cout.setf(ios::left);
260  cout << name << " " << f.getHelp() << "\n";
261  }
262  cout << endl;
263 }
264 
265 
266 void parse_args(int argc, char **argv, CLFlags &flags, string& fileName) {
267  /* skip 0'th argument */
268  argv++;
269  argc--;
270  bool seenFileName(false);
271 
272  for( ; argc > 0; argc--, argv++) {
273  if((*argv)[0] == '-' || (*argv)[0] == '+') {
274  // A command-line option
275  vector<string> names;
276  bool val = ((*argv)[0] == '+');
277  size_t n = flags.countFlags((*argv)+1, names);
278  if(n == 0)
279  throw CLException(string(*argv) + " does not match any known option");
280  else if(n > 1) {
281  ostringstream ss;
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";
285  }
286  throw CLException(ss.str());
287  } else {
288  string name = names[0];
289  if(name == "no-save-model") {
290  flags.setFlag("internal::userSetNoSaveModel", true);
291  }
292  // Single match; process the option
293  CLFlagType tp = flags[name].getType();
294  switch(tp) {
295  case CLFLAG_BOOL: flags.setFlag(name, val); break;
296  case CLFLAG_INT:
297  argc--;
298  if(argc <= 0)
299  throw CLException(string(*argv)+" (-"+name
300  +") expects an integer argument.");
301  argv++;
302  // FIXME: test for *argv being an integer string
303  flags.setFlag(name, atoi(*argv));
304  break;
305  case CLFLAG_STRING:
306  argc--;
307  if(argc <= 0)
308  throw CLException(string(*argv)+" (-"+name
309  +") expects a string argument.");
310  argv++;
311  flags.setFlag(name, *argv);
312  break;
313  case CLFLAG_STRVEC:
314  argc--;
315  if(argc <= 0)
316  throw CLException(string(*argv)+" (-"+name
317  +") expects a string argument.");
318  argv++;
319  flags.setFlag(name, pair<string,bool>(*argv,val));
320  break;
321  default:
322  DebugAssert(false, "parse_args: Bad flag type: "+int2string(tp));
323  }
324  }
325  } else if(seenFileName) {
326  throw CLException("More than one file name given: "+fileName
327  +" and "+string(*argv));
328  } else {
329  fileName = string(*argv);
330  seenFileName = true;
331  }
332  }
333 }
for output in SPASS format
Definition: lang.h:49
virtual ExprManager * getEM()=0
Return the ExprManager.
Generic API for a validity checker.
int main(int argc, char **argv)
Definition: main.cpp:92
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.
Definition: lang.h:30
InputLanguage getInputLang() const
Get the input language for printing.
SMT-LIB v2 format.
Definition: lang.h:52
void sighandler(int signum)
Definition: main.cpp:55
CLFlagType
Different types of command line flags.
static void parse_args(int argc, char **argv, CLFlags &flags, string &fileName)
Definition: main.cpp:266
#define DebugAssert(cond, str)
Definition: debug.h:408
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)
Definition: main.cpp:217
#define TRACE_MSG(flag, msg)
Definition: debug.h:414
virtual CLFlags & getFlags() const =0
Return the set of command-line flags.
static ValidityChecker * vc
Definition: main.cpp:51
static int left(int i)
Definition: minisat_heap.h:53
Abstraction over different operating systems.
const std::string & getHelp() const
std::string int2string(int n)
Definition: cvc_util.h:46
#define VERSION
#define IF_DEBUG(code)
Definition: debug.h:406
Generic API for a validity checker.
Definition: vc.h:92
virtual void printStatistics()=0
Print collected statistics to stdout.
const std::string & getString() const
static string programName
Definition: main.cpp:49
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)
Definition: lang.h:61
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.