GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/smt_engine.cpp Lines: 818 1010 81.0 %
Date: 2021-03-23 Branches: 1235 3371 36.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file smt_engine.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed
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 main entry point into the CVC4 library's SMT interface
13
 **
14
 ** The main entry point into the CVC4 library's SMT interface.
15
 **/
16
17
#include "smt/smt_engine.h"
18
19
#include "api/cvc4cpp.h"
20
#include "base/check.h"
21
#include "base/exception.h"
22
#include "base/modal_exception.h"
23
#include "base/output.h"
24
#include "decision/decision_engine.h"
25
#include "expr/bound_var_manager.h"
26
#include "expr/node.h"
27
#include "options/base_options.h"
28
#include "options/language.h"
29
#include "options/main_options.h"
30
#include "options/printer_options.h"
31
#include "options/proof_options.h"
32
#include "options/smt_options.h"
33
#include "options/theory_options.h"
34
#include "printer/printer.h"
35
#include "proof/proof_manager.h"
36
#include "proof/unsat_core.h"
37
#include "prop/prop_engine.h"
38
#include "smt/abduction_solver.h"
39
#include "smt/abstract_values.h"
40
#include "smt/assertions.h"
41
#include "smt/check_models.h"
42
#include "smt/defined_function.h"
43
#include "smt/dump.h"
44
#include "smt/dump_manager.h"
45
#include "smt/env.h"
46
#include "smt/interpolation_solver.h"
47
#include "smt/listeners.h"
48
#include "smt/logic_exception.h"
49
#include "smt/model_blocker.h"
50
#include "smt/model_core_builder.h"
51
#include "smt/node_command.h"
52
#include "smt/options_manager.h"
53
#include "smt/preprocessor.h"
54
#include "smt/proof_manager.h"
55
#include "smt/quant_elim_solver.h"
56
#include "smt/smt_engine_scope.h"
57
#include "smt/smt_engine_state.h"
58
#include "smt/smt_engine_stats.h"
59
#include "smt/smt_solver.h"
60
#include "smt/sygus_solver.h"
61
#include "smt/unsat_core_manager.h"
62
#include "theory/quantifiers/instantiation_list.h"
63
#include "theory/quantifiers/quantifiers_attributes.h"
64
#include "theory/quantifiers_engine.h"
65
#include "theory/rewriter.h"
66
#include "theory/smt_engine_subsolver.h"
67
#include "theory/theory_engine.h"
68
#include "util/random.h"
69
#include "util/resource_manager.h"
70
71
// required for hacks related to old proofs for unsat cores
72
#include "base/configuration.h"
73
#include "base/configuration_private.h"
74
75
using namespace std;
76
using namespace CVC4::smt;
77
using namespace CVC4::preprocessing;
78
using namespace CVC4::prop;
79
using namespace CVC4::context;
80
using namespace CVC4::theory;
81
82
namespace CVC4 {
83
84
9622
SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
85
9622
    : d_env(new Env(nm)),
86
9622
      d_state(new SmtEngineState(getContext(), getUserContext(), *this)),
87
9622
      d_absValues(new AbstractValues(getNodeManager())),
88
9622
      d_asserts(new Assertions(getUserContext(), *d_absValues.get())),
89
9622
      d_routListener(new ResourceOutListener(*this)),
90
9622
      d_snmListener(new SmtNodeManagerListener(*getDumpManager(), d_outMgr)),
91
      d_smtSolver(nullptr),
92
      d_proofManager(nullptr),
93
      d_model(nullptr),
94
      d_checkModels(nullptr),
95
      d_pfManager(nullptr),
96
      d_ucManager(nullptr),
97
      d_definedFunctions(nullptr),
98
      d_sygusSolver(nullptr),
99
      d_abductSolver(nullptr),
100
      d_interpolSolver(nullptr),
101
      d_quantElimSolver(nullptr),
102
      d_originalOptions(),
103
      d_isInternalSubsolver(false),
104
      d_stats(nullptr),
105
      d_outMgr(this),
106
      d_optm(nullptr),
107
      d_pp(nullptr),
108
67355
      d_scope(nullptr)
109
{
110
  // !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SmtEngine
111
  // we are constructing the current SmtEngine in scope for the lifetime of
112
  // this SmtEngine, or until another SmtEngine is constructed (that SmtEngine
113
  // is then in scope during its lifetime). This is mostly to ensure that
114
  // options are always in scope, for e.g. printing expressions, which rely
115
  // on knowing the output language.
116
  // Notice that the SmtEngine may spawn new SmtEngine "subsolvers" internally.
117
  // These are created, used, and deleted in a modular fashion while not
118
  // interleaving calls to the master SmtEngine. Thus the hack here does not
119
  // break this use case.
120
  // On the other hand, this hack breaks use cases where multiple SmtEngine
121
  // objects are created by the user.
122
9622
  d_scope.reset(new SmtScope(this));
123
  // Set options in the environment, which makes a deep copy of optr if
124
  // non-null. This may throw an options exception.
125
9622
  d_env->setOptions(optr);
126
  // set the options manager
127
9623
  d_optm.reset(new smt::OptionsManager(&getOptions(), getResourceManager()));
128
  // listen to node manager events
129
9621
  getNodeManager()->subscribeEvents(d_snmListener.get());
130
  // listen to resource out
131
9621
  getResourceManager()->registerListener(d_routListener.get());
132
  // make statistics
133
9621
  d_stats.reset(new SmtEngineStatistics());
134
  // reset the preprocessor
135
28863
  d_pp.reset(new smt::Preprocessor(
136
19242
      *this, getUserContext(), *d_absValues.get(), *d_stats));
137
  // make the SMT solver
138
48105
  d_smtSolver.reset(
139
38484
      new SmtSolver(*this, *d_state, getResourceManager(), *d_pp, *d_stats));
140
  // make the SyGuS solver
141
38484
  d_sygusSolver.reset(
142
28863
      new SygusSolver(*d_smtSolver, *d_pp, getUserContext(), d_outMgr));
143
  // make the quantifier elimination solver
144
9621
  d_quantElimSolver.reset(new QuantElimSolver(*d_smtSolver));
145
146
  // The ProofManager is constructed before any other proof objects such as
147
  // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
148
  // initialized in TheoryEngine and PropEngine respectively.
149
9621
  Assert(d_proofManager == nullptr);
150
151
  // d_proofManager must be created before Options has been finished
152
  // being parsed from the input file. Because of this, we cannot trust
153
  // that options::unsatCores() is set correctly yet.
154
#ifdef CVC4_PROOF
155
9621
  d_proofManager.reset(new ProofManager(getUserContext()));
156
#endif
157
158
9621
  d_definedFunctions = new (true) DefinedFunctionMap(getUserContext());
159
9621
}
160
161
24619
bool SmtEngine::isFullyInited() const { return d_state->isFullyInited(); }
162
8784
bool SmtEngine::isQueryMade() const { return d_state->isQueryMade(); }
163
2108
size_t SmtEngine::getNumUserLevels() const
164
{
165
2108
  return d_state->getNumUserLevels();
166
}
167
140
SmtMode SmtEngine::getSmtMode() const { return d_state->getMode(); }
168
116
bool SmtEngine::isSmtModeSat() const
169
{
170
116
  SmtMode mode = getSmtMode();
171
116
  return mode == SmtMode::SAT || mode == SmtMode::SAT_UNKNOWN;
172
}
173
Result SmtEngine::getStatusOfLastCommand() const
174
{
175
  return d_state->getStatus();
176
}
177
226251
context::UserContext* SmtEngine::getUserContext()
178
{
179
226251
  return d_env->getUserContext();
180
}
181
45660
context::Context* SmtEngine::getContext() { return d_env->getContext(); }
182
183
328158
TheoryEngine* SmtEngine::getTheoryEngine()
184
{
185
328158
  return d_smtSolver->getTheoryEngine();
186
}
187
188
43438
prop::PropEngine* SmtEngine::getPropEngine()
189
{
190
43438
  return d_smtSolver->getPropEngine();
191
}
192
193
109448
void SmtEngine::finishInit()
194
{
195
109448
  if (d_state->isFullyInited())
196
  {
197
    // already initialized, return
198
100451
    return;
199
  }
200
201
  // Notice that finishInitInternal is called when options are finalized. If we
202
  // are parsing smt2, this occurs at the moment we enter "Assert mode", page 52
203
  // of SMT-LIB 2.6 standard.
204
205
  // set the logic
206
8997
  const LogicInfo& logic = getLogicInfo();
207
8997
  if (!logic.isLocked())
208
  {
209
1267
    setLogicInternal();
210
  }
211
212
  // set the random seed
213
8997
  Random::getRandom().setSeed(options::seed());
214
215
  // Call finish init on the options manager. This inializes the resource
216
  // manager based on the options, and sets up the best default options
217
  // based on our heuristics.
218
8997
  d_optm->finishInit(d_env->d_logic, d_isInternalSubsolver);
219
220
8997
  ProofNodeManager* pnm = nullptr;
221
8997
  if (options::produceProofs())
222
  {
223
    // ensure bound variable uses canonical bound variables
224
962
    getNodeManager()->getBoundVarManager()->enableKeepCacheValues();
225
    // make the proof manager
226
962
    d_pfManager.reset(new PfManager(getUserContext(), this));
227
962
    PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator();
228
    // start the unsat core manager
229
962
    d_ucManager.reset(new UnsatCoreManager());
230
    // use this proof node manager
231
962
    pnm = d_pfManager->getProofNodeManager();
232
    // enable proof support in the environment/rewriter
233
962
    d_env->setProofNodeManager(pnm);
234
    // enable it in the assertions pipeline
235
962
    d_asserts->setProofGenerator(pppg);
236
    // enable it in the SmtSolver
237
962
    d_smtSolver->setProofNodeManager(pnm);
238
    // enabled proofs in the preprocessor
239
962
    d_pp->setProofGenerator(pppg);
240
  }
241
242
8997
  Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
243
8997
  d_smtSolver->finishInit(logic);
244
245
  // now can construct the SMT-level model object
246
8997
  TheoryEngine* te = d_smtSolver->getTheoryEngine();
247
8997
  Assert(te != nullptr);
248
8997
  TheoryModel* tm = te->getModel();
249
8997
  if (tm != nullptr)
250
  {
251
8997
    d_model.reset(new Model(tm));
252
    // make the check models utility
253
8997
    d_checkModels.reset(new CheckModels(*d_smtSolver.get()));
254
  }
255
256
  // global push/pop around everything, to ensure proper destruction
257
  // of context-dependent data structures
258
8997
  d_state->setup();
259
260
8997
  Trace("smt-debug") << "Set up assertions..." << std::endl;
261
8997
  d_asserts->finishInit();
262
263
  // dump out a set-logic command only when raw-benchmark is disabled to avoid
264
  // dumping the command twice.
265
8997
  if (Dump.isOn("benchmark") && !Dump.isOn("raw-benchmark"))
266
  {
267
2
      LogicInfo everything;
268
1
      everything.lock();
269
3
      getPrinter().toStreamCmdComment(
270
1
          getOutputManager().getDumpOut(),
271
          "CVC4 always dumps the most general, all-supported logic (below), as "
272
          "some internals might require the use of a logic more general than "
273
1
          "the input.");
274
2
      getPrinter().toStreamCmdSetBenchmarkLogic(getOutputManager().getDumpOut(),
275
2
                                                everything.getLogicString());
276
  }
277
278
  // initialize the dump manager
279
8997
  getDumpManager()->finishInit();
280
281
  // subsolvers
282
8997
  if (options::produceAbducts())
283
  {
284
596
    d_abductSolver.reset(new AbductionSolver(this));
285
  }
286
8997
  if (options::produceInterpols() != options::ProduceInterpols::NONE)
287
  {
288
73
    d_interpolSolver.reset(new InterpolationSolver(this));
289
  }
290
291
8997
  d_pp->finishInit();
292
293
8997
  AlwaysAssert(getPropEngine()->getAssertionLevel() == 0)
294
      << "The PropEngine has pushed but the SmtEngine "
295
         "hasn't finished initializing!";
296
297
8997
  Assert(getLogicInfo().isLocked());
298
299
  // store that we are finished initializing
300
8997
  d_state->finishInit();
301
8997
  Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl;
302
}
303
304
9600
void SmtEngine::shutdown() {
305
9600
  d_state->shutdown();
306
307
9600
  d_smtSolver->shutdown();
308
309
9600
  d_env->shutdown();
310
9600
}
311
312
19200
SmtEngine::~SmtEngine()
313
{
314
19200
  SmtScope smts(this);
315
316
  try {
317
9600
    shutdown();
318
319
    // global push/pop around everything, to ensure proper destruction
320
    // of context-dependent data structures
321
9600
    d_state->cleanup();
322
323
9600
    d_definedFunctions->deleteSelf();
324
325
    //destroy all passes before destroying things that they refer to
326
9600
    d_pp->cleanup();
327
328
    // d_proofManager is always created when proofs are enabled at configure
329
    // time.  Because of this, this code should not be wrapped in PROOF() which
330
    // additionally checks flags such as options::produceProofs().
331
    //
332
    // Note: the proof manager must be destroyed before the theory engine.
333
    // Because the destruction of the proofs depends on contexts owned be the
334
    // theory solvers.
335
#ifdef CVC4_PROOF
336
9600
    d_proofManager.reset(nullptr);
337
#endif
338
9600
    d_pfManager.reset(nullptr);
339
9600
    d_ucManager.reset(nullptr);
340
341
9600
    d_absValues.reset(nullptr);
342
9600
    d_asserts.reset(nullptr);
343
9600
    d_model.reset(nullptr);
344
345
9600
    d_sygusSolver.reset(nullptr);
346
347
9600
    d_smtSolver.reset(nullptr);
348
349
9600
    d_stats.reset(nullptr);
350
9600
    getNodeManager()->unsubscribeEvents(d_snmListener.get());
351
9600
    d_snmListener.reset(nullptr);
352
9600
    d_routListener.reset(nullptr);
353
9600
    d_optm.reset(nullptr);
354
9600
    d_pp.reset(nullptr);
355
    // destroy the state
356
9600
    d_state.reset(nullptr);
357
    // destroy the environment
358
9600
    d_env.reset(nullptr);
359
  } catch(Exception& e) {
360
    Warning() << "CVC4 threw an exception during cleanup." << endl
361
              << e << endl;
362
  }
363
9600
}
364
365
7785
void SmtEngine::setLogic(const LogicInfo& logic)
366
{
367
15570
  SmtScope smts(this);
368
7785
  if (d_state->isFullyInited())
369
  {
370
    throw ModalException("Cannot set logic in SmtEngine after the engine has "
371
                         "finished initializing.");
372
  }
373
7785
  d_env->d_logic = logic;
374
7785
  d_userLogic = logic;
375
7785
  setLogicInternal();
376
7785
}
377
378
2
void SmtEngine::setLogic(const std::string& s)
379
{
380
4
  SmtScope smts(this);
381
  try
382
  {
383
2
    setLogic(LogicInfo(s));
384
    // dump out a set-logic command
385
2
    if (Dump.isOn("raw-benchmark"))
386
    {
387
      getPrinter().toStreamCmdSetBenchmarkLogic(
388
          getOutputManager().getDumpOut(), getLogicInfo().getLogicString());
389
    }
390
  }
391
  catch (IllegalArgumentException& e)
392
  {
393
    throw LogicException(e.what());
394
  }
395
2
}
396
397
2
void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); }
398
399
41481
const LogicInfo& SmtEngine::getLogicInfo() const
400
{
401
41481
  return d_env->getLogicInfo();
402
}
403
404
389
LogicInfo SmtEngine::getUserLogicInfo() const
405
{
406
  // Lock the logic to make sure that this logic can be queried. We create a
407
  // copy of the user logic here to keep this method const.
408
389
  LogicInfo res = d_userLogic;
409
389
  res.lock();
410
389
  return res;
411
}
412
413
5504
void SmtEngine::notifyStartParsing(const std::string& filename)
414
{
415
5504
  d_state->setFilename(filename);
416
5504
  d_stats->d_driverFilename.set(filename);
417
  // Copy the original options. This is called prior to beginning parsing.
418
  // Hence reset should revert to these options, which note is after reading
419
  // the command line.
420
5504
  d_originalOptions.copyValues(getOptions());
421
5504
}
422
423
const std::string& SmtEngine::getFilename() const
424
{
425
  return d_state->getFilename();
426
}
427
428
5436
void SmtEngine::setResultStatistic(const std::string& result) {
429
5436
    d_stats->d_driverResult.set(result);
430
5436
}
431
432
5436
void SmtEngine::setTotalTimeStatistic(double seconds) {
433
5436
  d_stats->d_driverTotalTime.set(seconds);
434
5436
}
435
436
9052
void SmtEngine::setLogicInternal()
437
{
438
9052
  Assert(!d_state->isFullyInited())
439
      << "setting logic in SmtEngine but the engine has already"
440
         " finished initializing for this run";
441
9052
  d_env->d_logic.lock();
442
9052
  d_userLogic.lock();
443
9052
}
444
445
5388
void SmtEngine::setInfo(const std::string& key, const std::string& value)
446
{
447
10776
  SmtScope smts(this);
448
449
5388
  Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
450
451
5388
  if (Dump.isOn("benchmark"))
452
  {
453
    if (key == "status")
454
    {
455
      Result::Sat status =
456
          (value == "sat")
457
              ? Result::SAT
458
              : ((value == "unsat") ? Result::UNSAT : Result::SAT_UNKNOWN);
459
      getPrinter().toStreamCmdSetBenchmarkStatus(
460
          getOutputManager().getDumpOut(), status);
461
    }
462
    else
463
    {
464
      getPrinter().toStreamCmdSetInfo(
465
          getOutputManager().getDumpOut(), key, value);
466
    }
467
  }
468
469
5388
  if (key == "filename")
470
  {
471
55
    d_state->setFilename(value);
472
  }
473
5333
  else if (key == "smt-lib-version" && !options::inputLanguage.wasSetByUser())
474
  {
475
664
    language::input::Language ilang = language::input::LANG_SMTLIB_V2_6;
476
477
664
    if (value != "2" && value != "2.6")
478
    {
479
8
      Warning() << "SMT-LIB version " << value
480
                << " unsupported, defaulting to language (and semantics of) "
481
4
                   "SMT-LIB 2.6\n";
482
    }
483
664
    options::inputLanguage.set(ilang);
484
    // also update the output language
485
664
    if (!options::outputLanguage.wasSetByUser())
486
    {
487
664
      language::output::Language olang = language::toOutputLanguage(ilang);
488
664
      if (options::outputLanguage() != olang)
489
      {
490
2
        options::outputLanguage.set(olang);
491
2
        *options::out() << language::SetLanguage(olang);
492
      }
493
    }
494
  }
495
4669
  else if (key == "status")
496
  {
497
3390
    d_state->notifyExpectedStatus(value);
498
  }
499
5388
}
500
501
23
bool SmtEngine::isValidGetInfoFlag(const std::string& key) const
502
{
503
68
  if (key == "all-statistics" || key == "error-behavior" || key == "name"
504
18
      || key == "version" || key == "authors" || key == "status"
505
15
      || key == "reason-unknown" || key == "assertion-stack-levels"
506
29
      || key == "all-options" || key == "time")
507
  {
508
17
    return true;
509
  }
510
6
  return false;
511
}
512
513
17
CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
514
{
515
34
  SmtScope smts(this);
516
517
17
  Trace("smt") << "SMT getInfo(" << key << ")" << endl;
518
17
  if (key == "all-statistics")
519
  {
520
2
    vector<SExpr> stats;
521
39
    for (StatisticsRegistry::const_iterator i = d_env->getStatisticsRegistry()->begin();
522
39
         i != d_env->getStatisticsRegistry()->end();
523
         ++i)
524
    {
525
76
      vector<SExpr> v;
526
38
      v.push_back((*i).first);
527
38
      v.push_back((*i).second);
528
38
      stats.push_back(v);
529
    }
530
1
    return SExpr(stats);
531
  }
532
16
  if (key == "error-behavior")
533
  {
534
1
    return SExpr(SExpr::Keyword("immediate-exit"));
535
  }
536
15
  if (key == "name")
537
  {
538
3
    return SExpr(Configuration::getName());
539
  }
540
12
  if (key == "version")
541
  {
542
1
    return SExpr(Configuration::getVersionString());
543
  }
544
11
  if (key == "authors")
545
  {
546
1
    return SExpr(Configuration::about());
547
  }
548
10
  if (key == "status")
549
  {
550
    // sat | unsat | unknown
551
2
    Result status = d_state->getStatus();
552
1
    switch (status.asSatisfiabilityResult().isSat())
553
    {
554
      case Result::SAT: return SExpr(SExpr::Keyword("sat"));
555
      case Result::UNSAT: return SExpr(SExpr::Keyword("unsat"));
556
1
      default: return SExpr(SExpr::Keyword("unknown"));
557
    }
558
  }
559
9
  if (key == "time")
560
  {
561
    return SExpr(std::clock());
562
  }
563
9
  if (key == "reason-unknown")
564
  {
565
18
    Result status = d_state->getStatus();
566
9
    if (!status.isNull() && status.isUnknown())
567
    {
568
12
      std::stringstream ss;
569
6
      ss << status.whyUnknown();
570
12
      string s = ss.str();
571
6
      transform(s.begin(), s.end(), s.begin(), ::tolower);
572
6
      return SExpr(SExpr::Keyword(s));
573
    }
574
    else
575
    {
576
      throw RecoverableModalException(
577
          "Can't get-info :reason-unknown when the "
578
3
          "last result wasn't unknown!");
579
    }
580
  }
581
  if (key == "assertion-stack-levels")
582
  {
583
    size_t ulevel = d_state->getNumUserLevels();
584
    AlwaysAssert(ulevel <= std::numeric_limits<unsigned long int>::max());
585
    return SExpr(static_cast<unsigned long int>(ulevel));
586
  }
587
  Assert(key == "all-options");
588
  // get the options, like all-statistics
589
  std::vector<std::vector<std::string>> current_options =
590
      Options::current()->getOptions();
591
  return SExpr::parseListOfListOfAtoms(current_options);
592
}
593
594
2896
void SmtEngine::debugCheckFormals(const std::vector<Node>& formals, Node func)
595
{
596
7555
  for (std::vector<Node>::const_iterator i = formals.begin();
597
7555
       i != formals.end();
598
       ++i)
599
  {
600
4659
    if((*i).getKind() != kind::BOUND_VARIABLE) {
601
      stringstream ss;
602
      ss << "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n"
603
         << "definition of function " << func << ", formal\n"
604
         << "  " << *i << "\n"
605
         << "has kind " << (*i).getKind();
606
      throw TypeCheckingExceptionPrivate(func, ss.str());
607
    }
608
  }
609
2896
}
610
611
2896
void SmtEngine::debugCheckFunctionBody(Node formula,
612
                                       const std::vector<Node>& formals,
613
                                       Node func)
614
{
615
5792
  TypeNode formulaType = formula.getType(options::typeChecking());
616
5792
  TypeNode funcType = func.getType();
617
  // We distinguish here between definitions of constants and functions,
618
  // because the type checking for them is subtly different.  Perhaps we
619
  // should instead have SmtEngine::defineFunction() and
620
  // SmtEngine::defineConstant() for better clarity, although then that
621
  // doesn't match the SMT-LIBv2 standard...
622
2896
  if(formals.size() > 0) {
623
3326
    TypeNode rangeType = funcType.getRangeType();
624
1663
    if(! formulaType.isComparableTo(rangeType)) {
625
      stringstream ss;
626
      ss << "Type of defined function does not match its declaration\n"
627
         << "The function  : " << func << "\n"
628
         << "Declared type : " << rangeType << "\n"
629
         << "The body      : " << formula << "\n"
630
         << "Body type     : " << formulaType;
631
      throw TypeCheckingExceptionPrivate(func, ss.str());
632
    }
633
  } else {
634
1233
    if(! formulaType.isComparableTo(funcType)) {
635
      stringstream ss;
636
      ss << "Declared type of defined constant does not match its definition\n"
637
         << "The constant   : " << func << "\n"
638
         << "Declared type  : " << funcType << "\n"
639
         << "The definition : " << formula << "\n"
640
         << "Definition type: " << formulaType;
641
      throw TypeCheckingExceptionPrivate(func, ss.str());
642
    }
643
  }
644
2896
}
645
646
2700
void SmtEngine::defineFunction(Node func,
647
                               const std::vector<Node>& formals,
648
                               Node formula,
649
                               bool global)
650
{
651
5400
  SmtScope smts(this);
652
2700
  finishInit();
653
2700
  d_state->doPendingPops();
654
2700
  Trace("smt") << "SMT defineFunction(" << func << ")" << endl;
655
2700
  debugCheckFormals(formals, func);
656
657
5400
  stringstream ss;
658
  ss << language::SetLanguage(
659
            language::SetLanguage::getLanguage(Dump.getStream()))
660
2700
     << func;
661
5400
  std::vector<Node> nFormals;
662
2700
  nFormals.reserve(formals.size());
663
664
6951
  for (const Node& formal : formals)
665
  {
666
4251
    nFormals.push_back(formal);
667
  }
668
669
5400
  DefineFunctionNodeCommand nc(ss.str(), func, nFormals, formula);
670
2700
  getDumpManager()->addToDump(nc, "declarations");
671
672
  // type check body
673
2700
  debugCheckFunctionBody(formula, formals, func);
674
675
  // Substitute out any abstract values in formula
676
5400
  Node formNode = d_absValues->substituteAbstractValues(formula);
677
5400
  DefinedFunction def(func, formals, formNode);
678
  // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
679
  // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
680
  // d_haveAdditions = true;
681
2700
  Debug("smt") << "definedFunctions insert " << func << " " << formNode << endl;
682
683
2700
  if (global)
684
  {
685
377
    d_definedFunctions->insertAtContextLevelZero(func, def);
686
  }
687
  else
688
  {
689
2323
    d_definedFunctions->insert(func, def);
690
  }
691
2700
}
692
693
138
void SmtEngine::defineFunctionsRec(
694
    const std::vector<Node>& funcs,
695
    const std::vector<std::vector<Node>>& formals,
696
    const std::vector<Node>& formulas,
697
    bool global)
698
{
699
276
  SmtScope smts(this);
700
138
  finishInit();
701
138
  d_state->doPendingPops();
702
138
  Trace("smt") << "SMT defineFunctionsRec(...)" << endl;
703
704
138
  if (funcs.size() != formals.size() && funcs.size() != formulas.size())
705
  {
706
    stringstream ss;
707
    ss << "Number of functions, formals, and function bodies passed to "
708
          "defineFunctionsRec do not match:"
709
       << "\n"
710
       << "        #functions : " << funcs.size() << "\n"
711
       << "        #arg lists : " << formals.size() << "\n"
712
       << "  #function bodies : " << formulas.size() << "\n";
713
    throw ModalException(ss.str());
714
  }
715
334
  for (unsigned i = 0, size = funcs.size(); i < size; i++)
716
  {
717
    // check formal argument list
718
196
    debugCheckFormals(formals[i], funcs[i]);
719
    // type check body
720
196
    debugCheckFunctionBody(formulas[i], formals[i], funcs[i]);
721
  }
722
723
138
  if (Dump.isOn("raw-benchmark"))
724
  {
725
    getPrinter().toStreamCmdDefineFunctionRec(
726
        getOutputManager().getDumpOut(), funcs, formals, formulas);
727
  }
728
729
138
  NodeManager* nm = getNodeManager();
730
334
  for (unsigned i = 0, size = funcs.size(); i < size; i++)
731
  {
732
    // we assert a quantified formula
733
392
    Node func_app;
734
    // make the function application
735
196
    if (formals[i].empty())
736
    {
737
      // it has no arguments
738
21
      func_app = funcs[i];
739
    }
740
    else
741
    {
742
350
      std::vector<Node> children;
743
175
      children.push_back(funcs[i]);
744
175
      children.insert(children.end(), formals[i].begin(), formals[i].end());
745
175
      func_app = nm->mkNode(kind::APPLY_UF, children);
746
    }
747
392
    Node lem = nm->mkNode(kind::EQUAL, func_app, formulas[i]);
748
196
    if (!formals[i].empty())
749
    {
750
      // set the attribute to denote this is a function definition
751
350
      Node aexpr = nm->mkNode(kind::INST_ATTRIBUTE, func_app);
752
175
      aexpr = nm->mkNode(kind::INST_PATTERN_LIST, aexpr);
753
      FunDefAttribute fda;
754
175
      func_app.setAttribute(fda, true);
755
      // make the quantified formula
756
350
      Node boundVars = nm->mkNode(kind::BOUND_VAR_LIST, formals[i]);
757
175
      lem = nm->mkNode(kind::FORALL, boundVars, lem, aexpr);
758
    }
759
    // assert the quantified formula
760
    //   notice we don't call assertFormula directly, since this would
761
    //   duplicate the output on raw-benchmark.
762
    // add define recursive definition to the assertions
763
196
    d_asserts->addDefineFunRecDefinition(lem, global);
764
  }
765
138
}
766
767
16
void SmtEngine::defineFunctionRec(Node func,
768
                                  const std::vector<Node>& formals,
769
                                  Node formula,
770
                                  bool global)
771
{
772
32
  std::vector<Node> funcs;
773
16
  funcs.push_back(func);
774
32
  std::vector<std::vector<Node>> formals_multi;
775
16
  formals_multi.push_back(formals);
776
32
  std::vector<Node> formulas;
777
16
  formulas.push_back(formula);
778
16
  defineFunctionsRec(funcs, formals_multi, formulas, global);
779
16
}
780
781
138734
bool SmtEngine::isDefinedFunction(Node func)
782
{
783
138734
  Debug("smt") << "isDefined function " << func << "?" << std::endl;
784
138734
  return d_definedFunctions->find(func) != d_definedFunctions->end();
785
}
786
787
79466
Result SmtEngine::quickCheck() {
788
79466
  Assert(d_state->isFullyInited());
789
79466
  Trace("smt") << "SMT quickCheck()" << endl;
790
79466
  const std::string& filename = d_state->getFilename();
791
  return Result(
792
79466
      Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename);
793
}
794
795
5752
Model* SmtEngine::getAvailableModel(const char* c) const
796
{
797
5752
  if (!options::assignFunctionValues())
798
  {
799
    std::stringstream ss;
800
    ss << "Cannot " << c << " when --assign-function-values is false.";
801
    throw RecoverableModalException(ss.str().c_str());
802
  }
803
804
11504
  if (d_state->getMode() != SmtMode::SAT
805
5752
      && d_state->getMode() != SmtMode::SAT_UNKNOWN)
806
  {
807
14
    std::stringstream ss;
808
    ss << "Cannot " << c
809
7
       << " unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN "
810
7
          "response.";
811
7
    throw RecoverableModalException(ss.str().c_str());
812
  }
813
814
5745
  if (!options::produceModels())
815
  {
816
4
    std::stringstream ss;
817
2
    ss << "Cannot " << c << " when produce-models options is off.";
818
2
    throw ModalException(ss.str().c_str());
819
  }
820
821
5743
  TheoryEngine* te = d_smtSolver->getTheoryEngine();
822
5743
  Assert(te != nullptr);
823
5743
  TheoryModel* m = te->getBuiltModel();
824
825
5742
  if (m == nullptr)
826
  {
827
    std::stringstream ss;
828
    ss << "Cannot " << c
829
       << " since model is not available. Perhaps the most recent call to "
830
          "check-sat was interrupted?";
831
    throw RecoverableModalException(ss.str().c_str());
832
  }
833
834
5742
  return d_model.get();
835
}
836
837
146
QuantifiersEngine* SmtEngine::getAvailableQuantifiersEngine(const char* c) const
838
{
839
146
  QuantifiersEngine* qe = d_smtSolver->getQuantifiersEngine();
840
146
  if (qe == nullptr)
841
  {
842
    std::stringstream ss;
843
    ss << "Cannot " << c << " when quantifiers are not present.";
844
    throw ModalException(ss.str().c_str());
845
  }
846
146
  return qe;
847
}
848
849
3190
void SmtEngine::notifyPushPre() { d_smtSolver->processAssertions(*d_asserts); }
850
851
3190
void SmtEngine::notifyPushPost()
852
{
853
6380
  TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
854
3190
  Assert(getPropEngine() != nullptr);
855
3190
  getPropEngine()->push();
856
3190
}
857
858
3190
void SmtEngine::notifyPopPre()
859
{
860
6380
  TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
861
3190
  PropEngine* pe = getPropEngine();
862
3190
  Assert(pe != nullptr);
863
3190
  pe->pop();
864
3190
}
865
866
12401
void SmtEngine::notifyPostSolvePre()
867
{
868
12401
  PropEngine* pe = getPropEngine();
869
12401
  Assert(pe != nullptr);
870
12401
  pe->resetTrail();
871
12401
}
872
873
12401
void SmtEngine::notifyPostSolvePost()
874
{
875
12401
  TheoryEngine* te = getTheoryEngine();
876
12401
  Assert(te != nullptr);
877
12401
  te->postsolve();
878
12401
}
879
880
10244
Result SmtEngine::checkSat()
881
{
882
20488
  Node nullNode;
883
20469
  return checkSat(nullNode);
884
}
885
886
10804
Result SmtEngine::checkSat(const Node& assumption, bool inUnsatCore)
887
{
888
10804
  if (Dump.isOn("benchmark"))
889
  {
890
4
    getPrinter().toStreamCmdCheckSat(getOutputManager().getDumpOut(),
891
2
                                     assumption);
892
  }
893
21608
  std::vector<Node> assump;
894
10804
  if (!assumption.isNull())
895
  {
896
560
    assump.push_back(assumption);
897
  }
898
21588
  return checkSatInternal(assump, inUnsatCore, false);
899
}
900
901
984
Result SmtEngine::checkSat(const std::vector<Node>& assumptions,
902
                           bool inUnsatCore)
903
{
904
984
  if (Dump.isOn("benchmark"))
905
  {
906
    if (assumptions.empty())
907
    {
908
      getPrinter().toStreamCmdCheckSat(getOutputManager().getDumpOut());
909
    }
910
    else
911
    {
912
      getPrinter().toStreamCmdCheckSatAssuming(getOutputManager().getDumpOut(),
913
                                               assumptions);
914
    }
915
  }
916
984
  return checkSatInternal(assumptions, inUnsatCore, false);
917
}
918
919
243
Result SmtEngine::checkEntailed(const Node& node, bool inUnsatCore)
920
{
921
243
  if (Dump.isOn("benchmark"))
922
  {
923
    getPrinter().toStreamCmdQuery(getOutputManager().getDumpOut(), node);
924
  }
925
725
  return checkSatInternal(
926
486
             node.isNull() ? std::vector<Node>() : std::vector<Node>{node},
927
             inUnsatCore,
928
             true)
929
478
      .asEntailmentResult();
930
}
931
932
2
Result SmtEngine::checkEntailed(const std::vector<Node>& nodes,
933
                                bool inUnsatCore)
934
{
935
2
  return checkSatInternal(nodes, inUnsatCore, true).asEntailmentResult();
936
}
937
938
12033
Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
939
                                   bool inUnsatCore,
940
                                   bool isEntailmentCheck)
941
{
942
  try
943
  {
944
24066
    SmtScope smts(this);
945
12033
    finishInit();
946
947
24066
    Trace("smt") << "SmtEngine::"
948
24066
                 << (isEntailmentCheck ? "checkEntailed" : "checkSat") << "("
949
12033
                 << assumptions << ")" << endl;
950
    // check the satisfiability with the solver object
951
    Result r = d_smtSolver->checkSatisfiability(
952
24044
        *d_asserts.get(), assumptions, inUnsatCore, isEntailmentCheck);
953
954
24022
    Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat")
955
12011
                 << "(" << assumptions << ") => " << r << endl;
956
957
    // Check that SAT results generate a model correctly.
958
12011
    if(options::checkModels()) {
959
2312
      if (r.asSatisfiabilityResult().isSat() == Result::SAT)
960
      {
961
1950
        checkModel();
962
      }
963
    }
964
    // Check that UNSAT results generate a proof correctly.
965
12009
    if (options::checkProofs() || options::proofEagerChecking())
966
    {
967
1950
      if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
968
      {
969
2284
        if ((options::checkProofs() || options::proofEagerChecking())
970
2284
            && !options::produceProofs())
971
        {
972
          throw ModalException(
973
              "Cannot check-proofs because proofs were disabled.");
974
        }
975
1142
        checkProof();
976
      }
977
    }
978
    // Check that UNSAT results generate an unsat core correctly.
979
12009
    if (options::checkUnsatCores() || options::checkUnsatCoresNew())
980
    {
981
946
      if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
982
      {
983
1680
        TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime);
984
840
        checkUnsatCore();
985
      }
986
    }
987
988
12009
    return r;
989
  }
990
  catch (UnsafeInterruptException& e)
991
  {
992
    AlwaysAssert(getResourceManager()->out());
993
    // Notice that we do not notify the state of this result. If we wanted to
994
    // make the solver resume a working state after an interupt, then we would
995
    // implement a different callback and use it here, e.g.
996
    // d_state.notifyCheckSatInterupt.
997
    Result::UnknownExplanation why = getResourceManager()->outOfResources()
998
                                         ? Result::RESOURCEOUT
999
                                         : Result::TIMEOUT;
1000
    return Result(Result::SAT_UNKNOWN, why, d_state->getFilename());
1001
  }
1002
}
1003
1004
8
std::vector<Node> SmtEngine::getUnsatAssumptions(void)
1005
{
1006
8
  Trace("smt") << "SMT getUnsatAssumptions()" << endl;
1007
16
  SmtScope smts(this);
1008
8
  if (!options::unsatAssumptions())
1009
  {
1010
    throw ModalException(
1011
        "Cannot get unsat assumptions when produce-unsat-assumptions option "
1012
        "is off.");
1013
  }
1014
8
  if (d_state->getMode() != SmtMode::UNSAT)
1015
  {
1016
    throw RecoverableModalException(
1017
        "Cannot get unsat assumptions unless immediately preceded by "
1018
        "UNSAT/ENTAILED.");
1019
  }
1020
8
  finishInit();
1021
8
  if (Dump.isOn("benchmark"))
1022
  {
1023
    getPrinter().toStreamCmdGetUnsatAssumptions(
1024
        getOutputManager().getDumpOut());
1025
  }
1026
16
  UnsatCore core = getUnsatCoreInternal();
1027
8
  std::vector<Node> res;
1028
8
  std::vector<Node>& assumps = d_asserts->getAssumptions();
1029
24
  for (const Node& e : assumps)
1030
  {
1031
16
    if (std::find(core.begin(), core.end(), e) != core.end())
1032
    {
1033
10
      res.push_back(e);
1034
    }
1035
  }
1036
16
  return res;
1037
}
1038
1039
79466
Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore)
1040
{
1041
158932
  SmtScope smts(this);
1042
79466
  finishInit();
1043
79466
  d_state->doPendingPops();
1044
1045
79466
  Trace("smt") << "SmtEngine::assertFormula(" << formula << ")" << endl;
1046
1047
79466
  if (Dump.isOn("raw-benchmark"))
1048
  {
1049
3
    getPrinter().toStreamCmdAssert(getOutputManager().getDumpOut(), formula);
1050
  }
1051
1052
  // Substitute out any abstract values in ex
1053
158932
  Node n = d_absValues->substituteAbstractValues(formula);
1054
1055
79466
  d_asserts->assertFormula(n, inUnsatCore);
1056
158932
  return quickCheck().asEntailmentResult();
1057
}/* SmtEngine::assertFormula() */
1058
1059
/*
1060
   --------------------------------------------------------------------------
1061
    Handling SyGuS commands
1062
   --------------------------------------------------------------------------
1063
*/
1064
1065
683
void SmtEngine::declareSygusVar(Node var)
1066
{
1067
1366
  SmtScope smts(this);
1068
683
  d_sygusSolver->declareSygusVar(var);
1069
683
  if (Dump.isOn("raw-benchmark"))
1070
  {
1071
    getPrinter().toStreamCmdDeclareVar(
1072
        getOutputManager().getDumpOut(), var, var.getType());
1073
  }
1074
  // don't need to set that the conjecture is stale
1075
683
}
1076
1077
575
void SmtEngine::declareSynthFun(Node func,
1078
                                TypeNode sygusType,
1079
                                bool isInv,
1080
                                const std::vector<Node>& vars)
1081
{
1082
1150
  SmtScope smts(this);
1083
575
  d_state->doPendingPops();
1084
575
  d_sygusSolver->declareSynthFun(func, sygusType, isInv, vars);
1085
1086
  // !!! TEMPORARY: We cannot construct a SynthFunCommand since we cannot
1087
  // construct a Term-level Grammar from a Node-level sygus TypeNode. Thus we
1088
  // must print the command using the Node-level utility method for now.
1089
1090
575
  if (Dump.isOn("raw-benchmark"))
1091
  {
1092
    getPrinter().toStreamCmdSynthFun(
1093
        getOutputManager().getDumpOut(), func, vars, isInv, sygusType);
1094
  }
1095
575
}
1096
void SmtEngine::declareSynthFun(Node func,
1097
                                bool isInv,
1098
                                const std::vector<Node>& vars)
1099
{
1100
  // use a null sygus type
1101
  TypeNode sygusType;
1102
  declareSynthFun(func, sygusType, isInv, vars);
1103
}
1104
1105
1201
void SmtEngine::assertSygusConstraint(Node constraint)
1106
{
1107
2402
  SmtScope smts(this);
1108
1201
  finishInit();
1109
1201
  d_sygusSolver->assertSygusConstraint(constraint);
1110
1201
  if (Dump.isOn("raw-benchmark"))
1111
  {
1112
    getPrinter().toStreamCmdConstraint(getOutputManager().getDumpOut(),
1113
                                       constraint);
1114
  }
1115
1201
}
1116
1117
31
void SmtEngine::assertSygusInvConstraint(Node inv,
1118
                                         Node pre,
1119
                                         Node trans,
1120
                                         Node post)
1121
{
1122
62
  SmtScope smts(this);
1123
31
  finishInit();
1124
31
  d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post);
1125
31
  if (Dump.isOn("raw-benchmark"))
1126
  {
1127
    getPrinter().toStreamCmdInvConstraint(
1128
        getOutputManager().getDumpOut(), inv, pre, trans, post);
1129
  }
1130
31
}
1131
1132
372
Result SmtEngine::checkSynth()
1133
{
1134
744
  SmtScope smts(this);
1135
372
  finishInit();
1136
732
  return d_sygusSolver->checkSynth(*d_asserts);
1137
}
1138
1139
/*
1140
   --------------------------------------------------------------------------
1141
    End of Handling SyGuS commands
1142
   --------------------------------------------------------------------------
1143
*/
1144
1145
58
Node SmtEngine::simplify(const Node& ex)
1146
{
1147
116
  SmtScope smts(this);
1148
58
  finishInit();
1149
58
  d_state->doPendingPops();
1150
  // ensure we've processed assertions
1151
58
  d_smtSolver->processAssertions(*d_asserts);
1152
116
  return d_pp->simplify(ex);
1153
}
1154
1155
5698
Node SmtEngine::expandDefinitions(const Node& ex, bool expandOnly)
1156
{
1157
5698
  getResourceManager()->spendResource(
1158
      ResourceManager::Resource::PreprocessStep);
1159
1160
11396
  SmtScope smts(this);
1161
5698
  finishInit();
1162
5698
  d_state->doPendingPops();
1163
11396
  return d_pp->expandDefinitions(ex, expandOnly);
1164
}
1165
1166
// TODO(#1108): Simplify the error reporting of this method.
1167
3740
Node SmtEngine::getValue(const Node& ex) const
1168
{
1169
7480
  SmtScope smts(this);
1170
1171
3740
  Trace("smt") << "SMT getValue(" << ex << ")" << endl;
1172
3740
  if (Dump.isOn("benchmark"))
1173
  {
1174
    getPrinter().toStreamCmdGetValue(d_outMgr.getDumpOut(), {ex});
1175
  }
1176
7480
  TypeNode expectedType = ex.getType();
1177
1178
  // Substitute out any abstract values in ex and expand
1179
7480
  Node n = d_pp->expandDefinitions(ex);
1180
1181
3740
  Trace("smt") << "--- getting value of " << n << endl;
1182
  // There are two ways model values for terms are computed (for historical
1183
  // reasons).  One way is that used in check-model; the other is that
1184
  // used by the Model classes.  It's not clear to me exactly how these
1185
  // two are different, but they need to be unified.  This ugly hack here
1186
  // is to fix bug 554 until we can revamp boolean-terms and models [MGD]
1187
1188
  //AJR : necessary?
1189
3740
  if(!n.getType().isFunction()) {
1190
3730
    n = Rewriter::rewrite(n);
1191
  }
1192
1193
3740
  Trace("smt") << "--- getting value of " << n << endl;
1194
3740
  Model* m = getAvailableModel("get-value");
1195
3734
  Assert(m != nullptr);
1196
3734
  Node resultNode = m->getValue(n);
1197
3734
  Trace("smt") << "--- got value " << n << " = " << resultNode << endl;
1198
3734
  Trace("smt") << "--- type " << resultNode.getType() << endl;
1199
3734
  Trace("smt") << "--- expected type " << expectedType << endl;
1200
1201
  // type-check the result we got
1202
  // Notice that lambdas have function type, which does not respect the subtype
1203
  // relation, so we ignore them here.
1204
3734
  Assert(resultNode.isNull() || resultNode.getKind() == kind::LAMBDA
1205
         || resultNode.getType().isSubtypeOf(expectedType))
1206
      << "Run with -t smt for details.";
1207
1208
  // Ensure it's a constant, or a lambda (for uninterpreted functions). This
1209
  // assertion only holds for models that do not have approximate values.
1210
3734
  Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA
1211
         || resultNode.isConst());
1212
1213
3734
  if(options::abstractValues() && resultNode.getType().isArray()) {
1214
8
    resultNode = d_absValues->mkAbstractValue(resultNode);
1215
8
    Trace("smt") << "--- abstract value >> " << resultNode << endl;
1216
  }
1217
1218
7468
  return resultNode;
1219
}
1220
1221
std::vector<Node> SmtEngine::getValues(const std::vector<Node>& exprs)
1222
{
1223
  std::vector<Node> result;
1224
  for (const Node& e : exprs)
1225
  {
1226
    result.push_back(getValue(e));
1227
  }
1228
  return result;
1229
}
1230
1231
// TODO(#1108): Simplify the error reporting of this method.
1232
28
Model* SmtEngine::getModel() {
1233
28
  Trace("smt") << "SMT getModel()" << endl;
1234
56
  SmtScope smts(this);
1235
1236
28
  finishInit();
1237
1238
28
  if (Dump.isOn("benchmark"))
1239
  {
1240
    getPrinter().toStreamCmdGetModel(getOutputManager().getDumpOut());
1241
  }
1242
1243
28
  Model* m = getAvailableModel("get model");
1244
1245
  // Since model m is being returned to the user, we must ensure that this
1246
  // model object remains valid with future check-sat calls. Hence, we set
1247
  // the theory engine into "eager model building" mode. TODO #2648: revisit.
1248
25
  TheoryEngine* te = getTheoryEngine();
1249
25
  Assert(te != nullptr);
1250
25
  te->setEagerModelBuilding();
1251
1252
25
  if (options::modelCoresMode() != options::ModelCoresMode::NONE)
1253
  {
1254
    // If we enabled model cores, we compute a model core for m based on our
1255
    // (expanded) assertions using the model core builder utility
1256
    std::vector<Node> eassertsProc = getExpandedAssertions();
1257
    ModelCoreBuilder::setModelCore(
1258
        eassertsProc, m->getTheoryModel(), options::modelCoresMode());
1259
  }
1260
  // set the information on the SMT-level model
1261
25
  Assert(m != nullptr);
1262
25
  m->d_inputName = d_state->getFilename();
1263
25
  m->d_isKnownSat = (d_state->getMode() == SmtMode::SAT);
1264
50
  return m;
1265
}
1266
1267
14
Result SmtEngine::blockModel()
1268
{
1269
14
  Trace("smt") << "SMT blockModel()" << endl;
1270
28
  SmtScope smts(this);
1271
1272
14
  finishInit();
1273
1274
14
  if (Dump.isOn("benchmark"))
1275
  {
1276
    getPrinter().toStreamCmdBlockModel(getOutputManager().getDumpOut());
1277
  }
1278
1279
14
  Model* m = getAvailableModel("block model");
1280
1281
14
  if (options::blockModelsMode() == options::BlockModelsMode::NONE)
1282
  {
1283
4
    std::stringstream ss;
1284
2
    ss << "Cannot block model when block-models is set to none.";
1285
2
    throw RecoverableModalException(ss.str().c_str());
1286
  }
1287
1288
  // get expanded assertions
1289
24
  std::vector<Node> eassertsProc = getExpandedAssertions();
1290
  Node eblocker = ModelBlocker::getModelBlocker(
1291
24
      eassertsProc, m->getTheoryModel(), options::blockModelsMode());
1292
24
  return assertFormula(eblocker);
1293
}
1294
1295
10
Result SmtEngine::blockModelValues(const std::vector<Node>& exprs)
1296
{
1297
10
  Trace("smt") << "SMT blockModelValues()" << endl;
1298
20
  SmtScope smts(this);
1299
1300
10
  finishInit();
1301
1302
10
  if (Dump.isOn("benchmark"))
1303
  {
1304
    getPrinter().toStreamCmdBlockModelValues(getOutputManager().getDumpOut(),
1305
                                             exprs);
1306
  }
1307
1308
10
  Model* m = getAvailableModel("block model values");
1309
1310
  // get expanded assertions
1311
18
  std::vector<Node> eassertsProc = getExpandedAssertions();
1312
  // we always do block model values mode here
1313
  Node eblocker =
1314
      ModelBlocker::getModelBlocker(eassertsProc,
1315
                                    m->getTheoryModel(),
1316
                                    options::BlockModelsMode::VALUES,
1317
16
                                    exprs);
1318
16
  return assertFormula(eblocker);
1319
}
1320
1321
10
std::pair<Node, Node> SmtEngine::getSepHeapAndNilExpr(void)
1322
{
1323
10
  if (!getLogicInfo().isTheoryEnabled(THEORY_SEP))
1324
  {
1325
    const char* msg =
1326
        "Cannot obtain separation logic expressions if not using the "
1327
        "separation logic theory.";
1328
    throw RecoverableModalException(msg);
1329
  }
1330
20
  NodeManagerScope nms(getNodeManager());
1331
20
  Node heap;
1332
20
  Node nil;
1333
10
  Model* m = getAvailableModel("get separation logic heap and nil");
1334
10
  TheoryModel* tm = m->getTheoryModel();
1335
10
  if (!tm->getHeapModel(heap, nil))
1336
  {
1337
4
    const char* msg =
1338
        "Failed to obtain heap/nil "
1339
        "expressions from theory model.";
1340
4
    throw RecoverableModalException(msg);
1341
  }
1342
12
  return std::make_pair(heap, nil);
1343
}
1344
1345
69
std::vector<Node> SmtEngine::getExpandedAssertions()
1346
{
1347
136
  std::vector<Node> easserts = getAssertions();
1348
  // must expand definitions
1349
67
  std::vector<Node> eassertsProc;
1350
134
  std::unordered_map<Node, Node, NodeHashFunction> cache;
1351
350
  for (const Node& e : easserts)
1352
  {
1353
566
    Node eae = d_pp->expandDefinitions(e, cache);
1354
283
    eassertsProc.push_back(eae);
1355
  }
1356
134
  return eassertsProc;
1357
}
1358
1359
121
void SmtEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
1360
{
1361
121
  if (!getLogicInfo().isTheoryEnabled(THEORY_SEP))
1362
  {
1363
    const char* msg =
1364
        "Cannot declare heap if not using the separation logic theory.";
1365
    throw RecoverableModalException(msg);
1366
  }
1367
242
  SmtScope smts(this);
1368
121
  finishInit();
1369
121
  TheoryEngine* te = getTheoryEngine();
1370
123
  te->declareSepHeap(locT, dataT);
1371
119
}
1372
1373
840
bool SmtEngine::getSepHeapTypes(TypeNode& locT, TypeNode& dataT)
1374
{
1375
1680
  SmtScope smts(this);
1376
840
  finishInit();
1377
840
  TheoryEngine* te = getTheoryEngine();
1378
1680
  return te->getSepHeapTypes(locT, dataT);
1379
}
1380
1381
5
Node SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; }
1382
1383
5
Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
1384
1385
1142
void SmtEngine::checkProof()
1386
{
1387
1142
  Assert(options::produceProofs());
1388
  // internal check the proof
1389
1142
  PropEngine* pe = getPropEngine();
1390
1142
  Assert(pe != nullptr);
1391
1142
  if (options::proofEagerChecking())
1392
  {
1393
    pe->checkProof(d_asserts->getAssertionList());
1394
  }
1395
1142
  Assert(pe->getProof() != nullptr);
1396
2284
  std::shared_ptr<ProofNode> pePfn = pe->getProof();
1397
1142
  if (options::checkProofs())
1398
  {
1399
1142
    d_pfManager->checkProof(pePfn, *d_asserts, *d_definedFunctions);
1400
  }
1401
1142
}
1402
1403
9105994
StatisticsRegistry* SmtEngine::getStatisticsRegistry()
1404
{
1405
9105994
  return d_env->getStatisticsRegistry();
1406
}
1407
1408
908
UnsatCore SmtEngine::getUnsatCoreInternal()
1409
{
1410
#if IS_PROOFS_BUILD
1411
908
  if (!options::unsatCores())
1412
  {
1413
    throw ModalException(
1414
        "Cannot get an unsat core when produce-unsat-cores option is off.");
1415
  }
1416
908
  if (d_state->getMode() != SmtMode::UNSAT)
1417
  {
1418
    throw RecoverableModalException(
1419
        "Cannot get an unsat core unless immediately preceded by "
1420
        "UNSAT/ENTAILED response.");
1421
  }
1422
  // use old proof infrastructure
1423
908
  if (!d_pfManager)
1424
  {
1425
908
    d_proofManager->traceUnsatCore();  // just to trigger core creation
1426
908
    return UnsatCore(d_proofManager->extractUnsatCore());
1427
  }
1428
  // generate with new proofs
1429
  PropEngine* pe = getPropEngine();
1430
  Assert(pe != nullptr);
1431
  Assert(pe->getProof() != nullptr);
1432
  std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(
1433
      pe->getProof(), *d_asserts, *d_definedFunctions);
1434
  std::vector<Node> core;
1435
  d_ucManager->getUnsatCore(pfn, *d_asserts, core);
1436
  return UnsatCore(core);
1437
#else  /* IS_PROOFS_BUILD */
1438
  throw ModalException(
1439
      "This build of CVC4 doesn't have proof support (required for unsat "
1440
      "cores).");
1441
#endif /* IS_PROOFS_BUILD */
1442
}
1443
1444
840
void SmtEngine::checkUnsatCore() {
1445
840
  Assert(options::unsatCores())
1446
      << "cannot check unsat core if unsat cores are turned off";
1447
1448
840
  Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl;
1449
1680
  UnsatCore core = getUnsatCore();
1450
1451
  // initialize the core checker
1452
1680
  std::unique_ptr<SmtEngine> coreChecker;
1453
840
  initializeSubsolver(coreChecker);
1454
840
  coreChecker->getOptions().set(options::checkUnsatCores, false);
1455
  // disable all proof options
1456
840
  coreChecker->getOptions().set(options::produceProofs, false);
1457
840
  coreChecker->getOptions().set(options::checkUnsatCoresNew, false);
1458
  // set up separation logic heap if necessary
1459
1680
  TypeNode sepLocType, sepDataType;
1460
840
  if (getSepHeapTypes(sepLocType, sepDataType))
1461
  {
1462
21
    coreChecker->declareSepHeap(sepLocType, sepDataType);
1463
  }
1464
1465
840
  Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions"
1466
           << std::endl;
1467
3337
  for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
1468
4994
    Node assertionAfterExpansion = expandDefinitions(*i);
1469
2497
    Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
1470
             << ", expanded to " << assertionAfterExpansion << "\n";
1471
2497
    coreChecker->assertFormula(assertionAfterExpansion);
1472
  }
1473
1680
  Result r;
1474
  try {
1475
840
    r = coreChecker->checkSat();
1476
  } catch(...) {
1477
    throw;
1478
  }
1479
840
  Notice() << "SmtEngine::checkUnsatCore(): result is " << r << endl;
1480
840
  if(r.asSatisfiabilityResult().isUnknown()) {
1481
1
    Warning()
1482
        << "SmtEngine::checkUnsatCore(): could not check core result unknown."
1483
        << std::endl;
1484
  }
1485
839
  else if (r.asSatisfiabilityResult().isSat())
1486
  {
1487
    InternalError()
1488
        << "SmtEngine::checkUnsatCore(): produced core was satisfiable.";
1489
  }
1490
840
}
1491
1492
1950
void SmtEngine::checkModel(bool hardFailure) {
1493
1950
  context::CDList<Node>* al = d_asserts->getAssertionList();
1494
  // --check-model implies --produce-assertions, which enables the
1495
  // assertion list, so we should be ok.
1496
1950
  Assert(al != nullptr)
1497
      << "don't have an assertion list to check in SmtEngine::checkModel()";
1498
1499
3900
  TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
1500
1501
1950
  Notice() << "SmtEngine::checkModel(): generating model" << endl;
1502
1950
  Model* m = getAvailableModel("check model");
1503
1949
  Assert(m != nullptr);
1504
1505
  // check the model with the check models utility
1506
1949
  Assert(d_checkModels != nullptr);
1507
1949
  d_checkModels->checkModel(m, al, hardFailure);
1508
1948
}
1509
1510
900
UnsatCore SmtEngine::getUnsatCore() {
1511
900
  Trace("smt") << "SMT getUnsatCore()" << std::endl;
1512
1800
  SmtScope smts(this);
1513
900
  finishInit();
1514
900
  if (Dump.isOn("benchmark"))
1515
  {
1516
    getPrinter().toStreamCmdGetUnsatCore(getOutputManager().getDumpOut());
1517
  }
1518
1800
  return getUnsatCoreInternal();
1519
}
1520
1521
4
void SmtEngine::getRelevantInstantiationTermVectors(
1522
    std::map<Node, std::vector<std::vector<Node>>>& insts)
1523
{
1524
4
  Assert(d_state->getMode() == SmtMode::UNSAT);
1525
  // generate with new proofs
1526
4
  PropEngine* pe = getPropEngine();
1527
4
  Assert(pe != nullptr);
1528
4
  Assert(pe->getProof() != nullptr);
1529
  std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(
1530
8
      pe->getProof(), *d_asserts, *d_definedFunctions);
1531
4
  d_ucManager->getRelevantInstantiations(pfn, insts);
1532
4
}
1533
1534
std::string SmtEngine::getProof()
1535
{
1536
  Trace("smt") << "SMT getProof()\n";
1537
  SmtScope smts(this);
1538
  finishInit();
1539
  if (Dump.isOn("benchmark"))
1540
  {
1541
    getPrinter().toStreamCmdGetProof(getOutputManager().getDumpOut());
1542
  }
1543
#if IS_PROOFS_BUILD
1544
  if (!options::produceProofs())
1545
  {
1546
    throw ModalException("Cannot get a proof when proof option is off.");
1547
  }
1548
  if (d_state->getMode() != SmtMode::UNSAT)
1549
  {
1550
    throw RecoverableModalException(
1551
        "Cannot get a proof unless immediately preceded by "
1552
        "UNSAT/ENTAILED response.");
1553
  }
1554
  // the prop engine has the proof of false
1555
  PropEngine* pe = getPropEngine();
1556
  Assert(pe != nullptr);
1557
  Assert(pe->getProof() != nullptr);
1558
  Assert(d_pfManager);
1559
  std::ostringstream ss;
1560
  d_pfManager->printProof(ss, pe->getProof(), *d_asserts, *d_definedFunctions);
1561
  return ss.str();
1562
#else  /* IS_PROOFS_BUILD */
1563
  throw ModalException("This build of CVC4 doesn't have proof support.");
1564
#endif /* IS_PROOFS_BUILD */
1565
}
1566
1567
10
void SmtEngine::printInstantiations( std::ostream& out ) {
1568
20
  SmtScope smts(this);
1569
10
  finishInit();
1570
119
  if (options::instFormatMode() == options::InstFormatMode::SZS)
1571
  {
1572
    out << "% SZS output start Proof for " << d_state->getFilename()
1573
        << std::endl;
1574
  }
1575
10
  QuantifiersEngine* qe = getAvailableQuantifiersEngine("printInstantiations");
1576
1577
  // First, extract and print the skolemizations
1578
10
  bool printed = false;
1579
38
  bool reqNames = !options::printInstFull();
1580
  // only print when in list mode
1581
46
  if (options::printInstMode() == options::PrintInstMode::LIST)
1582
  {
1583
14
    std::map<Node, std::vector<Node>> sks;
1584
7
    qe->getSkolemTermVectors(sks);
1585
14
    for (const std::pair<const Node, std::vector<Node>>& s : sks)
1586
    {
1587
14
      Node name;
1588
7
      if (!qe->getNameForQuant(s.first, name, reqNames))
1589
      {
1590
        // did not have a name and we are only printing formulas with names
1591
        continue;
1592
      }
1593
14
      SkolemList slist(name, s.second);
1594
7
      out << slist;
1595
7
      printed = true;
1596
    }
1597
  }
1598
1599
  // Second, extract and print the instantiations
1600
20
  std::map<Node, std::vector<std::vector<Node>>> insts;
1601
10
  getInstantiationTermVectors(insts);
1602
23
  for (const std::pair<const Node, std::vector<std::vector<Node>>>& i : insts)
1603
  {
1604
13
    if (i.second.empty())
1605
    {
1606
      // no instantiations, skip
1607
      continue;
1608
    }
1609
26
    Node name;
1610
13
    if (!qe->getNameForQuant(i.first, name, reqNames))
1611
    {
1612
      // did not have a name and we are only printing formulas with names
1613
      continue;
1614
    }
1615
    // must have a name
1616
13
    if (options::printInstMode() == options::PrintInstMode::NUM)
1617
    {
1618
12
      out << "(num-instantiations " << name << " " << i.second.size() << ")"
1619
6
          << std::endl;
1620
    }
1621
    else
1622
    {
1623
7
      Assert(options::printInstMode() == options::PrintInstMode::LIST);
1624
14
      InstantiationList ilist(name, i.second);
1625
7
      out << ilist;
1626
    }
1627
13
    printed = true;
1628
  }
1629
  // if we did not print anything, we indicate this
1630
10
  if (!printed)
1631
  {
1632
    out << "No instantiations" << std::endl;
1633
  }
1634
10
  if (options::instFormatMode() == options::InstFormatMode::SZS)
1635
  {
1636
    out << "% SZS output end Proof for " << d_state->getFilename() << std::endl;
1637
  }
1638
10
}
1639
1640
10
void SmtEngine::getInstantiationTermVectors(
1641
    std::map<Node, std::vector<std::vector<Node>>>& insts)
1642
{
1643
20
  SmtScope smts(this);
1644
10
  finishInit();
1645
10
  if (options::produceProofs() && getSmtMode() == SmtMode::UNSAT)
1646
  {
1647
    // minimize instantiations based on proof manager
1648
4
    getRelevantInstantiationTermVectors(insts);
1649
  }
1650
  else
1651
  {
1652
    QuantifiersEngine* qe =
1653
6
        getAvailableQuantifiersEngine("getInstantiationTermVectors");
1654
    // otherwise, just get the list of all instantiations
1655
6
    qe->getInstantiationTermVectors(insts);
1656
  }
1657
10
}
1658
1659
4
void SmtEngine::printSynthSolution( std::ostream& out ) {
1660
8
  SmtScope smts(this);
1661
4
  finishInit();
1662
4
  d_sygusSolver->printSynthSolution(out);
1663
4
}
1664
1665
84
bool SmtEngine::getSynthSolutions(std::map<Node, Node>& solMap)
1666
{
1667
168
  SmtScope smts(this);
1668
84
  finishInit();
1669
168
  return d_sygusSolver->getSynthSolutions(solMap);
1670
}
1671
1672
30
Node SmtEngine::getQuantifierElimination(Node q, bool doFull, bool strict)
1673
{
1674
60
  SmtScope smts(this);
1675
30
  finishInit();
1676
30
  const LogicInfo& logic = getLogicInfo();
1677
30
  if (!logic.isPure(THEORY_ARITH) && strict)
1678
  {
1679
10
    Warning() << "Unexpected logic for quantifier elimination " << logic
1680
4
              << endl;
1681
  }
1682
  return d_quantElimSolver->getQuantifierElimination(
1683
60
      *d_asserts, q, doFull, d_isInternalSubsolver);
1684
}
1685
1686
10
bool SmtEngine::getInterpol(const Node& conj,
1687
                            const TypeNode& grammarType,
1688
                            Node& interpol)
1689
{
1690
20
  SmtScope smts(this);
1691
10
  finishInit();
1692
10
  bool success = d_interpolSolver->getInterpol(conj, grammarType, interpol);
1693
  // notify the state of whether the get-interpol call was successfuly, which
1694
  // impacts the SMT mode.
1695
10
  d_state->notifyGetInterpol(success);
1696
20
  return success;
1697
}
1698
1699
9
bool SmtEngine::getInterpol(const Node& conj, Node& interpol)
1700
{
1701
18
  TypeNode grammarType;
1702
18
  return getInterpol(conj, grammarType, interpol);
1703
}
1704
1705
22
bool SmtEngine::getAbduct(const Node& conj,
1706
                          const TypeNode& grammarType,
1707
                          Node& abd)
1708
{
1709
44
  SmtScope smts(this);
1710
22
  finishInit();
1711
22
  bool success = d_abductSolver->getAbduct(conj, grammarType, abd);
1712
  // notify the state of whether the get-abduct call was successfuly, which
1713
  // impacts the SMT mode.
1714
18
  d_state->notifyGetAbduct(success);
1715
36
  return success;
1716
}
1717
1718
14
bool SmtEngine::getAbduct(const Node& conj, Node& abd)
1719
{
1720
28
  TypeNode grammarType;
1721
26
  return getAbduct(conj, grammarType, abd);
1722
}
1723
1724
67
void SmtEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
1725
{
1726
134
  SmtScope smts(this);
1727
  QuantifiersEngine* qe =
1728
67
      getAvailableQuantifiersEngine("getInstantiatedQuantifiedFormulas");
1729
67
  qe->getInstantiatedQuantifiedFormulas(qs);
1730
67
}
1731
1732
63
void SmtEngine::getInstantiationTermVectors(
1733
    Node q, std::vector<std::vector<Node>>& tvecs)
1734
{
1735
126
  SmtScope smts(this);
1736
  QuantifiersEngine* qe =
1737
63
      getAvailableQuantifiersEngine("getInstantiationTermVectors");
1738
63
  qe->getInstantiationTermVectors(q, tvecs);
1739
63
}
1740
1741
69
std::vector<Node> SmtEngine::getAssertions()
1742
{
1743
138
  SmtScope smts(this);
1744
69
  finishInit();
1745
69
  d_state->doPendingPops();
1746
69
  if (Dump.isOn("benchmark"))
1747
  {
1748
    getPrinter().toStreamCmdGetAssertions(getOutputManager().getDumpOut());
1749
  }
1750
69
  Trace("smt") << "SMT getAssertions()" << endl;
1751
69
  if(!options::produceAssertions()) {
1752
2
    const char* msg =
1753
      "Cannot query the current assertion list when not in produce-assertions mode.";
1754
2
    throw ModalException(msg);
1755
  }
1756
67
  context::CDList<Node>* al = d_asserts->getAssertionList();
1757
67
  Assert(al != nullptr);
1758
67
  std::vector<Node> res;
1759
350
  for (const Node& n : *al)
1760
  {
1761
283
    res.emplace_back(n);
1762
  }
1763
  // copy the result out
1764
134
  return res;
1765
}
1766
1767
2556
void SmtEngine::push()
1768
{
1769
5112
  SmtScope smts(this);
1770
2556
  finishInit();
1771
2556
  d_state->doPendingPops();
1772
2556
  Trace("smt") << "SMT push()" << endl;
1773
2556
  d_smtSolver->processAssertions(*d_asserts);
1774
2556
  if(Dump.isOn("benchmark")) {
1775
    getPrinter().toStreamCmdPush(getOutputManager().getDumpOut());
1776
  }
1777
2556
  d_state->userPush();
1778
2556
}
1779
1780
2134
void SmtEngine::pop() {
1781
4268
  SmtScope smts(this);
1782
2134
  finishInit();
1783
2134
  Trace("smt") << "SMT pop()" << endl;
1784
2134
  if (Dump.isOn("benchmark"))
1785
  {
1786
    getPrinter().toStreamCmdPop(getOutputManager().getDumpOut());
1787
  }
1788
2134
  d_state->userPop();
1789
1790
  // Clear out assertion queues etc., in case anything is still in there
1791
2134
  d_asserts->clearCurrent();
1792
  // clear the learned literals from the preprocessor
1793
2134
  d_pp->clearLearnedLiterals();
1794
1795
4268
  Trace("userpushpop") << "SmtEngine: popped to level "
1796
2134
                       << getUserContext()->getLevel() << endl;
1797
  // should we reset d_status here?
1798
  // SMT-LIBv2 spec seems to imply no, but it would make sense to..
1799
2134
}
1800
1801
47
void SmtEngine::reset()
1802
{
1803
  // save pointer to the current node manager
1804
47
  NodeManager* nm = getNodeManager();
1805
47
  Trace("smt") << "SMT reset()" << endl;
1806
47
  if (Dump.isOn("benchmark"))
1807
  {
1808
    getPrinter().toStreamCmdReset(getOutputManager().getDumpOut());
1809
  }
1810
94
  std::string filename = d_state->getFilename();
1811
94
  Options opts;
1812
47
  opts.copyValues(d_originalOptions);
1813
47
  this->~SmtEngine();
1814
47
  new (this) SmtEngine(nm, &opts);
1815
  // Restore data set after creation
1816
47
  notifyStartParsing(filename);
1817
47
}
1818
1819
36
void SmtEngine::resetAssertions()
1820
{
1821
68
  SmtScope smts(this);
1822
1823
36
  if (!d_state->isFullyInited())
1824
  {
1825
    // We're still in Start Mode, nothing asserted yet, do nothing.
1826
    // (see solver execution modes in the SMT-LIB standard)
1827
4
    Assert(getContext()->getLevel() == 0);
1828
4
    Assert(getUserContext()->getLevel() == 0);
1829
4
    getDumpManager()->resetAssertions();
1830
4
    return;
1831
  }
1832
1833
1834
32
  Trace("smt") << "SMT resetAssertions()" << endl;
1835
32
  if (Dump.isOn("benchmark"))
1836
  {
1837
    getPrinter().toStreamCmdResetAssertions(getOutputManager().getDumpOut());
1838
  }
1839
1840
32
  d_asserts->clearCurrent();
1841
32
  d_state->notifyResetAssertions();
1842
32
  getDumpManager()->resetAssertions();
1843
  // push the state to maintain global context around everything
1844
32
  d_state->setup();
1845
1846
  // reset SmtSolver, which will construct a new prop engine
1847
32
  d_smtSolver->resetAssertions();
1848
}
1849
1850
void SmtEngine::interrupt()
1851
{
1852
  if (!d_state->isFullyInited())
1853
  {
1854
    return;
1855
  }
1856
  d_smtSolver->interrupt();
1857
}
1858
1859
void SmtEngine::setResourceLimit(unsigned long units, bool cumulative)
1860
{
1861
  getResourceManager()->setResourceLimit(units, cumulative);
1862
}
1863
void SmtEngine::setTimeLimit(unsigned long milis)
1864
{
1865
  getResourceManager()->setTimeLimit(milis);
1866
}
1867
1868
unsigned long SmtEngine::getResourceUsage() const
1869
{
1870
  return getResourceManager()->getResourceUsage();
1871
}
1872
1873
unsigned long SmtEngine::getTimeUsage() const
1874
{
1875
  return getResourceManager()->getTimeUsage();
1876
}
1877
1878
unsigned long SmtEngine::getResourceRemaining() const
1879
{
1880
  return getResourceManager()->getResourceRemaining();
1881
}
1882
1883
878508
NodeManager* SmtEngine::getNodeManager() const
1884
{
1885
878508
  return d_env->getNodeManager();
1886
}
1887
1888
Statistics SmtEngine::getStatistics() const
1889
{
1890
  return Statistics(*d_env->getStatisticsRegistry());
1891
}
1892
1893
SExpr SmtEngine::getStatistic(std::string name) const
1894
{
1895
  return d_env->getStatisticsRegistry()->getStatistic(name);
1896
}
1897
1898
void SmtEngine::flushStatistics(std::ostream& out) const
1899
{
1900
  d_env->getStatisticsRegistry()->flushInformation(out);
1901
}
1902
1903
void SmtEngine::safeFlushStatistics(int fd) const
1904
{
1905
  d_env->getStatisticsRegistry()->safeFlushInformation(fd);
1906
}
1907
1908
79
void SmtEngine::setUserAttribute(const std::string& attr,
1909
                                 Node expr,
1910
                                 const std::vector<Node>& expr_values,
1911
                                 const std::string& str_value)
1912
{
1913
158
  SmtScope smts(this);
1914
79
  finishInit();
1915
79
  TheoryEngine* te = getTheoryEngine();
1916
79
  Assert(te != nullptr);
1917
79
  te->setUserAttribute(attr, expr, expr_values, str_value);
1918
79
}
1919
1920
9200
void SmtEngine::setOption(const std::string& key, const std::string& value)
1921
{
1922
18398
  NodeManagerScope nms(getNodeManager());
1923
9200
  Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
1924
1925
9200
  if (Dump.isOn("benchmark"))
1926
  {
1927
4
    getPrinter().toStreamCmdSetOption(
1928
2
        getOutputManager().getDumpOut(), key, value);
1929
  }
1930
1931
9200
  if (key == "command-verbosity")
1932
  {
1933
2
    size_t fstIndex = value.find(" ");
1934
2
    size_t sndIndex = value.find(" ", fstIndex + 1);
1935
2
    if (sndIndex == std::string::npos)
1936
    {
1937
4
      string c = value.substr(1, fstIndex - 1);
1938
      int v =
1939
2
          std::stoi(value.substr(fstIndex + 1, value.length() - fstIndex - 1));
1940
2
      if (v < 0 || v > 2)
1941
      {
1942
        throw OptionException("command-verbosity must be 0, 1, or 2");
1943
      }
1944
2
      d_commandVerbosity[c] = v;
1945
2
      return;
1946
    }
1947
    throw OptionException(
1948
        "command-verbosity value must be a tuple (command-name integer)");
1949
  }
1950
1951
9198
  if (value.find(" ") != std::string::npos)
1952
  {
1953
    throw OptionException("bad value for :" + key);
1954
  }
1955
1956
18396
  std::string optionarg = value;
1957
9198
  getOptions().setOption(key, optionarg);
1958
}
1959
1960
2566
void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; }
1961
1962
11323
bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver; }
1963
1964
561154
Node SmtEngine::getOption(const std::string& key) const
1965
{
1966
1122308
  NodeManagerScope nms(getNodeManager());
1967
561154
  NodeManager* nm = d_env->getNodeManager();
1968
1969
561154
  Trace("smt") << "SMT getOption(" << key << ")" << endl;
1970
1971
561154
  if (key.length() >= 18 && key.compare(0, 18, "command-verbosity:") == 0)
1972
  {
1973
    map<string, Integer>::const_iterator i =
1974
561123
        d_commandVerbosity.find(key.c_str() + 18);
1975
561123
    if (i != d_commandVerbosity.end())
1976
    {
1977
      return nm->mkConst(Rational(i->second));
1978
    }
1979
561123
    i = d_commandVerbosity.find("*");
1980
561123
    if (i != d_commandVerbosity.end())
1981
    {
1982
22
      return nm->mkConst(Rational(i->second));
1983
    }
1984
561101
    return nm->mkConst(Rational(2));
1985
  }
1986
1987
31
  if (Dump.isOn("benchmark"))
1988
  {
1989
    getPrinter().toStreamCmdGetOption(d_outMgr.getDumpOut(), key);
1990
  }
1991
1992
31
  if (key == "command-verbosity")
1993
  {
1994
4
    vector<Node> result;
1995
4
    Node defaultVerbosity;
1996
4
    for (map<string, Integer>::const_iterator i = d_commandVerbosity.begin();
1997
4
         i != d_commandVerbosity.end();
1998
         ++i)
1999
    {
2000
      // treat the command name as a variable name as opposed to a string
2001
      // constant to avoid printing double quotes around the name
2002
4
      Node name = nm->mkBoundVar(i->first, nm->integerType());
2003
4
      Node value = nm->mkConst(Rational(i->second));
2004
2
      if ((*i).first == "*")
2005
      {
2006
        // put the default at the end of the SExpr
2007
1
        defaultVerbosity = nm->mkNode(Kind::SEXPR, name, value);
2008
      }
2009
      else
2010
      {
2011
1
        result.push_back(nm->mkNode(Kind::SEXPR, name, value));
2012
      }
2013
    }
2014
    // ensure the default is always listed
2015
2
    if (defaultVerbosity.isNull())
2016
    {
2017
3
      defaultVerbosity = nm->mkNode(Kind::SEXPR,
2018
2
                                    nm->mkBoundVar("*", nm->integerType()),
2019
2
                                    nm->mkConst(Rational(2)));
2020
    }
2021
2
    result.push_back(defaultVerbosity);
2022
2
    return nm->mkNode(Kind::SEXPR, result);
2023
  }
2024
2025
  // parse atom string
2026
56
  std::string atom = getOptions().getOption(key);
2027
2028
27
  if (atom == "true")
2029
  {
2030
22
    return nm->mkConst<bool>(true);
2031
  }
2032
5
  else if (atom == "false")
2033
  {
2034
2
    return nm->mkConst<bool>(false);
2035
  }
2036
  try
2037
  {
2038
4
    Integer z(atom);
2039
1
    return nm->mkConst(Rational(z));
2040
  }
2041
2
  catch (std::invalid_argument&)
2042
  {
2043
    // Fall through to the next case
2044
  }
2045
4
  return nm->mkConst(String(atom));
2046
}
2047
2048
4255528
Options& SmtEngine::getOptions() { return d_env->d_options; }
2049
2050
29
const Options& SmtEngine::getOptions() const { return d_env->getOptions(); }
2051
2052
6185080
ResourceManager* SmtEngine::getResourceManager() const
2053
{
2054
6185080
  return d_env->getResourceManager();
2055
}
2056
2057
21367
DumpManager* SmtEngine::getDumpManager() { return d_env->getDumpManager(); }
2058
2059
12
const Printer& SmtEngine::getPrinter() const { return d_env->getPrinter(); }
2060
2061
18058
OutputManager& SmtEngine::getOutputManager() { return d_outMgr; }
2062
2063
30574872
theory::Rewriter* SmtEngine::getRewriter() { return d_env->getRewriter(); }
2064
2065
26685
}/* CVC4 namespace */