-
Notifications
You must be signed in to change notification settings - Fork 1
/
main.cpp
66 lines (55 loc) · 1.31 KB
/
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
#include <iostream>
#include <stdio.h>
#include <stdlib.h>
#include <vector>
#include <cmath>
#include <string>
#include <sstream>
#include <string.h>
using namespace std;
#define DEBUG 0
#define GLOBAL_CUTOFF 200
void invariant(bool inv, int num) {
if (!inv) {
cerr << "Invariant failed " << num << endl;
throw num;
}
}
#include "model.cpp"
#include "literal.cpp"
#include "clause.cpp"
#include "formula.cpp"
#include "parser.cpp"
#include "solver.cpp"
int main(int argc, char **argv) {
if (argc != 2) {
cerr << "usage: saturday <filename>" << endl;
return 1;
}
// Get file pointer for <filename>.
char *fname = argv[1];
FILE *file = Parser::open(fname);
if (file == NULL) {
cerr << "File '" << fname << "' failed to open!" << endl;
return 1;
}
// Parse the file.
Formula *formula = Parser::parse(file);
fclose(file);
if (DEBUG >= 5)
cout << formula->toString();
// // model testing code
// Model *testModel = new Model(5);
// testModel->setVar(1);
// testModel->setVar(2);
// testModel->clearVar(2);
// cout << testModel->toString() << endl;
Model *model = Solver::solve(formula);
if (model == NULL) {
cout << "s UNSATISFIABLE" << endl;
} else {
cout << "s SATISFIABLE" << endl;
cout << "v " << model->toString() << endl;
}
return 0;
}