GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/smt_engine_scope.cpp Lines: 24 24 100.0 %
Date: 2021-03-22 Branches: 18 88 20.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file smt_engine_scope.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andres Noetzli, Morgan Deters, Andrew Reynolds
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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "smt/smt_engine_scope.h"
19
20
#include "base/check.h"
21
#include "base/configuration_private.h"
22
#include "base/output.h"
23
#include "smt/smt_engine.h"
24
25
namespace CVC4 {
26
namespace smt {
27
28
thread_local SmtEngine* s_smtEngine_current = NULL;
29
30
30516698
SmtEngine* currentSmtEngine() {
31
30516698
  Assert(s_smtEngine_current != NULL);
32
30516698
  return s_smtEngine_current;
33
}
34
35
15442917
bool smtEngineInScope() { return s_smtEngine_current != NULL; }
36
37
10230834
ProofManager* currentProofManager() {
38
#if IS_PROOFS_BUILD
39
10230834
  Assert(s_smtEngine_current != NULL);
40
10230834
  return s_smtEngine_current->getProofManager();
41
#else  /* IS_PROOFS_BUILD */
42
  InternalError()
43
      << "proofs/unsat cores are not on, but ProofManager requested";
44
  return NULL;
45
#endif /* IS_PROOFS_BUILD */
46
}
47
48
6118220
ResourceManager* currentResourceManager()
49
{
50
6118220
  return s_smtEngine_current->getResourceManager();
51
}
52
53
146190
SmtScope::SmtScope(const SmtEngine* smt)
54
    : NodeManagerScope(smt->getNodeManager()),
55
      d_oldSmtEngine(s_smtEngine_current),
56
146190
      d_optionsScope(smt ? &const_cast<SmtEngine*>(smt)->getOptions() : nullptr)
57
{
58
146190
  Assert(smt != NULL);
59
146190
  s_smtEngine_current = const_cast<SmtEngine*>(smt);
60
146190
  Debug("current") << "smt scope: " << s_smtEngine_current << std::endl;
61
146190
}
62
63
292338
SmtScope::~SmtScope() {
64
146169
  s_smtEngine_current = d_oldSmtEngine;
65
292338
  Debug("current") << "smt scope: returning to " << s_smtEngine_current
66
146169
                   << std::endl;
67
146169
}
68
69
9027967
StatisticsRegistry* SmtScope::currentStatisticsRegistry() {
70
9027967
  Assert(smtEngineInScope());
71
9027967
  return s_smtEngine_current->getStatisticsRegistry();
72
}
73
74
}/* CVC4::smt namespace */
75
26676
}/* CVC4 namespace */