1
2 /*
3 * File vutil.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 /**
20 * @file vutil.cpp. Implements the main function for running small tools thet use Vampire's infrastructure.
21 */
22
23 #include <iostream>
24
25 #include "Forwards.hpp"
26
27 #include "Debug/Tracer.hpp"
28
29 #include "Lib/Allocator.hpp"
30 #include "Lib/Exception.hpp"
31 #include "Lib/Environment.hpp"
32 #include "Lib/Int.hpp"
33 #include "Lib/Random.hpp"
34 #include "Lib/Stack.hpp"
35 #include "Lib/System.hpp"
36 #include "Lib/VString.hpp"
37
38 #include "Shell/CommandLine.hpp"
39 #include "Shell/Options.hpp"
40 #include "Shell/Statistics.hpp"
41 #include "CASC/CASCMode.hpp"
42
43 #include "VUtils/AnnotationColoring.hpp"
44 #include "VUtils/CPAInterpolator.hpp"
45 #include "VUtils/DPTester.hpp"
46 #include "VUtils/EPRRestoringScanner.hpp"
47 #include "VUtils/FOEquivalenceDiscovery.hpp"
48 #include "VUtils/PreprocessingEvaluator.hpp"
49 #include "VUtils/ProblemColoring.hpp"
50 #include "VUtils/SATReplayer.hpp"
51 #include "VUtils/SimpleSMT.hpp"
52 #include "VUtils/SMTLIBConcat.hpp"
53 #include "VUtils/Z3InterpolantExtractor.hpp"
54
55 using namespace Lib;
56 using namespace Shell;
57 using namespace CASC;
58 using namespace VUtils;
59
60
explainException(Exception & exception)61 void explainException (Exception& exception)
62 {
63 env.beginOutput();
64 exception.cry(env.out());
65 env.endOutput();
66 } // explainException
67
readAndFilterGlobalOpts(Stack<char * > & args)68 void readAndFilterGlobalOpts(Stack<char*>& args) {
69 Stack<char*>::StableDelIterator it(args);
70
71 //skip the first item which is the executable name
72 ALWAYS(it.hasNext());
73 it.next();
74
75 while(it.hasNext()) {
76 vstring arg(it.next());
77 if(arg=="-tr") {
78 it.del();
79 if(!it.hasNext()) {
80 USER_ERROR("value for -tr option expected");
81 }
82 vstring traceStr(it.next());
83 it.del();
84 PROCESS_TRACE_SPEC_STRING(traceStr);
85 }
86 else if(arg=="-m") {
87 it.del();
88 if(!it.hasNext()) {
89 USER_ERROR("value for -m option expected");
90 }
91 vstring memLimitStr = it.next();
92 it.del();
93 unsigned memLimit;
94 if(!Int::stringToUnsignedInt(memLimitStr, memLimit)) {
95 USER_ERROR("unsigned number expected as value of -m option");
96 }
97 env.options->setMemoryLimit(memLimit);
98 Allocator::setMemoryLimit(env.options->memoryLimit()*1048576ul);
99 }
100 else {
101 break;
102 }
103 }
104 }
105
106 /**
107 * The main function.
108 */
main(int argc,char * argv[])109 int main(int argc, char* argv [])
110 {
111 CALL ("main");
112
113 int resultValue=2;
114
115 System::registerArgv0(argv[0]);
116 System::setSignalHandlers();
117 // create random seed for the random number generation
118 Lib::Random::setSeed(123456);
119
120 Stack<char*> args;
121 args.loadFromIterator(getArrayishObjectIterator(argv, argc));
122
123 try {
124 env.options->setMode(Options::MODE_VAMPIRE);
125 env.options->setTimeLimitInDeciseconds(0);
126
127 Allocator::setMemoryLimit(1024u*1048576ul);
128
129 readAndFilterGlobalOpts(args);
130
131 if(args.size()<2) {
132 USER_ERROR("missing name of the vutil module to be run (vutil requires at least one command line argument)");
133 }
134 vstring module=args[1];
135 if(module=="problem_coloring") {
136 resultValue=ProblemColoring().perform(args.size(), args.begin());
137 }
138 else if(module=="conjecture_coloring" || module=="axiom_coloring") {
139 resultValue=AnnotationColoring().perform(args.size(), args.begin());
140 }
141 else if(module=="zie") {
142 resultValue=ZIE().perform(args.size(), args.begin());
143 }
144 else if(module=="epr_restoring_scanner") {
145 resultValue=EPRRestoringScanner().perform(args.size(), args.begin());
146 }
147 else if(module=="fed") {
148 resultValue=FOEquivalenceDiscovery().perform(args.size(), args.begin());
149 }
150 else if(module=="sc") {
151 resultValue=SMTLIBConcat().perform(args.size(), args.begin());
152 }
153 else if(module=="cpa") {
154 resultValue=CPAInterpolator().perform(args.size(), args.begin());
155 }
156 else if(module=="pe") {
157 resultValue=PreprocessingEvaluator().perform(args.size(), args.begin());
158 }
159 else if(module=="smt") {
160 resultValue=SimpleSMT().perform(args.size(), args.begin());
161
162 }
163 else if(module=="dpt") {
164 resultValue=DPTester().perform(args.size(), args.begin());
165 }
166 else if(module=="sr") {
167 resultValue=SATReplayer().perform(args.size(), args.begin());
168 }
169 else if(module=="vamp_casc") {
170 Shell::CommandLine cl(args.size()-1, args.begin()+1);
171 cl.interpret(*env.options);
172 Allocator::setMemoryLimit(env.options->memoryLimit()*1048576ul);
173 Lib::Random::setSeed(env.options->randomSeed());
174 if(CASC::CASCMode::perform(args.size()-1, args.begin()+1)) {
175 //casc mode succeeded in solving the problem, so we return zero
176 resultValue = VAMP_RESULT_STATUS_SUCCESS;
177 }
178 }
179 else {
180 USER_ERROR("unknown vutil module name: "+module);
181 }
182 }
183 #if VDEBUG
184 catch (Debug::AssertionViolationException& exception) {
185 reportSpiderFail();
186 }
187 #endif
188 catch (UserErrorException& exception) {
189 reportSpiderFail();
190 explainException(exception);
191 }
192 catch (Exception& exception) {
193 reportSpiderFail();
194 env.beginOutput();
195 explainException(exception);
196 env.statistics->print(env.out());
197 env.endOutput();
198 }
199 catch (std::bad_alloc& _) {
200 reportSpiderFail();
201 env.beginOutput();
202 env.out() << "Insufficient system memory" << '\n';
203 env.endOutput();
204 }
205 // delete env.allocator;
206
207 return resultValue;
208 } // main
209
210