1
2 /*
3 * File MainLoop.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 MainLoop.cpp
21 * Implements class MainLoop.
22 */
23
24
25 #include "Lib/Environment.hpp"
26 #include "Lib/SmartPtr.hpp"
27 #include "Lib/System.hpp"
28
29 #include "Inferences/InferenceEngine.hpp"
30 #include "Inferences/TermAlgebraReasoning.hpp"
31 #include "Inferences/TautologyDeletionISE.hpp"
32
33 #include "InstGen/IGAlgorithm.hpp"
34
35 #include "Saturation/SaturationAlgorithm.hpp"
36
37 #include "FMB/FiniteModelBuilder.hpp"
38
39 #include "SAT/Z3MainLoop.hpp"
40
41 #include "Shell/BFNTMainLoop.hpp"
42 #include "Shell/Options.hpp"
43 #include "Shell/UIHelper.hpp"
44
45 #include "Signature.hpp"
46 #include "Clause.hpp"
47 #include "Problem.hpp"
48
49 #include "MainLoop.hpp"
50
51 using namespace Kernel;
52 using namespace InstGen;
53 using namespace Saturation;
54 using namespace FMB;
55
updateStatistics()56 void MainLoopResult::updateStatistics()
57 {
58 CALL("MainLoopResult::updateStatistics");
59
60 env.statistics->terminationReason = terminationReason;
61 env.statistics->refutation = refutation;
62 env.statistics->saturatedSet = saturatedSet;
63 if(refutation) {
64 env.statistics->maxInductionDepth = refutation->inference().inductionDepth();
65 }
66 }
67
68 /**
69 * Run the solving algorithm
70 */
run()71 MainLoopResult MainLoop::run()
72 {
73 CALL("MainLoop::run");
74
75 try {
76 init();
77 return runImpl();
78 }
79 catch(RefutationFoundException& rs)
80 {
81 return MainLoopResult(Statistics::REFUTATION, rs.refutation);
82 }
83 catch(TimeLimitExceededException&)
84 {
85 return MainLoopResult(Statistics::TIME_LIMIT);
86 }
87 catch(ActivationLimitExceededException&)
88 {
89 return MainLoopResult(Statistics::ACTIVATION_LIMIT);
90 }
91 catch(MainLoopFinishedException& e)
92 {
93 return e.result;
94 }
95 }
96
97 /**
98 * Return true iff clause @b c is refutation clause.
99 *
100 * Deriving a refutation clause means that the saturation algorithm can
101 * terminate with success.
102 */
isRefutation(Clause * cl)103 bool MainLoop::isRefutation(Clause* cl)
104 {
105 CALL("MainLoop::isRefutation");
106
107 return cl->isEmpty() && cl->noSplits();
108 }
109
createFromOptions(Problem & prb,const Options & opt)110 MainLoop* MainLoop::createFromOptions(Problem& prb, const Options& opt)
111 {
112 CALL("MainLoop::createFromOptions");
113
114 if(opt.bfnt()) {
115 return new BFNTMainLoop(prb, opt);
116 }
117
118 #if VZ3
119 bool isComplete = false; // artificially prevent smtForGround from running
120
121 if(isComplete && opt.smtForGround() && prb.getProperty()->allNonTheoryClausesGround()
122 && prb.getProperty()->hasInterpretedOperations()){
123 return new SAT::Z3MainLoop(prb,opt);
124 }
125 #endif
126
127 MainLoop* res;
128
129 switch (opt.saturationAlgorithm()) {
130 case Options::SaturationAlgorithm::INST_GEN:
131 res = new IGAlgorithm(prb, opt);
132 break;
133 case Options::SaturationAlgorithm::FINITE_MODEL_BUILDING:
134 res = new FiniteModelBuilder(prb,opt);
135 break;
136 #if VZ3
137 case Options::SaturationAlgorithm::Z3:
138 if(!isComplete || !prb.getProperty()->allNonTheoryClausesGround()){
139 reportSpiderStatus('u');
140 USER_ERROR("Z3 saturation algorithm is only appropriate where preprocessing produces a ground problem");
141 //TODO should return inappropriate result instead of error
142 }
143 res = new SAT::Z3MainLoop(prb,opt);
144 break;
145 #endif
146 default:
147 res = SaturationAlgorithm::createFromOptions(prb, opt);
148 break;
149 }
150
151 return res;
152 }
153
154