GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/smt_engine_state.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file smt_engine_state.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Ying Sheng, 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 Utility for maintaining the state of the SMT engine.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__SMT__SMT_ENGINE_STATE_H
18
#define CVC4__SMT__SMT_ENGINE_STATE_H
19
20
#include <string>
21
22
#include "context/context.h"
23
#include "smt/smt_mode.h"
24
#include "util/result.h"
25
26
namespace CVC4 {
27
28
class SmtEngine;
29
30
namespace smt {
31
32
/**
33
 * This utility is responsible for maintaining the basic state of the SmtEngine.
34
 *
35
 * It has no concept of anything related to the assertions of the SmtEngine,
36
 * or more generally it does not depend on Node.
37
 *
38
 * This class has three sets of interfaces:
39
 * (1) notification methods that are used by SmtEngine to notify when an event
40
 * occurs (e.g. the beginning of a check-sat call),
41
 * (2) maintaining the SAT and user contexts to be used by the SmtEngine,
42
 * (3) general information queries, including the mode that the SmtEngine is
43
 * in, based on the notifications it has received.
44
 *
45
 * It maintains a reference to the SmtEngine for the sake of making callbacks.
46
 */
47
class SmtEngineState
48
{
49
 public:
50
  SmtEngineState(context::Context* c, context::UserContext* u, SmtEngine& smt);
51
9599
  ~SmtEngineState() {}
52
  /**
53
   * Notify that the expected status of the next check-sat is given by the
54
   * string status, which should be one of "sat", "unsat" or "unknown".
55
   */
56
  void notifyExpectedStatus(const std::string& status);
57
  /**
58
   * Notify that the SmtEngine is fully initialized, which is called when
59
   * options are finalized.
60
   */
61
  void notifyFullyInited();
62
  /**
63
   * Notify that we are resetting the assertions, called when a reset-assertions
64
   * command is issued by the user.
65
   */
66
  void notifyResetAssertions();
67
  /**
68
   * Notify that we are about to call check-sat. This call is made prior to
69
   * initializing the assertions. It processes pending pops and pushes a
70
   * (user) context if necessary.
71
   *
72
   * @param hasAssumptions Whether the call to check-sat has assumptions. If
73
   * so, we push a context.
74
   */
75
  void notifyCheckSat(bool hasAssumptions);
76
  /**
77
   * Notify that the result of the last check-sat was r. This should be called
78
   * once immediately following notifyCheckSat() if the check-sat call
79
   * returned normal (i.e. it was not interupted).
80
   *
81
   * @param hasAssumptions Whether the prior call to check-sat had assumptions.
82
   * If so, we pop a context.
83
   * @param r The result of the check-sat call.
84
   */
85
  void notifyCheckSatResult(bool hasAssumptions, Result r);
86
  /**
87
   * Notify that we finished an abduction query, where success is whether the
88
   * command was successful. This is managed independently of the above
89
   * calls for notifying check-sat. In other words, if a get-abduct command
90
   * is issued to an SmtEngine, it may use a satisfiability call (if desired)
91
   * to solve the abduction query. This method is called *in addition* to
92
   * the above calls to notifyCheckSat / notifyCheckSatResult in this case.
93
   * In particular, it is called after these two methods are completed.
94
   * This overwrites the SMT mode to the "ABDUCT" mode if the call to abduction
95
   * was successful.
96
   */
97
  void notifyGetAbduct(bool success);
98
  /**
99
   * Notify that we finished an interpolation query, where success is whether
100
   * the command was successful. This is managed independently of the above
101
   * calls for notifying check-sat. In other words, if a get-interpol command
102
   * is issued to an SmtEngine, it may use a satisfiability call (if desired)
103
   * to solve the interpolation query. This method is called *in addition* to
104
   * the above calls to notifyCheckSat / notifyCheckSatResult in this case.
105
   * In particular, it is called after these two methods are completed.
106
   * This overwrites the SMT mode to the "INTERPOL" mode if the call to
107
   * interpolation was successful.
108
   */
109
  void notifyGetInterpol(bool success);
110
  /**
111
   * Setup the context, which makes a single push to maintain a global
112
   * context around everything.
113
   */
114
  void setup();
115
  /**
116
   * Set that we are in a fully initialized state.
117
   */
118
  void finishInit();
119
  /**
120
   * Prepare for a shutdown of the SmtEngine, which does pending pops and
121
   * pops the user context to zero.
122
   */
123
  void shutdown();
124
  /**
125
   * Cleanup, which pops all contexts to level zero.
126
   */
127
  void cleanup();
128
  /**
129
   * Set that the file name of the current instance is the given string. This
130
   * is used for various purposes (e.g. get-info, SZS status).
131
   */
132
  void setFilename(const std::string& filename);
133
134
  //---------------------------- context management
135
  /**
136
   * Do all pending pops, which ensures that the context levels are up-to-date.
137
   * This method should be called by the SmtEngine before using any of its
138
   * members that rely on the context (e.g. PropEngine or TheoryEngine).
139
   */
140
  void doPendingPops();
141
  /**
142
   * Called when the user of SmtEngine issues a push. This corresponds to
143
   * the SMT-LIB command push.
144
   */
145
  void userPush();
146
  /**
147
   * Called when the user of SmtEngine issues a pop. This corresponds to
148
   * the SMT-LIB command pop.
149
   */
150
  void userPop();
151
  /** Get a pointer to the UserContext owned by this SmtEngine. */
152
  context::UserContext* getUserContext();
153
  /** Get a pointer to the Context owned by this SmtEngine. */
154
  context::Context* getContext();
155
  //---------------------------- end context management
156
157
  //---------------------------- queries
158
  /**
159
   * Return true if the SmtEngine is fully initialized (post-construction).
160
   * This post-construction initialization is automatically triggered by the
161
   * use of the SmtEngine; e.g. when the first formula is asserted, a call
162
   * to simplify() is issued, a scope is pushed, etc.
163
   */
164
  bool isFullyInited() const;
165
  /**
166
   * Return true if the SmtEngine is fully initialized and there are no
167
   * pending pops.
168
   */
169
  bool isFullyReady() const;
170
  /**
171
   * Return true if a notifyCheckSat call has been made, e.g. a query has been
172
   * issued to the SmtEngine.
173
   */
174
  bool isQueryMade() const;
175
  /** Return the user context level.  */
176
  size_t getNumUserLevels() const;
177
  /** Get the status of the last check-sat */
178
  Result getStatus() const;
179
  /** Get the SMT mode we are in */
180
  SmtMode getMode() const;
181
  /** return the input name (if any) */
182
  const std::string& getFilename() const;
183
  //---------------------------- end queries
184
185
 private:
186
  /** Pushes the user and SAT contexts */
187
  void push();
188
  /** Pops the user and SAT contexts */
189
  void pop();
190
  /** Pops the user and SAT contexts to the given level */
191
  void popto(int toLevel);
192
  /**
193
   * Internal push, which processes any pending pops, and pushes (if in
194
   * incremental mode).
195
   */
196
  void internalPush();
197
  /**
198
   * Internal pop. If immediate is true, this processes any pending pops, and
199
   * pops (if in incremental mode). Otherwise, it increments the pending pop
200
   * counter and does nothing.
201
   */
202
  void internalPop(bool immediate = false);
203
  /** Reference to the SmtEngine */
204
  SmtEngine& d_smt;
205
  /** Expr manager context */
206
  context::Context* d_context;
207
  /** User level context */
208
  context::UserContext* d_userContext;
209
  /** The context levels of user pushes */
210
  std::vector<int> d_userLevels;
211
212
  /**
213
   * Number of internal pops that have been deferred.
214
   */
215
  unsigned d_pendingPops;
216
217
  /**
218
   * Whether or not the SmtEngine is fully initialized (post-construction).
219
   * This post-construction initialization is automatically triggered by the
220
   * use of the SmtEngine which calls the finishInit method above; e.g. when
221
   * the first formula is asserted, a call to simplify() is issued, a scope is
222
   * pushed, etc.
223
   */
224
  bool d_fullyInited;
225
226
  /**
227
   * Whether or not a notifyCheckSat call has been made, which corresponds to
228
   * when a checkEntailed() or checkSatisfiability() has already been
229
   * made through the SmtEngine.  If true, and incrementalSolving is false,
230
   * then attempting an additional checks for satisfiability will fail with
231
   * a ModalException during notifyCheckSat.
232
   */
233
  bool d_queryMade;
234
235
  /**
236
   * Internal status flag to indicate whether we have been issued a
237
   * notifyCheckSat call and have yet to process the "postsolve" methods of
238
   * SmtEngine via SmtEngine::notifyPostSolvePre/notifyPostSolvePost.
239
   */
240
  bool d_needPostsolve;
241
242
  /**
243
   * Most recent result of last checkSatisfiability/checkEntailed in the
244
   * SmtEngine.
245
   */
246
  Result d_status;
247
248
  /**
249
   * The expected status of the next satisfiability check.
250
   */
251
  Result d_expectedStatus;
252
253
  /** The SMT mode, for details see enumeration above. */
254
  SmtMode d_smtMode;
255
256
  /**
257
   * The input file name or the name set through (set-info :filename ...), if
258
   * any.
259
   */
260
  std::string d_filename;
261
};
262
263
}  // namespace smt
264
}  // namespace CVC4
265
266
#endif