GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/main/command_executor.cpp Lines: 72 150 48.0 %
Date: 2021-03-22 Branches: 116 353 32.9 %

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