1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
/********************* -*- C++ -*- */
/** main.cpp
** This file is part of the CVC4 prototype.
** Copyright (c) 2009 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.
**
** [[ Add file-specific comments here ]]
**/
#include <cstdio>
#include <cstdlib>
#include <cerrno>
#include <new>
#include <exception>
#include <unistd.h>
#include <string.h>
#include <stdint.h>
#include <time.h>
#include "config.h"
#include "main.h"
#include "usage.h"
using namespace std;
using namespace CVC4;
using namespace CVC4::main;
int main(int argc, char *argv[]) {
struct Options opts;
try {
cvc4_init();
int firstArgIndex = parseOptions(argc, argv, &opts);
FILE *infile;
if(firstArgIndex >= argc) {
infile = stdin;
} else if(argc > firstArgIndex + 1) {
throw new Exception("Too many input files specified.");
} else {
infile = fopen(argv[firstArgIndex], "r");
if(!infile) {
throw new Exception(string("Could not open input file `") + argv[firstArgIndex] + "' for reading: " + strerror(errno));
exit(1);
}
// ExprManager *exprMgr = ...;
// SmtEngine smt(exprMgr, &opts);
// Parser parser(infile, exprMgr, &opts);
// while(!parser.done) {
// Command *cmd = parser.get();
// cmd->invoke(smt);
// delete cmd;
// }
}
} catch(CVC4::main::OptionException* e) {
if(opts.smtcomp_mode) {
printf("unknown");
fflush(stdout);
}
fprintf(stderr, "CVC4 Error:\n%s\n\n", e->toString().c_str());
printf(usage, opts.binary_name.c_str());
exit(1);
} catch(CVC4::Exception* e) {
if(opts.smtcomp_mode) {
printf("unknown");
fflush(stdout);
}
fprintf(stderr, "CVC4 Error:\n%s\n", e->toString().c_str());
exit(1);
} catch(bad_alloc) {
if(opts.smtcomp_mode) {
printf("unknown");
fflush(stdout);
}
fprintf(stderr, "CVC4 ran out of memory.\n");
exit(1);
} catch(...) {
fprintf(stderr, "CVC4 threw an exception of unknown type.\n");
exit(1);
}
return 0;
}
|