GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/smt_engine_state.cpp Lines: 126 141 89.4 %
Date: 2021-03-23 Branches: 92 253 36.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file smt_engine_state.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Ying Sheng
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 "smt/smt_engine_state.h"
16
17
#include "options/smt_options.h"
18
#include "smt/smt_engine.h"
19
20
namespace CVC4 {
21
namespace smt {
22
23
9622
SmtEngineState::SmtEngineState(context::Context* c,
24
                               context::UserContext* u,
25
9622
                               SmtEngine& smt)
26
    : d_smt(smt),
27
      d_context(c),
28
      d_userContext(u),
29
      d_pendingPops(0),
30
      d_fullyInited(false),
31
      d_queryMade(false),
32
      d_needPostsolve(false),
33
      d_status(),
34
      d_expectedStatus(),
35
9622
      d_smtMode(SmtMode::START)
36
{
37
9622
}
38
39
3390
void SmtEngineState::notifyExpectedStatus(const std::string& status)
40
{
41
3390
  Assert(status == "sat" || status == "unsat" || status == "unknown")
42
      << "SmtEngineState::notifyExpectedStatus: unexpected status string "
43
      << status;
44
3390
  d_expectedStatus = Result(status, d_filename);
45
3390
}
46
47
32
void SmtEngineState::notifyResetAssertions()
48
{
49
32
  doPendingPops();
50
64
  while (!d_userLevels.empty())
51
  {
52
16
    userPop();
53
  }
54
  // Remember the global push/pop around everything when beyond Start mode
55
  // (see solver execution modes in the SMT-LIB standard)
56
32
  Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1);
57
32
  popto(0);
58
32
}
59
60
12435
void SmtEngineState::notifyCheckSat(bool hasAssumptions)
61
{
62
  // process the pending pops
63
12435
  doPendingPops();
64
12435
  if (d_queryMade && !options::incrementalSolving())
65
  {
66
    throw ModalException(
67
        "Cannot make multiple queries unless "
68
        "incremental solving is enabled "
69
        "(try --incremental)");
70
  }
71
72
  // Note that a query has been made and we are in assert mode
73
12435
  d_queryMade = true;
74
12435
  d_smtMode = SmtMode::ASSERT;
75
76
  // push if there are assumptions
77
12435
  if (hasAssumptions)
78
  {
79
2191
    internalPush();
80
  }
81
12435
}
82
83
12401
void SmtEngineState::notifyCheckSatResult(bool hasAssumptions, Result r)
84
{
85
12401
  d_needPostsolve = true;
86
87
  // Pop the context
88
12401
  if (hasAssumptions)
89
  {
90
2174
    internalPop();
91
  }
92
93
  // Remember the status
94
12401
  d_status = r;
95
  // Check against expected status
96
28127
  if (!d_expectedStatus.isUnknown() && !d_status.isUnknown()
97
15723
      && d_status != d_expectedStatus)
98
  {
99
    CVC4_FATAL() << "Expected result " << d_expectedStatus << " but got "
100
                 << d_status;
101
  }
102
  // clear expected status
103
12401
  d_expectedStatus = Result();
104
  // Update the SMT mode
105
12401
  switch (d_status.asSatisfiabilityResult().isSat())
106
  {
107
6441
    case Result::UNSAT: d_smtMode = SmtMode::UNSAT; break;
108
5864
    case Result::SAT: d_smtMode = SmtMode::SAT; break;
109
96
    default: d_smtMode = SmtMode::SAT_UNKNOWN;
110
  }
111
12401
}
112
113
18
void SmtEngineState::notifyGetAbduct(bool success)
114
{
115
18
  if (success)
116
  {
117
    // successfully generated an abduct, update to abduct state
118
18
    d_smtMode = SmtMode::ABDUCT;
119
  }
120
  else
121
  {
122
    // failed, we revert to the assert state
123
    d_smtMode = SmtMode::ASSERT;
124
  }
125
18
}
126
127
10
void SmtEngineState::notifyGetInterpol(bool success)
128
{
129
10
  if (success)
130
  {
131
    // successfully generated an interpolant, update to interpol state
132
10
    d_smtMode = SmtMode::INTERPOL;
133
  }
134
  else
135
  {
136
    // failed, we revert to the assert state
137
    d_smtMode = SmtMode::ASSERT;
138
  }
139
10
}
140
141
9029
void SmtEngineState::setup()
142
{
143
  // push a context
144
9029
  push();
145
9029
}
146
147
8997
void SmtEngineState::finishInit()
148
{
149
  // set the flag to remember that we are fully initialized
150
8997
  d_fullyInited = true;
151
8997
}
152
153
9600
void SmtEngineState::shutdown()
154
{
155
9600
  doPendingPops();
156
157
10412
  while (options::incrementalSolving() && d_userContext->getLevel() > 1)
158
  {
159
406
    internalPop(true);
160
  }
161
9600
}
162
163
9600
void SmtEngineState::cleanup()
164
{
165
  // pop to level zero
166
9600
  popto(0);
167
9600
}
168
169
5559
void SmtEngineState::setFilename(const std::string& filename)
170
{
171
5559
  d_filename = filename;
172
5559
}
173
174
2556
void SmtEngineState::userPush()
175
{
176
2556
  if (!options::incrementalSolving())
177
  {
178
    throw ModalException(
179
        "Cannot push when not solving incrementally (use --incremental)");
180
  }
181
  // The problem isn't really "extended" yet, but this disallows
182
  // get-model after a push, simplifying our lives somewhat and
183
  // staying symmetric with pop.
184
2556
  d_smtMode = SmtMode::ASSERT;
185
186
2556
  d_userLevels.push_back(d_userContext->getLevel());
187
2556
  internalPush();
188
5112
  Trace("userpushpop") << "SmtEngineState: pushed to level "
189
2556
                       << d_userContext->getLevel() << std::endl;
190
2556
}
191
192
2150
void SmtEngineState::userPop()
193
{
194
2150
  if (!options::incrementalSolving())
195
  {
196
    throw ModalException(
197
        "Cannot pop when not solving incrementally (use --incremental)");
198
  }
199
2150
  if (d_userLevels.size() == 0)
200
  {
201
    throw ModalException("Cannot pop beyond the first user frame");
202
  }
203
  // The problem isn't really "extended" yet, but this disallows
204
  // get-model after a pop, simplifying our lives somewhat.  It might
205
  // not be strictly necessary to do so, since the pops occur lazily,
206
  // but also it would be weird to have a legally-executed (get-model)
207
  // that only returns a subset of the assignment (because the rest
208
  // is no longer in scope!).
209
2150
  d_smtMode = SmtMode::ASSERT;
210
211
2150
  AlwaysAssert(d_userContext->getLevel() > 0);
212
2150
  AlwaysAssert(d_userLevels.back() < d_userContext->getLevel());
213
6450
  while (d_userLevels.back() < d_userContext->getLevel())
214
  {
215
2150
    internalPop(true);
216
  }
217
2150
  d_userLevels.pop_back();
218
2150
}
219
220
9029
void SmtEngineState::push()
221
{
222
9029
  d_userContext->push();
223
9029
  d_context->push();
224
9029
}
225
226
void SmtEngineState::pop()
227
{
228
  d_userContext->pop();
229
  d_context->pop();
230
}
231
232
9632
void SmtEngineState::popto(int toLevel)
233
{
234
9632
  d_context->popto(toLevel);
235
9632
  d_userContext->popto(toLevel);
236
9632
}
237
238
context::UserContext* SmtEngineState::getUserContext() { return d_userContext; }
239
240
context::Context* SmtEngineState::getContext() { return d_context; }
241
242
10
Result SmtEngineState::getStatus() const { return d_status; }
243
244
230406
bool SmtEngineState::isFullyInited() const { return d_fullyInited; }
245
18239
bool SmtEngineState::isFullyReady() const
246
{
247
18239
  return d_fullyInited && d_pendingPops == 0;
248
}
249
8784
bool SmtEngineState::isQueryMade() const { return d_queryMade; }
250
2108
size_t SmtEngineState::getNumUserLevels() const { return d_userLevels.size(); }
251
252
6846
SmtMode SmtEngineState::getMode() const { return d_smtMode; }
253
254
91973
const std::string& SmtEngineState::getFilename() const { return d_filename; }
255
256
4747
void SmtEngineState::internalPush()
257
{
258
4747
  Assert(d_fullyInited);
259
4747
  Trace("smt") << "SmtEngineState::internalPush()" << std::endl;
260
4747
  doPendingPops();
261
4747
  if (options::incrementalSolving())
262
  {
263
    // notifies the SmtEngine to process the assertions immediately
264
3190
    d_smt.notifyPushPre();
265
3190
    d_userContext->push();
266
    // the context push is done inside of the SAT solver
267
3190
    d_smt.notifyPushPost();
268
  }
269
4747
}
270
271
4730
void SmtEngineState::internalPop(bool immediate)
272
{
273
4730
  Assert(d_fullyInited);
274
4730
  Trace("smt") << "SmtEngineState::internalPop()" << std::endl;
275
4730
  if (options::incrementalSolving())
276
  {
277
3190
    ++d_pendingPops;
278
  }
279
4730
  if (immediate)
280
  {
281
2556
    doPendingPops();
282
  }
283
4730
}
284
285
120630
void SmtEngineState::doPendingPops()
286
{
287
120630
  Trace("smt") << "SmtEngineState::doPendingPops()" << std::endl;
288
120630
  Assert(d_pendingPops == 0 || options::incrementalSolving());
289
  // check to see if a postsolve() is pending
290
120630
  if (d_needPostsolve)
291
  {
292
12401
    d_smt.notifyPostSolvePre();
293
  }
294
127010
  while (d_pendingPops > 0)
295
  {
296
    // the context pop is done inside of the SAT solver
297
3190
    d_smt.notifyPopPre();
298
    // pop the context
299
3190
    d_userContext->pop();
300
3190
    --d_pendingPops;
301
    // no need for pop post (for now)
302
  }
303
120630
  if (d_needPostsolve)
304
  {
305
12401
    d_smt.notifyPostSolvePost();
306
12401
    d_needPostsolve = false;
307
  }
308
120630
}
309
310
}  // namespace smt
311
26685
}  // namespace CVC4