-
Notifications
You must be signed in to change notification settings - Fork 0
/
sm_main.cpp
71 lines (57 loc) · 1.48 KB
/
sm_main.cpp
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
/*
* File: main.cpp
* Author: yzf
*
* Created on July 10, 2013, 2:17 PM
*/
#include <cstdlib>
#include <cstdio>
#include <assert.h>
#include "Vocabulary.h"
#include "structs.h"
#include "Utils.h"
#include "Formula.h"
#include "Formulas.h"
#include "SMTranslator.h"
#include <iostream>
#include <unistd.h>
#include "CircTranslator.h"
#include "Optimization.h"
using namespace std;
FILE* fout;
extern FILE* yyin;
extern _formula* gformula;
extern int yyparse();
void io(const char* iPathName, const char* oPathName) {
yyin = fopen (iPathName, "r");
fout = fopen (oPathName, "w+");
if (! yyin) {
printf("IO Error: cannot open the input file.\n" );
assert(0);
}
if (! fout) {
printf("IO Error: cannot open the output file.\n");
assert(0);
}
}
int main(int argc, char** argv) {
if(argc < 3) {
io("res/input/sample.in","res/output/sample.out");
}
else {
io(argv[1], argv[2]);
}
yyparse();
fclose(yyin);
Formula f = Formula(gformula, false);
SMTranslator::instance().init(f);
SMTranslator::instance().convert();
SMTranslator::instance().outputOriginalFormulas(stdout);
SMTranslator::instance().outputHengZhangFormulas(stdout);
SMTranslator::instance().outputCabalarFormulas(stdout);
SMTranslator::instance().outputFinalResult(fout);
SMTranslator::instance().destroy();
fclose(fout);
Vocabulary::instance().dumpVocabulary(stdout);
return 0;
}