GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/main/command_executor.cpp Lines: 71 147 48.3 %
Date: 2021-03-23 Branches: 114 349 32.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file command_executor.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Kshitij Bansal, Andrew Reynolds, Morgan Deters
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief An additional layer between commands and invoking them.
13
 **/
14
15
#include "main/command_executor.h"
16
17
#ifndef __WIN32__
18
#  include <sys/resource.h>
19
#endif /* ! __WIN32__ */
20
21
#include <iostream>
22
#include <memory>
23
#include <string>
24
#include <vector>
25
26
#include "main/main.h"
27
#include "smt/command.h"
28
29
namespace CVC4 {
30
namespace main {
31
32
// Function to cancel any (externally-imposed) limit on CPU time.
33
// This is used for competitions while a solution (proof or model)
34
// is being dumped (so that we don't give "sat" or "unsat" then get
35
// interrupted partway through outputting a proof!).
36
void setNoLimitCPU() {
37
  // Windows doesn't have these things, just ignore
38
#ifndef __WIN32__
39
  struct rlimit rlc;
40
  int st = getrlimit(RLIMIT_CPU, &rlc);
41
  if(st == 0) {
42
    rlc.rlim_cur = rlc.rlim_max;
43
    setrlimit(RLIMIT_CPU, &rlc);
44
  }
45
#endif /* ! __WIN32__ */
46
}
47
48
void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString, const std::string& curStatsString);
49
50
5460
CommandExecutor::CommandExecutor(Options& options)
51
5461
    : d_solver(new api::Solver(&options)),
52
5459
      d_symman(new SymbolManager(d_solver.get())),
53
      d_options(options),
54
16378
      d_result()
55
{
56
5459
}
57
16314
CommandExecutor::~CommandExecutor()
58
{
59
  // ensure that symbol manager is destroyed before solver
60
5438
  d_symman.reset(nullptr);
61
5438
  d_solver.reset(nullptr);
62
10876
}
63
64
void CommandExecutor::flushStatistics(std::ostream& out) const
65
{
66
  // SmtEngine + node manager flush statistics is part of the call below
67
  getSmtEngine()->flushStatistics(out);
68
}
69
70
void CommandExecutor::safeFlushStatistics(int fd) const
71
{
72
  // SmtEngine + node manager flush statistics is part of the call below
73
  getSmtEngine()->safeFlushStatistics(fd);
74
}
75
76
286676
bool CommandExecutor::doCommand(Command* cmd)
77
{
78
286676
  if( d_options.getParseOnly() ) {
79
    return true;
80
  }
81
82
286676
  CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd);
83
286676
  if(seq != nullptr) {
84
    // assume no error
85
3525
    bool status = true;
86
87
9454
    for (CommandSequence::iterator subcmd = seq->begin();
88
9454
         status && subcmd != seq->end();
89
         ++subcmd)
90
    {
91
5929
      status = doCommand(*subcmd);
92
    }
93
94
3525
    return status;
95
  } else {
96
283151
    if(d_options.getVerbosity() > 2) {
97
11
      *d_options.getOut() << "Invoking: " << *cmd << std::endl;
98
    }
99
100
283151
    return doCommandSingleton(cmd);
101
  }
102
}
103
104
void CommandExecutor::reset()
105
{
106
  if (d_options.getStatistics())
107
  {
108
    flushStatistics(*d_options.getErr());
109
  }
110
  /* We have to keep options passed via CL on reset. These options are stored
111
   * in CommandExecutor::d_options (populated and created in the driver), and
112
   * CommandExecutor::d_options only contains *these* options since the
113
   * NodeManager copies the options into a new options object before SmtEngine
114
   * configures additional options based on the given CL options.
115
   * We can thus safely reuse CommandExecutor::d_options here. */
116
  d_solver.reset(new api::Solver(&d_options));
117
}
118
119
283174
bool CommandExecutor::doCommandSingleton(Command* cmd)
120
{
121
283174
  bool status = true;
122
283174
  if(d_options.getVerbosity() >= -1) {
123
283174
    status =
124
283174
        solverInvoke(d_solver.get(), d_symman.get(), cmd, d_options.getOut());
125
  } else {
126
    status = solverInvoke(d_solver.get(), d_symman.get(), cmd, nullptr);
127
  }
128
129
566348
  api::Result res;
130
283174
  const CheckSatCommand* cs = dynamic_cast<const CheckSatCommand*>(cmd);
131
283174
  if(cs != nullptr) {
132
7448
    d_result = res = cs->getResult();
133
  }
134
  const CheckSatAssumingCommand* csa =
135
283174
      dynamic_cast<const CheckSatAssumingCommand*>(cmd);
136
283174
  if (csa != nullptr)
137
  {
138
980
    d_result = res = csa->getResult();
139
  }
140
283174
  const QueryCommand* q = dynamic_cast<const QueryCommand*>(cmd);
141
283174
  if(q != nullptr) {
142
221
    d_result = res = q->getResult();
143
  }
144
145
283174
  if((cs != nullptr || q != nullptr) && d_options.getStatsEveryQuery()) {
146
    std::ostringstream ossCurStats;
147
    flushStatistics(ossCurStats);
148
    std::ostream& err = *d_options.getErr();
149
    printStatsIncremental(err, d_lastStatistics, ossCurStats.str());
150
    d_lastStatistics = ossCurStats.str();
151
  }
152
153
283174
  bool isResultUnsat = res.isUnsat() || res.isEntailed();
154
155
  // dump the model/proof/unsat core if option is set
156
283174
  if (status) {
157
566270
    std::vector<std::unique_ptr<Command> > getterCommands;
158
566270
    if (d_options.getDumpModels()
159
283145
        && (res.isSat()
160
34
            || (res.isSatUnknown()
161
                && res.getUnknownExplanation() == api::Result::INCOMPLETE)))
162
    {
163
10
      getterCommands.emplace_back(new GetModelCommand());
164
    }
165
283135
    if (d_options.getDumpProofs() && isResultUnsat)
166
    {
167
      getterCommands.emplace_back(new GetProofCommand());
168
    }
169
170
566270
    if (d_options.getDumpInstantiations()
171
283145
        && ((d_options.getInstFormatMode() != options::InstFormatMode::SZS
172
89
             && (res.isSat()
173
89
                 || (res.isSatUnknown()
174
                     && res.getUnknownExplanation()
175
                            == api::Result::INCOMPLETE)))
176
89
            || isResultUnsat))
177
    {
178
10
      getterCommands.emplace_back(new GetInstantiationsCommand());
179
    }
180
181
283135
    if (d_options.getDumpUnsatCores() && isResultUnsat)
182
    {
183
3
      getterCommands.emplace_back(new GetUnsatCoreCommand());
184
    }
185
186
283135
    if (!getterCommands.empty()) {
187
      // set no time limit during dumping if applicable
188
23
      if (d_options.getForceNoLimitCpuWhileDump()) {
189
        setNoLimitCPU();
190
      }
191
46
      for (const auto& getterCommand : getterCommands) {
192
23
        status = doCommandSingleton(getterCommand.get());
193
23
        if (!status)
194
        {
195
          break;
196
        }
197
      }
198
    }
199
  }
200
566348
  return status;
201
}
202
203
283174
bool solverInvoke(api::Solver* solver,
204
                  SymbolManager* sm,
205
                  Command* cmd,
206
                  std::ostream* out)
207
{
208
283174
  if (out == NULL)
209
  {
210
    cmd->invoke(solver, sm);
211
  }
212
  else
213
  {
214
283174
    cmd->invoke(solver, sm, *out);
215
  }
216
  // ignore the error if the command-verbosity is 0 for this command
217
  std::string commandName =
218
566348
      std::string("command-verbosity:") + cmd->getCommandName();
219
283174
  if (solver->getOption(commandName) == "0")
220
  {
221
    return true;
222
  }
223
283174
  return !cmd->fail();
224
}
225
226
void printStatsIncremental(std::ostream& out,
227
                           const std::string& prvsStatsString,
228
                           const std::string& curStatsString)
229
{
230
  if(prvsStatsString == "") {
231
    out << curStatsString;
232
    return;
233
  }
234
235
  // read each line
236
  // if a number, subtract and add that to parentheses
237
  std::istringstream issPrvs(prvsStatsString);
238
  std::istringstream issCur(curStatsString);
239
240
  std::string prvsStatName, prvsStatValue, curStatName, curStatValue;
241
242
  std::getline(issPrvs, prvsStatName, ',');
243
  std::getline(issCur, curStatName, ',');
244
245
  /**
246
   * Stat are assumed to one-per line: "<statName>, <statValue>"
247
   *   e.g. "sat::decisions, 100"
248
   * Output is of the form: "<statName>, <statValue> (<statDiffFromPrvs>)"
249
   *   e.g. "sat::decisions, 100 (20)"
250
   * If the value is not numeric, no change is made.
251
   */
252
  while( !issCur.eof() ) {
253
254
    std::getline(issCur, curStatValue, '\n');
255
256
    if(curStatName == prvsStatName) {
257
      std::getline(issPrvs, prvsStatValue, '\n');
258
259
      double prvsFloat, curFloat;
260
      bool isFloat =
261
        (std::istringstream(prvsStatValue) >> prvsFloat) &&
262
        (std::istringstream(curStatValue) >> curFloat);
263
264
      if(isFloat) {
265
        const std::streamsize old_precision = out.precision();
266
        out << curStatName << ", " << curStatValue << " "
267
            << "(" << std::setprecision(8) << (curFloat-prvsFloat) << ")"
268
            << std::endl;
269
        out.precision(old_precision);
270
      } else {
271
        out << curStatName << ", " << curStatValue << std::endl;
272
      }
273
274
      std::getline(issPrvs, prvsStatName, ',');
275
    } else {
276
      out << curStatName << ", " << curStatValue << std::endl;
277
    }
278
279
    std::getline(issCur, curStatName, ',');
280
  }
281
}
282
283
void CommandExecutor::printStatsFilterZeros(std::ostream& out,
284
                                            const std::string& statsString) {
285
  // read each line, if a number, check zero and skip if so
286
  // Stat are assumed to one-per line: "<statName>, <statValue>"
287
288
  std::istringstream iss(statsString);
289
  std::string statName, statValue;
290
291
  std::getline(iss, statName, ',');
292
293
  while (!iss.eof())
294
  {
295
    std::getline(iss, statValue, '\n');
296
297
    bool skip = false;
298
    try
299
    {
300
      double dval = std::stod(statValue);
301
      skip = (dval == 0.0);
302
    }
303
    // Value can not be converted, don't skip
304
    catch (const std::invalid_argument&) {}
305
    catch (const std::out_of_range&) {}
306
307
    skip = skip || (statValue == " \"0\"" || statValue == " \"[]\"");
308
309
    if (!skip)
310
    {
311
      out << statName << "," << statValue << std::endl;
312
    }
313
314
    std::getline(iss, statName, ',');
315
  }
316
}
317
318
5438
void CommandExecutor::flushOutputStreams() {
319
5438
  if(d_options.getStatistics()) {
320
    if(d_options.getStatsHideZeros() == false) {
321
      flushStatistics(*(d_options.getErr()));
322
    } else {
323
      std::ostringstream ossStats;
324
      flushStatistics(ossStats);
325
      printStatsFilterZeros(*(d_options.getErr()), ossStats.str());
326
    }
327
  }
328
329
  // make sure out and err streams are flushed too
330
5438
  d_options.flushOut();
331
5438
  d_options.flushErr();
332
5438
}
333
334
}/* CVC4::main namespace */
335
26667
}/* CVC4 namespace */