GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/smt_solver.cpp Lines: 108 119 90.8 %
Date: 2021-03-22 Branches: 163 354 46.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file smt_solver.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Aina Niemetz, 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 The solver for SMT queries in an SmtEngine.
13
 **/
14
15
#include "smt/smt_solver.h"
16
17
#include "options/smt_options.h"
18
#include "prop/prop_engine.h"
19
#include "smt/assertions.h"
20
#include "smt/preprocessor.h"
21
#include "smt/smt_engine.h"
22
#include "smt/smt_engine_state.h"
23
#include "smt/smt_engine_stats.h"
24
#include "theory/logic_info.h"
25
#include "theory/theory_engine.h"
26
#include "theory/theory_traits.h"
27
28
using namespace std;
29
30
namespace CVC4 {
31
namespace smt {
32
33
9619
SmtSolver::SmtSolver(SmtEngine& smt,
34
                     SmtEngineState& state,
35
                     ResourceManager* rm,
36
                     Preprocessor& pp,
37
9619
                     SmtEngineStatistics& stats)
38
    : d_smt(smt),
39
      d_state(state),
40
      d_rm(rm),
41
      d_pp(pp),
42
      d_stats(stats),
43
      d_pnm(nullptr),
44
      d_theoryEngine(nullptr),
45
9619
      d_propEngine(nullptr)
46
{
47
9619
}
48
49
9598
SmtSolver::~SmtSolver() {}
50
51
8995
void SmtSolver::finishInit(const LogicInfo& logicInfo)
52
{
53
  // We have mutual dependency here, so we add the prop engine to the theory
54
  // engine later (it is non-essential there)
55
26985
  d_theoryEngine.reset(new TheoryEngine(d_smt.getContext(),
56
8995
                                        d_smt.getUserContext(),
57
                                        d_rm,
58
                                        logicInfo,
59
8995
                                        d_smt.getOutputManager(),
60
8995
                                        d_pnm));
61
62
  // Add the theories
63
125930
  for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST;
64
       ++id)
65
  {
66
116935
    theory::TheoryConstructor::addTheory(d_theoryEngine.get(), id);
67
  }
68
69
8995
  Trace("smt-debug") << "Making prop engine..." << std::endl;
70
  /* force destruction of referenced PropEngine to enforce that statistics
71
   * are unregistered by the obsolete PropEngine object before registered
72
   * again by the new PropEngine object */
73
8995
  d_propEngine.reset(nullptr);
74
26985
  d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(),
75
8995
                                          d_smt.getContext(),
76
8995
                                          d_smt.getUserContext(),
77
                                          d_rm,
78
8995
                                          d_smt.getOutputManager(),
79
8995
                                          d_pnm));
80
81
8995
  Trace("smt-debug") << "Setting up theory engine..." << std::endl;
82
8995
  d_theoryEngine->setPropEngine(getPropEngine());
83
8995
  Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
84
8995
  d_theoryEngine->finishInit();
85
8995
  d_propEngine->finishInit();
86
8995
}
87
88
32
void SmtSolver::resetAssertions()
89
{
90
  /* Create new PropEngine.
91
   * First force destruction of referenced PropEngine to enforce that
92
   * statistics are unregistered by the obsolete PropEngine object before
93
   * registered again by the new PropEngine object */
94
32
  d_propEngine.reset(nullptr);
95
96
  d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(),
96
32
                                          d_smt.getContext(),
97
32
                                          d_smt.getUserContext(),
98
                                          d_rm,
99
32
                                          d_smt.getOutputManager(),
100
32
                                          d_pnm));
101
32
  d_theoryEngine->setPropEngine(getPropEngine());
102
  // Notice that we do not reset TheoryEngine, nor does it require calling
103
  // finishInit again. In particular, TheoryEngine::finishInit does not
104
  // depend on knowing the associated PropEngine.
105
32
  d_propEngine->finishInit();
106
32
}
107
108
void SmtSolver::interrupt()
109
{
110
  if (d_propEngine != nullptr)
111
  {
112
    d_propEngine->interrupt();
113
  }
114
  if (d_theoryEngine != nullptr)
115
  {
116
    d_theoryEngine->interrupt();
117
  }
118
}
119
120
9598
void SmtSolver::shutdown()
121
{
122
9598
  if (d_propEngine != nullptr)
123
  {
124
8992
    d_propEngine->shutdown();
125
  }
126
9598
  if (d_theoryEngine != nullptr)
127
  {
128
8992
    d_theoryEngine->shutdown();
129
  }
130
9598
}
131
132
12433
Result SmtSolver::checkSatisfiability(Assertions& as,
133
                                      const std::vector<Node>& assumptions,
134
                                      bool inUnsatCore,
135
                                      bool isEntailmentCheck)
136
{
137
  // update the state to indicate we are about to run a check-sat
138
12433
  bool hasAssumptions = !assumptions.empty();
139
12433
  d_state.notifyCheckSat(hasAssumptions);
140
141
  // then, initialize the assertions
142
12433
  as.initializeCheckSat(assumptions, inUnsatCore, isEntailmentCheck);
143
144
  // make the check
145
12433
  Assert(d_smt.isFullyInited());
146
147
12433
  Trace("smt") << "SmtSolver::check()" << endl;
148
149
12433
  const std::string& filename = d_state.getFilename();
150
12433
  if (d_rm->out())
151
  {
152
    Result::UnknownExplanation why =
153
        d_rm->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT;
154
    return Result(Result::ENTAILMENT_UNKNOWN, why, filename);
155
  }
156
12433
  d_rm->beginCall();
157
158
  // Make sure the prop layer has all of the assertions
159
12433
  Trace("smt") << "SmtSolver::check(): processing assertions" << endl;
160
12433
  processAssertions(as);
161
12420
  Trace("smt") << "SmtSolver::check(): done processing assertions" << endl;
162
163
24840
  TimerStat::CodeTimer solveTimer(d_stats.d_solveTime);
164
165
12420
  Chat() << "solving..." << endl;
166
12420
  Trace("smt") << "SmtSolver::check(): running check" << endl;
167
24819
  Result result = d_propEngine->checkSat();
168
169
12399
  d_rm->endCall();
170
24798
  Trace("limit") << "SmtSolver::check(): cumulative millis "
171
24798
                 << d_rm->getTimeUsage() << ", resources "
172
12399
                 << d_rm->getResourceUsage() << endl;
173
174
37184
  if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
175
24818
      && result.asSatisfiabilityResult().isSat() == Result::UNSAT)
176
  {
177
4
    result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
178
  }
179
  // flipped if we did a global negation
180
12399
  if (as.isGlobalNegated())
181
  {
182
4
    Trace("smt") << "SmtSolver::process global negate " << result << std::endl;
183
4
    if (result.asSatisfiabilityResult().isSat() == Result::UNSAT)
184
    {
185
2
      result = Result(Result::SAT);
186
    }
187
2
    else if (result.asSatisfiabilityResult().isSat() == Result::SAT)
188
    {
189
      // Only can answer unsat if the theory is satisfaction complete. This
190
      // includes linear arithmetic and bitvectors, which are the primary
191
      // targets for the global negate option. Other logics are possible here
192
      // but not considered.
193
4
      LogicInfo logic = d_smt.getLogicInfo();
194
2
      if ((logic.isPure(theory::THEORY_ARITH) && logic.isLinear()) ||
195
          logic.isPure(theory::THEORY_BV))
196
      {
197
2
        result = Result(Result::UNSAT);
198
      }
199
      else
200
      {
201
        result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
202
      }
203
    }
204
4
    Trace("smt") << "SmtSolver::global negate returned " << result << std::endl;
205
  }
206
207
  // set the filename on the result
208
24798
  Result r = Result(result, filename);
209
210
  // notify our state of the check-sat result
211
12399
  d_state.notifyCheckSatResult(hasAssumptions, r);
212
213
12399
  return r;
214
}
215
216
18237
void SmtSolver::processAssertions(Assertions& as)
217
{
218
29560
  TimerStat::CodeTimer paTimer(d_stats.d_processAssertionsTime);
219
18237
  d_rm->spendResource(ResourceManager::Resource::PreprocessStep);
220
18237
  Assert(d_state.isFullyReady());
221
222
18237
  preprocessing::AssertionPipeline& ap = as.getAssertionPipeline();
223
224
18237
  if (ap.size() == 0)
225
  {
226
    // nothing to do
227
6914
    return;
228
  }
229
230
  // process the assertions with the preprocessor
231
11323
  bool noConflict = d_pp.process(as);
232
233
  // Notify the input formulas to theory engine
234
11314
  if (noConflict)
235
  {
236
10348
    Chat() << "notifying theory engine..." << std::endl;
237
10348
    d_propEngine->notifyPreprocessedAssertions(ap.ref());
238
  }
239
240
  // end: INVARIANT to maintain: no reordering of assertions or
241
  // introducing new ones
242
243
  // Push the formula to SAT
244
  {
245
11314
    Chat() << "converting to CNF..." << endl;
246
22628
    TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime);
247
11314
    const std::vector<Node>& assertions = ap.ref();
248
    // It is important to distinguish the input assertions from the skolem
249
    // definitions, as the decision justification heuristic treates the latter
250
    // specially.
251
11314
    preprocessing::IteSkolemMap& ism = ap.getIteSkolemMap();
252
11314
    preprocessing::IteSkolemMap::iterator it;
253
122822
    for (size_t i = 0, asize = assertions.size(); i < asize; i++)
254
    {
255
      // is the assertion a skolem definition?
256
111512
      it = ism.find(i);
257
111512
      if (it == ism.end())
258
      {
259
91971
        Chat() << "+ input " << assertions[i] << std::endl;
260
91975
        d_propEngine->assertFormula(assertions[i]);
261
      }
262
      else
263
      {
264
19541
        Chat() << "+ skolem definition " << assertions[i] << " (from "
265
               << it->second << ")" << std::endl;
266
19541
        d_propEngine->assertSkolemDefinition(assertions[i], it->second);
267
      }
268
    }
269
  }
270
271
  // clear the current assertions
272
11310
  as.clearCurrent();
273
}
274
275
962
void SmtSolver::setProofNodeManager(ProofNodeManager* pnm) { d_pnm = pnm; }
276
277
344852
TheoryEngine* SmtSolver::getTheoryEngine() { return d_theoryEngine.get(); }
278
279
52459
prop::PropEngine* SmtSolver::getPropEngine() { return d_propEngine.get(); }
280
281
400
theory::QuantifiersEngine* SmtSolver::getQuantifiersEngine()
282
{
283
400
  Assert(d_theoryEngine != nullptr);
284
400
  return d_theoryEngine->getQuantifiersEngine();
285
}
286
287
1947
Preprocessor* SmtSolver::getPreprocessor() { return &d_pp; }
288
289
}  // namespace smt
290
26676
}  // namespace CVC4