-
Notifications
You must be signed in to change notification settings - Fork 0
/
main.cpp
63 lines (54 loc) · 1.61 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
#include <iostream>
#include <chrono>
#include "common.h"
#include "DimacsParser.h"
#include "DPLL.h"
// helper function to show a formula
std::string show_formula(const formula& phi) {
std::stringstream ss;
ss << "(and" << std::endl;
for (const auto & clause : phi.clauses) {
ss << " (or";
for (literal l : clause) {
if (POSITIVE(l)) ss << " " << l;
else ss << " (not " << VAR(l) << ")";
}
ss << ")" << std::endl;
}
ss << ")";
return ss.str();
}
// entry
int main(int argc, char **argv) {
if (argc < 2) {
std::cerr << "error: no input files" << std::endl;
return 1;
}
for (int i = 1; i < argc; i++) {
std::string f(argv[i]);
std::cout << f << std::endl;
formula phi = DimacsParser::parse(f);
// std::cout << show_formula(phi) << std::endl;
// timer start
auto start = std::chrono::steady_clock::now();
DPLL solver(phi);
bool sat = solver.check_sat_noncdcl();
model m;
if (sat) {
m = solver.get_model();
}
auto end = std::chrono::steady_clock::now();
// timer end
if (sat) {
std::cout << " sat" << std::endl;
for (const auto &p : m) {
std::cout << " " << p.first << " -> " << p.second << std::endl;
}
} else {
std::cout << " unsat" << std::endl;
}
auto duration = std::chrono::duration<float, std::milli>(end - start);
std::cout << " time: " << duration.count() << " ms" << std::endl;
}
return 0;
}