GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/main/command_executor.h Lines: 8 8 100.0 %
Date: 2021-03-22 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
  SmtEngine* d_smtEngine;
56
  Options& d_options;
57
  StatisticsRegistry d_stats;
58
  api::Result d_result;
59
60
 public:
61
  CommandExecutor(Options& options);
62
63
  virtual ~CommandExecutor();
64
65
  /**
66
   * Executes a command. Recursively handles if cmd is a command
67
   * sequence.  Eventually uses doCommandSingleton (which can be
68
   * overridden by a derived class).
69
   */
70
  bool doCommand(CVC4::Command* cmd);
71
72
280737
  bool doCommand(std::unique_ptr<CVC4::Command>& cmd) {
73
280737
    return doCommand(cmd.get());
74
  }
75
76
  /** Get a pointer to the solver object owned by this CommandExecutor. */
77
5457
  api::Solver* getSolver() { return d_solver.get(); }
78
79
  /** Get a pointer to the symbol manager owned by this CommandExecutor */
80
5457
  SymbolManager* getSymbolManager() { return d_symman.get(); }
81
82
5397
  api::Result getResult() const { return d_result; }
83
  void reset();
84
85
16350
  StatisticsRegistry& getStatisticsRegistry() {
86
16350
    return d_stats;
87
  }
88
89
5457
  SmtEngine* getSmtEngine() { return d_smtEngine; }
90
91
  /**
92
   * Flushes statistics to a file descriptor.
93
   */
94
  virtual void flushStatistics(std::ostream& out) const;
95
96
  /**
97
   * Flushes statistics to a file descriptor.
98
   * Safe to use in a signal handler.
99
   */
100
  void safeFlushStatistics(int fd) const;
101
102
  static void printStatsFilterZeros(std::ostream& out,
103
                                    const std::string& statsString);
104
105
  void flushOutputStreams();
106
107
protected:
108
  /** Executes treating cmd as a singleton */
109
  virtual bool doCommandSingleton(CVC4::Command* cmd);
110
111
private:
112
  CommandExecutor();
113
114
}; /* class CommandExecutor */
115
116
bool solverInvoke(api::Solver* solver,
117
                  SymbolManager* sm,
118
                  Command* cmd,
119
                  std::ostream* out);
120
121
}/* CVC4::main namespace */
122
}/* CVC4 namespace */
123
124
#endif  /* CVC4__MAIN__COMMAND_EXECUTOR_H */