1/******************************************************************************************[Main.C]
2MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
3
4Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
5associated documentation files (the "Software"), to deal in the Software without restriction,
6including without limitation the rights to use, copy, modify, merge, publish, distribute,
7sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
8furnished to do so, subject to the following conditions:
9
10The above copyright notice and this permission notice shall be included in all copies or
11substantial portions of the Software.
12
13THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
14NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
15NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
16DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
17OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
18**************************************************************************************************/
19
20#include "Solver.h"
21#include <ctime>
22#include <unistd.h>
23#include <signal.h>
24#include <iostream>
25#include <fstream>
26
27//=================================================================================================
28// DIMACS Parser: // Inserts problem into solver.
29
30using namespace std;
31
32void addLit(int parsed_lit,Solver& S, vec<Lit>& lits) {
33  int var = abs(parsed_lit)-1;
34  while (var >= S.nVars()) S.newVar();
35  lits.push( (parsed_lit > 0) ? Lit(var) : ~Lit(var) );
36}
37
38void addClause(Solver& S, vec<Lit>& lits) {
39  /*for (int i=0;i<lits.size();i++)
40    cout << (sign(lits[i]) ? "-" : "") << (var(lits[i])+1) << " ";
41    cout << "#" << endl;*/
42  S.addClause(lits);
43  lits.clear();
44}
45
46static void parse_DIMACS(char* filename, Solver& S) {
47  ifstream fin(filename);
48  if (fin.fail()) { cerr << "Error opening input file " << filename << endl; exit(1); }
49  string line,stok;
50  int itok;
51  vec<Lit> lits;
52  while(true) { // skip preamble (must have at least the p line)
53    fin >> stok;
54    if (stok=="c" || stok=="p") getline(fin,line);
55    else break;
56  }
57  addLit(atoi(stok.c_str()),S,lits); // first lit of first clause
58  while (true) {
59    fin >> itok;
60    if (fin.eof()) {
61      if (lits.size()>0) addClause(S,lits); // in case last clause had no trailing 0
62      break;
63    }
64    if (itok==0) addClause(S,lits);
65    else addLit(itok,S,lits);
66  }
67}
68//=================================================================================================
69
70
71void printStats(SolverStats& stats, double& cpu_time, int64& mem_used)
72{
73    cpu_time = cpuTime();
74    mem_used = memUsed();
75    reportf("restarts              : %"I64_fmt"\n", stats.starts);
76    reportf("conflicts             : %-12"I64_fmt"   (%.0f /sec)\n", stats.conflicts   , stats.conflicts   /cpu_time);
77    reportf("decisions             : %-12"I64_fmt"   (%.0f /sec)\n", stats.decisions   , stats.decisions   /cpu_time);
78    reportf("propagations          : %-12"I64_fmt"   (%.0f /sec)\n", stats.propagations, stats.propagations/cpu_time);
79    reportf("conflict literals     : %-12"I64_fmt"   (%4.2f %% deleted)\n", stats.tot_literals, (stats.max_literals - stats.tot_literals)*100 / (double)stats.max_literals);
80    if (mem_used != 0) reportf("Memory used           : %.2f MB\n", mem_used / 1048576.0);
81    reportf("CPU time              : %g s\n", cpu_time);
82}
83
84void printProofStats(double cpu_time, int64 mem_used) {
85      double  cpu_time1 = cpuTime();
86      int64   mem_used1 = memUsed();
87      if (mem_used1!= 0) reportf("Extra memory used     : %.2f MB\n",
88				 (mem_used1-mem_used)/1048576.0);
89      reportf("Extra CPU time        : %g s\n", (cpu_time1-cpu_time));
90}
91
92Solver* solver;
93static void SIGINT_handler(int signum) {
94    reportf("\n"); reportf("*** INTERRUPTED ***\n");
95    double cpu_time = 0;
96    int64 mem_used = 0;
97    printStats(solver->stats,cpu_time,mem_used);
98    reportf("\n"); reportf("*** INTERRUPTED ***\n");
99    exit(1); }
100
101
102//=================================================================================================
103// Simplistic proof-checker -- just to illustrate the use of 'ProofTraverser':
104
105
106#include "Sort.h"
107
108static void resolve(vec<Lit>& main, vec<Lit>& other, Var x)
109{
110    Lit     p;
111    bool    ok1 = false, ok2 = false;
112    for (int i = 0; i < main.size(); i++){
113        if (var(main[i]) == x){
114            ok1 = true, p = main[i];
115            main[i] = main.last();
116            main.pop();
117            break;
118        }
119    }
120
121    for (int i = 0; i < other.size(); i++){
122        if (var(other[i]) != x)
123            main.push(other[i]);
124        else{
125            if (p != ~other[i])
126                printf("PROOF ERROR! Resolved on variable with SAME polarity in both clauses: %d\n", x+1);
127            ok2 = true;
128        }
129    }
130
131    if (!ok1 || !ok2)
132        printf("PROOF ERROR! Resolved on missing variable: %d\n", x+1);
133
134    sortUnique(main);
135}
136
137
138struct Checker : public ProofTraverser {
139    vec<vec<Lit> >  clauses;
140
141    void root   (const vec<Lit>& c) {
142        //**/printf("%d: ROOT", clauses.size());
143        //for (int i = 0; i < c.size(); i++)
144        //   printf(" %s%d", sign(c[i])?"-":"", var(c[i])+1);
145        //printf("\n");
146        clauses.push();
147        c.copyTo(clauses.last()); }
148
149    void chain  (const vec<ClauseId>& cs, const vec<Var>& xs) {
150        //**/printf("%d: CHAIN %d", clauses.size(), cs[0]-1);
151        //for (int i = 0; i < xs.size(); i++) printf(" [%d] %d", (xs[i]>>1)+1, cs[i+1]-1);
152        clauses.push();
153        vec<Lit>& c = clauses.last();
154
155	//HA: the -1 to compensate for id_counter base 1
156	//HA: the >> 1 to drop sign info from vars
157        clauses[cs[0]-1].copyTo(c);
158        for (int i = 0; i < xs.size(); i++)
159	  resolve(c, clauses[cs[i+1]-1], xs[i] >> 1);
160        //**/printf(" =>"); for (int i = 0; i < c.size(); i++)
161	//  printf(" %s%d", sign(c[i])?"-":"", var(c[i])+1); printf("\n");
162        }
163
164    void deleted(ClauseId c) {
165        clauses[c].clear(); }
166};
167
168
169//HA: called with no second arg, so goal gets default value
170void checkProof(Proof* proof, ClauseId goal = ClauseId_NULL)
171{
172    Checker trav;
173    int res_count = 0;
174    proof->traverse(trav, res_count, goal);
175    printf("%d resolution steps.\n",res_count);
176    vec<Lit>& c = trav.clauses.last();
177    printf("Final clause:");
178    if (c.size() == 0)
179        printf(" <empty>\n");
180    else{
181        for (int i = 0; i < c.size(); i++)
182            printf(" %s%d", sign(c[i])?"-":"", var(c[i])+1);
183        printf("\n");
184    }
185}
186
187
188//=================================================================================================
189// Main:
190
191
192static const char* doc =
193    "USAGE: minisat <input-file> [options]\n"
194    "  -r <result file>   Write result (the word \"SAT\" plus model, or just \"UNSAT\") to file.\n"
195    "  -p <proof trace>   Write the trace to this file.\n"
196    "  -c                 Check the trace by simple (read \"slow\") proof checker.\n"
197    "  -x                 Extract proof from trace.\n"
198;
199
200int main(int argc, char** argv)
201{
202    char*       input  = NULL;
203    char*       result = NULL;
204    char*       proof  = NULL;
205    bool        check  = false;
206    bool        compress = false;
207
208    // Parse options:
209    //
210    for (int i = 1; i < argc; i++){
211        if (argv[i][0] != '-'){
212            if (input != NULL)
213                fprintf(stderr, "ERROR! Only one input file may be specified.\n"), exit(1);
214            input = argv[i];
215        }else{
216            switch (argv[i][1]){
217            case 'r':
218                i++; if (i >= argc) fprintf(stderr, "ERROR! Missing filename after '-r' option.\n");
219                result = argv[i];
220                break;
221            case 'p':
222                i++; if (i >= argc) fprintf(stderr, "ERROR! Missing filename after '-p' option.\n");
223                proof = argv[i];
224                break;
225            case 'c':
226                check = true;
227                break;
228            case 'x':
229	        compress = true;
230                break;
231            case 'h':
232                reportf("%s", doc);
233                exit(0);
234            default:
235                fprintf(stderr, "ERROR! Invalid option: %s\n", argv[i]), exit(1);
236            }
237        }
238    }
239
240    // Parse input and perform SAT:
241    //
242    Solver      S;
243    if (proof != NULL || check) S.proof = new Proof();
244    if (input == NULL) { fprintf(stderr, "ERROR! Input file not specified"); exit(1); }
245    parse_DIMACS(input, S);
246
247    FILE*   res = (result != NULL) ? fopen(result, "wb") : NULL;
248
249    if (!S.okay()){
250        if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
251        if (S.proof != NULL && proof != NULL) S.proof->save(proof);
252        if (S.proof != NULL && check) printf("Checking proof...\n"), checkProof(S.proof);
253        reportf("Trivial problem\n");
254        reportf("UNSATISFIABLE\n");
255        exit(20);
256    }
257
258    S.verbosity = 1;
259    solver = &S;
260    signal(SIGINT,SIGINT_handler);
261    signal(SIGHUP,SIGINT_handler);
262
263    S.solve();
264
265    double cpu_time = 0; int64 mem_used = 0;
266    printStats(S.stats,cpu_time,mem_used);
267    reportf("\n");
268    reportf(S.okay() ? "SATISFIABLE\n" : "UNSATISFIABLE\n");
269
270    if (res != NULL){
271        if (S.okay()){
272            fprintf(res, "SAT\n");
273            for (int i = 0; i < S.nVars(); i++)
274                if (S.model[i] != l_Undef)
275                    fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1);
276            fprintf(res, " 0\n");
277        }else
278            fprintf(res, "UNSAT\n");
279        fclose(res);
280    }
281
282    // Post-processing of proof in case of UNSAT
283    if (S.proof != NULL && !S.okay()){
284      if (compress) { // ...compress, and possibly check
285	reportf("Compressing proof...\n");
286	Proof compressed;
287	S.proof->compress(compressed,S.proof->last());
288	if (check)
289	  reportf("Checking compressed proof...\n"),
290	    checkProof(&compressed);
291	if (proof != NULL) compressed.save(proof);
292	printProofStats(cpu_time,mem_used);
293      } else if (check) { // ...check
294	reportf("Checking proof...\n"),
295	  checkProof(S.proof);
296	if (proof != NULL) S.proof->save(proof);
297	printProofStats(cpu_time,mem_used);
298      } else if (proof != NULL) S.proof->save(proof);
299    }
300
301    // (faster than "return", which will invoke the destructor for 'Solver')
302    exit(S.okay() ? 10 : 20);
303
304}
305