GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/smt_engine.cpp Lines: 817 1011 80.8 %
Date: 2021-03-22 Branches: 1248 3395 36.8 %

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