1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Kshitij Bansal, Andrew Reynolds, Morgan Deters |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* An additional layer between commands and invoking them. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "main/command_executor.h" |
17 |
|
|
18 |
|
#ifndef __WIN32__ |
19 |
|
# include <sys/resource.h> |
20 |
|
#endif /* ! __WIN32__ */ |
21 |
|
|
22 |
|
#include <iomanip> |
23 |
|
#include <iostream> |
24 |
|
#include <memory> |
25 |
|
#include <string> |
26 |
|
#include <vector> |
27 |
|
|
28 |
|
#include "main/main.h" |
29 |
|
#include "smt/command.h" |
30 |
|
#include "smt/solver_engine.h" |
31 |
|
|
32 |
|
namespace cvc5 { |
33 |
|
namespace main { |
34 |
|
|
35 |
|
// Function to cancel any (externally-imposed) limit on CPU time. |
36 |
|
// This is used for competitions while a solution (proof or model) |
37 |
|
// is being dumped (so that we don't give "sat" or "unsat" then get |
38 |
|
// interrupted partway through outputting a proof!). |
39 |
|
void setNoLimitCPU() { |
40 |
|
// Windows doesn't have these things, just ignore |
41 |
|
#ifndef __WIN32__ |
42 |
|
struct rlimit rlc; |
43 |
|
int st = getrlimit(RLIMIT_CPU, &rlc); |
44 |
|
if(st == 0) { |
45 |
|
rlc.rlim_cur = rlc.rlim_max; |
46 |
|
setrlimit(RLIMIT_CPU, &rlc); |
47 |
|
} |
48 |
|
#endif /* ! __WIN32__ */ |
49 |
|
} |
50 |
|
|
51 |
9312 |
CommandExecutor::CommandExecutor(std::unique_ptr<api::Solver>& solver) |
52 |
|
: d_solver(solver), |
53 |
9312 |
d_symman(new SymbolManager(d_solver.get())), |
54 |
18624 |
d_result() |
55 |
|
{ |
56 |
9312 |
} |
57 |
18624 |
CommandExecutor::~CommandExecutor() |
58 |
|
{ |
59 |
18624 |
} |
60 |
|
|
61 |
6583 |
void CommandExecutor::storeOptionsAsOriginal() |
62 |
|
{ |
63 |
6583 |
d_solver->d_originalOptions->copyValues(d_solver->d_slv->getOptions()); |
64 |
6583 |
} |
65 |
|
|
66 |
6563 |
void CommandExecutor::printStatistics(std::ostream& out) const |
67 |
|
{ |
68 |
6563 |
if (d_solver->getOptionInfo("stats").boolValue()) |
69 |
|
{ |
70 |
|
const auto& stats = d_solver->getStatistics(); |
71 |
|
auto it = stats.begin(d_solver->getOptionInfo("stats-expert").boolValue(), |
72 |
|
d_solver->getOptionInfo("stats-all").boolValue()); |
73 |
|
for (; it != stats.end(); ++it) |
74 |
|
{ |
75 |
|
out << it->first << " = " << it->second << std::endl; |
76 |
|
} |
77 |
|
} |
78 |
6563 |
} |
79 |
|
|
80 |
|
void CommandExecutor::printStatisticsSafe(int fd) const |
81 |
|
{ |
82 |
|
if (d_solver->getOptionInfo("stats").boolValue()) |
83 |
|
{ |
84 |
|
d_solver->printStatisticsSafe(fd); |
85 |
|
} |
86 |
|
} |
87 |
|
|
88 |
242553 |
bool CommandExecutor::doCommand(Command* cmd) |
89 |
|
{ |
90 |
242553 |
CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd); |
91 |
242553 |
if(seq != nullptr) { |
92 |
|
// assume no error |
93 |
140 |
bool status = true; |
94 |
|
|
95 |
493 |
for (CommandSequence::iterator subcmd = seq->begin(); |
96 |
493 |
status && subcmd != seq->end(); |
97 |
|
++subcmd) |
98 |
|
{ |
99 |
353 |
status = doCommand(*subcmd); |
100 |
|
} |
101 |
|
|
102 |
140 |
return status; |
103 |
|
} else { |
104 |
242413 |
if (d_solver->getOptionInfo("verbosity").intValue() > 2) |
105 |
|
{ |
106 |
11 |
d_solver->getDriverOptions().out() << "Invoking: " << *cmd << std::endl; |
107 |
|
} |
108 |
|
|
109 |
242413 |
return doCommandSingleton(cmd); |
110 |
|
} |
111 |
|
} |
112 |
|
|
113 |
|
void CommandExecutor::reset() |
114 |
|
{ |
115 |
|
printStatistics(d_solver->getDriverOptions().err()); |
116 |
|
Command::resetSolver(d_solver.get()); |
117 |
|
} |
118 |
|
|
119 |
242442 |
bool CommandExecutor::doCommandSingleton(Command* cmd) |
120 |
|
{ |
121 |
484884 |
bool status = solverInvoke( |
122 |
727326 |
d_solver.get(), d_symman.get(), cmd, d_solver->getDriverOptions().out()); |
123 |
|
|
124 |
484884 |
api::Result res; |
125 |
242442 |
const CheckSatCommand* cs = dynamic_cast<const CheckSatCommand*>(cmd); |
126 |
242442 |
if(cs != nullptr) { |
127 |
9443 |
d_result = res = cs->getResult(); |
128 |
|
} |
129 |
|
const CheckSatAssumingCommand* csa = |
130 |
242442 |
dynamic_cast<const CheckSatAssumingCommand*>(cmd); |
131 |
242442 |
if (csa != nullptr) |
132 |
|
{ |
133 |
1563 |
d_result = res = csa->getResult(); |
134 |
|
} |
135 |
242442 |
const QueryCommand* q = dynamic_cast<const QueryCommand*>(cmd); |
136 |
242442 |
if(q != nullptr) { |
137 |
23 |
d_result = res = q->getResult(); |
138 |
|
} |
139 |
|
|
140 |
242442 |
bool isResultUnsat = res.isUnsat() || res.isEntailed(); |
141 |
242442 |
bool isResultSat = res.isSat() || res.isNotEntailed(); |
142 |
|
|
143 |
|
// dump the model/proof/unsat core if option is set |
144 |
242442 |
if (status) { |
145 |
484788 |
std::vector<std::unique_ptr<Command> > getterCommands; |
146 |
727182 |
if (d_solver->getOptionInfo("dump-models").boolValue() |
147 |
727192 |
&& (isResultSat |
148 |
34 |
|| (res.isSatUnknown() |
149 |
|
&& res.getUnknownExplanation() == api::Result::INCOMPLETE))) |
150 |
|
{ |
151 |
10 |
getterCommands.emplace_back(new GetModelCommand()); |
152 |
|
} |
153 |
242394 |
if (d_solver->getOptionInfo("dump-proofs").boolValue() && isResultUnsat) |
154 |
|
{ |
155 |
1 |
getterCommands.emplace_back(new GetProofCommand()); |
156 |
|
} |
157 |
|
|
158 |
727182 |
if ((d_solver->getOptionInfo("dump-instantiations").boolValue() |
159 |
484641 |
|| d_solver->getOptionInfo("dump-instantiations-debug").boolValue()) |
160 |
727329 |
&& GetInstantiationsCommand::isEnabled(d_solver.get(), res)) |
161 |
|
{ |
162 |
15 |
getterCommands.emplace_back(new GetInstantiationsCommand()); |
163 |
|
} |
164 |
|
|
165 |
727182 |
if (d_solver->getOptionInfo("dump-unsat-cores").boolValue() |
166 |
727182 |
&& isResultUnsat) |
167 |
|
{ |
168 |
3 |
getterCommands.emplace_back(new GetUnsatCoreCommand()); |
169 |
|
} |
170 |
|
|
171 |
727182 |
if (d_solver->getOptionInfo("dump-difficulty").boolValue() |
172 |
727182 |
&& (isResultUnsat || isResultSat || res.isSatUnknown())) |
173 |
|
{ |
174 |
|
getterCommands.emplace_back(new GetDifficultyCommand()); |
175 |
|
} |
176 |
|
|
177 |
242394 |
if (!getterCommands.empty()) { |
178 |
|
// set no time limit during dumping if applicable |
179 |
29 |
if (d_solver->getOptionInfo("force-no-limit-cpu-while-dump").boolValue()) |
180 |
|
{ |
181 |
|
setNoLimitCPU(); |
182 |
|
} |
183 |
58 |
for (const auto& getterCommand : getterCommands) { |
184 |
29 |
status = doCommandSingleton(getterCommand.get()); |
185 |
29 |
if (!status) |
186 |
|
{ |
187 |
|
break; |
188 |
|
} |
189 |
|
} |
190 |
|
} |
191 |
|
} |
192 |
484884 |
return status; |
193 |
|
} |
194 |
|
|
195 |
242442 |
bool solverInvoke(api::Solver* solver, |
196 |
|
SymbolManager* sm, |
197 |
|
Command* cmd, |
198 |
|
std::ostream& out) |
199 |
|
{ |
200 |
|
// print output for -o raw-benchmark |
201 |
242442 |
if (solver->isOutputOn("raw-benchmark")) |
202 |
|
{ |
203 |
21 |
cmd->toStream(solver->getOutput("raw-benchmark")); |
204 |
|
} |
205 |
|
|
206 |
|
// In parse-only mode, we do not invoke any of the commands except define-fun |
207 |
|
// commands. We invoke define-fun commands because they add function names |
208 |
|
// to the symbol table. |
209 |
727326 |
if (solver->getOptionInfo("parse-only").boolValue() |
210 |
727326 |
&& dynamic_cast<DefineFunctionCommand*>(cmd) == nullptr) |
211 |
|
{ |
212 |
|
return true; |
213 |
|
} |
214 |
|
|
215 |
242442 |
cmd->invoke(solver, sm, out); |
216 |
|
// ignore the error if the command-verbosity is 0 for this command |
217 |
|
std::string commandName = |
218 |
484884 |
std::string("command-verbosity:") + cmd->getCommandName(); |
219 |
242442 |
if (solver->getOption(commandName) == "0") |
220 |
|
{ |
221 |
|
return true; |
222 |
|
} |
223 |
242442 |
return !cmd->fail(); |
224 |
|
} |
225 |
|
|
226 |
6563 |
void CommandExecutor::flushOutputStreams() { |
227 |
6563 |
printStatistics(d_solver->getDriverOptions().err()); |
228 |
|
|
229 |
|
// make sure out and err streams are flushed too |
230 |
6563 |
d_solver->getDriverOptions().out() << std::flush; |
231 |
6563 |
d_solver->getDriverOptions().err() << std::flush; |
232 |
6563 |
} |
233 |
|
|
234 |
|
} // namespace main |
235 |
31110 |
} // namespace cvc5 |