1
2 /*
3 * File vsat.cpp.
4 *
5 * This file is part of the source code of the software program
6 * Vampire. It is protected by applicable
7 * copyright laws.
8 *
9 * This source code is distributed under the licence found here
10 * https://vprover.github.io/license.html
11 * and in the source directory
12 *
13 * In summary, you are allowed to use Vampire for non-commercial
14 * purposes but not allowed to distribute, modify, copy, create derivatives,
15 * or use in competitions.
16 * For other uses of Vampire please contact developers for a different
17 * licence, which we will make an effort to provide.
18 */
19 #include <iostream>
20
21 #include "Forwards.hpp"
22
23 #include "Debug/Assertion.hpp"
24
25 #include "Lib/Allocator.hpp"
26 #include "Lib/Environment.hpp"
27 #include "Lib/Random.hpp"
28 #include "Lib/Stack.hpp"
29 #include "Lib/System.hpp"
30 #include "Lib/Timer.hpp"
31 #include "Lib/VirtualIterator.hpp"
32 #include "Lib/Int.hpp"
33
34 #include "SAT/DIMACS.hpp"
35 #include "SAT/MinimizingSolver.hpp"
36 #include "SAT/Preprocess.hpp"
37 #include "SAT/SingleWatchSAT.hpp"
38 #include "SAT/TWLSolver.hpp"
39
40 #include "Indexing/TermSharing.hpp"
41
42 #include "Shell/CommandLine.hpp"
43 #include "Shell/Options.hpp"
44 #include "Shell/Statistics.hpp"
45
46 #include "Test/CheckedSatSolver.hpp"
47
48 using namespace Lib;
49 using namespace SAT;
50 using namespace Shell;
51 using namespace Test;
52 using namespace std;
53
54 struct SatOptions
55 {
56 bool simulateIncremental;
57 bool minimizingSolver;
58 bool checkingSolver;
59 vstring fileName;
60
SatOptionsSatOptions61 SatOptions()
62 : simulateIncremental(false),
63 minimizingSolver(false),
64 checkingSolver(false)
65 {}
66 };
67
68
69
getInputClauses(const char * fname,unsigned & varCnt)70 SATClauseList* getInputClauses(const char* fname, unsigned& varCnt)
71 {
72 CALL("getInputClauses");
73
74 SATClauseIterator cit=Preprocess::removeDuplicateLiterals( DIMACS::parse(fname, varCnt) );
75
76 SATClauseList* clauses = 0;
77 SATClauseList::pushFromIterator(cit, clauses);
78 return clauses;
79 }
80
preprocessClauses(unsigned varCnt,SATClauseList * & clauses)81 void preprocessClauses(unsigned varCnt, SATClauseList*& clauses)
82 {
83 CALL("preprocessClauses");
84
85 Preprocess::filterPureLiterals(varCnt, clauses);
86 // SATClauseIterator cl = pvi( SATClauseList::DestructiveIterator(clauses));
87 // SATClauseIterator units, nonUnits;
88 // Preprocess::propagateUnits(cl, units, nonUnits);
89 // clauses = 0;
90 // SATClauseList::pushFromIterator(nonUnits, clauses);
91 }
92
getPreprocessedClauses(const char * fname,unsigned & varCnt)93 SATClauseList* getPreprocessedClauses(const char* fname, unsigned& varCnt)
94 {
95 CALL("getPreprocessedClauses");
96
97 SATClauseList* clauses = getInputClauses(fname, varCnt);
98 preprocessClauses(varCnt, clauses);
99 return clauses;
100 }
101
102
runSolverIncrementally(SATSolver & solver,unsigned varCnt,SATClauseList * clauses)103 SATSolver::Status runSolverIncrementally(SATSolver& solver, unsigned varCnt, SATClauseList* clauses)
104 {
105 CALL("runSolverIncrementally");
106
107 bool testAssumptions = true;
108
109 Stack<SATClause*> cls;
110 cls.loadFromIterator(SATClauseList::Iterator(clauses));
111
112 solver.ensureVarCnt(varCnt);
113
114 SATSolver::Status solverStatus = SATSolver::SATISFIABLE;
115
116 SATClauseStack units;
117 SATClauseStack inner;
118
119 while(cls.isNonEmpty()) {
120 units.reset();
121 inner.reset();
122 unsigned currCnt= (cls.size()>1) ? (Random::getInteger(cls.size()-1)+1) : 1;
123 while(currCnt--) {
124 SATClause* cl = cls.pop();
125 if(cl->length()==1) {
126 units.push(cl);
127 }
128 else {
129 inner.push(cl);
130 }
131 }
132
133 SATClauseIterator ic1=pvi( Stack<SATClause*>::Iterator(inner) );
134 solver.addClauses(ic1);
135
136 solverStatus = solver.getStatus();
137 if(solverStatus!=SATSolver::SATISFIABLE) {
138 return solverStatus;
139 }
140
141 if(testAssumptions) {
142
143 //first we try adding wrong literals, so that we check retracting works as it should...
144 SATClauseStack::Iterator uit0(units);
145 while(uit0.hasNext()) {
146 SATClause* cl = uit0.next();
147 solver.addAssumption((*cl)[0].opposite());
148 }
149 //solver.retractAllAssumptions();
150
151 SATClauseStack::Iterator uit(units);
152 while(uit.hasNext()) {
153 SATClause* cl = uit.next();
154 solver.addAssumption((*cl)[0]);
155
156 solverStatus = solver.getStatus();
157 if(solverStatus!=SATSolver::SATISFIABLE) { return solverStatus; }
158 }
159 //solver.retractAllAssumptions();
160 }
161
162 while(units.isNonEmpty()) {
163 SATClause* cl = units.pop();
164 solver.addClauses(pvi( getSingletonIterator(cl) ));
165
166 ASS_EQ(solver.getStatus(), SATSolver::SATISFIABLE);
167 }
168 }
169
170 ASS_EQ(solverStatus, SATSolver::SATISFIABLE);
171 return SATSolver::SATISFIABLE;
172 }
173
174
runSolver(SATSolver & solver,unsigned varCnt,SATClauseList * clauses)175 SATSolver::Status runSolver(SATSolver& solver, unsigned varCnt, SATClauseList* clauses)
176 {
177 CALL("runSolver");
178
179 /*solver.ensureVarCnt(varCnt);
180 solver.addClauses(pvi( SATClauseList::Iterator(clauses)));
181 return solver.getStatus();
182 */
183 solver.addClauses(pvi(SATClauseList::Iterator(clauses)));
184 return solver.getStatus();
185 }
186
satSolverMode(SatOptions & opts)187 void satSolverMode(SatOptions& opts)
188 {
189 CALL("satSolverMode");
190
191 env.statistics->phase = Statistics::PARSING;
192 unsigned varCnt;
193 SATClauseList* clauses;
194
195 if(opts.fileName.empty()) {
196 clauses = getInputClauses(0,varCnt);
197 //clauses = getPreprocessedClauses(0, varCnt);
198 }
199 else {
200 clauses = getInputClauses(opts.fileName.c_str(), varCnt);
201 //clauses = getPreprocessedClauses(opts.fileName.c_str(), varCnt);
202 }
203
204 env.statistics->phase = Statistics::SAT_SOLVING;
205
206 cout<<"start varcnt :"<<varCnt<<"\n";
207
208 SATSolverSCP solver(new TWLSolver(*env.options, true));
209 //for the minimized case
210 //solver = new MinimizingSolver(solver.release());
211
212 /*if(opts.minimizingSolver) {
213 solver = new MinimizingSolver(solver.release());
214 }
215 if(opts.checkingSolver) {
216 solver = new CheckedSatSolver(solver.release());
217 }
218 */
219
220 SATSolver::Status res;
221 if(opts.simulateIncremental) {
222 res = runSolverIncrementally(*solver, varCnt, clauses);
223 }
224 else {
225 res = runSolver(*solver, varCnt, clauses);
226 }
227
228 env.statistics->phase = Statistics::FINALIZATION;
229
230 switch(res) {
231 case SATSolver::SATISFIABLE:
232 cout<<"SATISFIABLE\n";
233 env.statistics->terminationReason = Statistics::SATISFIABLE;
234 break;
235 case SATSolver::UNSATISFIABLE:
236 cout<<"UNSATISFIABLE\n";
237 env.statistics->terminationReason = Statistics::REFUTATION;
238 break;
239 case SATSolver::UNKNOWN:
240 cout<<"Unknown\n";
241 break;
242 default:
243 cout<<res<<endl;
244 ASSERTION_VIOLATION;
245 }
246
247 //clauses->destroy();
248 }
249
processArgs(StringStack & args,SatOptions & opts)250 bool processArgs(StringStack& args, SatOptions& opts)
251 {
252 CALL("processArgs");
253 bool flag=true;
254 StringStack::StableDelIterator it(args);
255 while(it.hasNext()) {
256 vstring arg = it.next();
257 if(arg=="-incr") {
258 opts.simulateIncremental = true;
259 it.del();
260 }
261 else if(arg=="-minim") {
262 opts.minimizingSolver = true;
263 it.del();
264 }
265 else if(arg=="-checked") {
266 opts.checkingSolver = true;
267 it.del();
268 }
269 else if(arg=="-tr") {
270 it.del();
271 if(!it.hasNext()) {
272 USER_ERROR("value for -tr option expected");
273 }
274 vstring traceStr(it.next());
275 it.del();
276 PROCESS_TRACE_SPEC_STRING(traceStr);
277 }
278 else if(arg == "-t"){
279 it.del();
280 if(!it.hasNext()){
281 USER_ERROR("value for -t option expected");
282 }
283 vstring timelimit(it.next());
284 it.del();
285 int timeout;
286 Lib::Int::stringToInt(timelimit, timeout);
287
288 env.options->setTimeLimitInSeconds(timeout);
289 flag=false;
290 }
291 }
292 if(args.size()>1) {
293 while(args.isNonEmpty()) {
294 cout<<args.pop()<<endl;
295 }
296 USER_ERROR("too many arguments");
297 }
298 if(args.isNonEmpty()) {
299 opts.fileName = args.pop();
300 }
301 return flag;
302 }
303
main(int argc,char * argv[])304 int main(int argc, char* argv [])
305 {
306 CALL("main");
307 //ScopedPtr<SATSolver> solver;
308
309 try {
310 System::registerArgv0(argv[0]);
311 Random::setSeed(1);
312 Options options;
313 Allocator::setMemoryLimit(env.options->memoryLimit()*1048576);
314
315 StringStack args;
316 System::readCmdArgs(argc, argv, args);
317
318 SatOptions opts;
319 if (processArgs(args, opts)){
320 env.options->setTimeLimitInDeciseconds(3600);
321 }
322
323 Lib::Random::setSeed(env.options->randomSeed());
324
325 satSolverMode(opts);
326 }
327 catch(MemoryLimitExceededException&)
328 {
329 cerr<<"Memory limit exceeded\n";
330 env.statistics->terminationReason = Statistics::MEMORY_LIMIT;
331 cout<<"-MEMORY_LIMIT\n";
332 }
333 catch(TimeLimitExceededException&)
334 {
335 env.statistics->terminationReason = Statistics::TIME_LIMIT;
336 cout<<"TIME LIMIT\n";
337 }
338 catch(UserErrorException& e)
339 {
340
341 cout<<"USER ERROR: ";
342 e.cry(cout);
343 cout<<"\n";
344 }
345
346 env.statistics->print(cout);
347
348 return 0;
349 }
350
351