GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/main/command_executor.h Lines: 6 6 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file command_executor.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Kshitij Bansal, Aina Niemetz
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
#ifndef CVC4__MAIN__COMMAND_EXECUTOR_H
16
#define CVC4__MAIN__COMMAND_EXECUTOR_H
17
18
#include <iosfwd>
19
#include <string>
20
21
#include "api/cvc4cpp.h"
22
#include "expr/symbol_manager.h"
23
#include "options/options.h"
24
#include "smt/smt_engine.h"
25
#include "util/statistics_registry.h"
26
27
namespace CVC4 {
28
29
class Command;
30
31
namespace main {
32
33
class CommandExecutor
34
{
35
 private:
36
  std::string d_lastStatistics;
37
38
 protected:
39
  /**
40
   * The solver object, which is allocated by this class and is used for
41
   * executing most commands (e.g. check-sat).
42
   */
43
  std::unique_ptr<api::Solver> d_solver;
44
  /**
45
   * The symbol manager, which is allocated by this class. This manages
46
   * all things related to definitions of symbols and their impact on behaviors
47
   * for commands (e.g. get-unsat-core, get-model, get-assignment), as well
48
   * as tracking expression names. Note the symbol manager is independent from
49
   * the parser, which uses this symbol manager given a text input.
50
   *
51
   * Certain commands (e.g. reset-assertions) have a specific impact on the
52
   * symbol manager.
53
   */
54
  std::unique_ptr<SymbolManager> d_symman;
55
  Options& d_options;
56
  api::Result d_result;
57
58
 public:
59
  CommandExecutor(Options& options);
60
61
  virtual ~CommandExecutor();
62
63
  /**
64
   * Executes a command. Recursively handles if cmd is a command
65
   * sequence.  Eventually uses doCommandSingleton (which can be
66
   * overridden by a derived class).
67
   */
68
  bool doCommand(CVC4::Command* cmd);
69
70
280747
  bool doCommand(std::unique_ptr<CVC4::Command>& cmd) {
71
280747
    return doCommand(cmd.get());
72
  }
73
74
  /** Get a pointer to the solver object owned by this CommandExecutor. */
75
5459
  api::Solver* getSolver() { return d_solver.get(); }
76
77
  /** Get a pointer to the symbol manager owned by this CommandExecutor */
78
5459
  SymbolManager* getSymbolManager() { return d_symman.get(); }
79
80
5399
  api::Result getResult() const { return d_result; }
81
  void reset();
82
83
16335
  SmtEngine* getSmtEngine() const { return d_solver->getSmtEngine(); }
84
85
  /**
86
   * Flushes statistics to a file descriptor.
87
   */
88
  virtual void flushStatistics(std::ostream& out) const;
89
90
  /**
91
   * Flushes statistics to a file descriptor.
92
   * Safe to use in a signal handler.
93
   */
94
  void safeFlushStatistics(int fd) const;
95
96
  static void printStatsFilterZeros(std::ostream& out,
97
                                    const std::string& statsString);
98
99
  void flushOutputStreams();
100
101
protected:
102
  /** Executes treating cmd as a singleton */
103
  virtual bool doCommandSingleton(CVC4::Command* cmd);
104
105
private:
106
  CommandExecutor();
107
108
}; /* class CommandExecutor */
109
110
bool solverInvoke(api::Solver* solver,
111
                  SymbolManager* sm,
112
                  Command* cmd,
113
                  std::ostream* out);
114
115
}/* CVC4::main namespace */
116
}/* CVC4 namespace */
117
118
#endif  /* CVC4__MAIN__COMMAND_EXECUTOR_H */