GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/env.cpp Lines: 35 37 94.6 %
Date: 2021-03-22 Branches: 15 32 46.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file env.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   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 Smt Environment, main access to global utilities available to
13
 ** internal code.
14
 **/
15
16
#include "smt/env.h"
17
18
#include "context/context.h"
19
#include "expr/node.h"
20
#include "expr/term_conversion_proof_generator.h"
21
#include "options/base_options.h"
22
#include "printer/printer.h"
23
#include "smt/dump_manager.h"
24
#include "smt/smt_engine_stats.h"
25
#include "theory/rewriter.h"
26
#include "util/resource_manager.h"
27
28
using namespace CVC4::smt;
29
30
namespace CVC4 {
31
32
9620
Env::Env(NodeManager* nm)
33
9620
    : d_context(new context::Context()),
34
9620
      d_userContext(new context::UserContext()),
35
      d_nodeManager(nm),
36
      d_proofNodeManager(nullptr),
37
9620
      d_rewriter(new theory::Rewriter()),
38
9620
      d_dumpManager(new DumpManager(d_userContext.get())),
39
      d_logic(),
40
      d_statisticsRegistry(std::make_unique<StatisticsRegistry>()),
41
48100
      d_resourceManager(std::make_unique<ResourceManager>(*d_statisticsRegistry, d_options))
42
{
43
9620
}
44
45
9599
Env::~Env() {}
46
47
9620
void Env::setOptions(Options* optr)
48
{
49
9620
  if (optr != nullptr)
50
  {
51
    // if we provided a set of options, copy their values to the options
52
    // owned by this Env.
53
8160
    d_options.copyValues(*optr);
54
  }
55
9620
}
56
57
962
void Env::setProofNodeManager(ProofNodeManager* pnm)
58
{
59
962
  d_proofNodeManager = pnm;
60
962
  d_rewriter->setProofNodeManager(pnm);
61
962
}
62
63
9598
void Env::shutdown()
64
{
65
9598
  d_rewriter.reset(nullptr);
66
9598
  d_dumpManager.reset(nullptr);
67
  // d_resourceManager must be destroyed before d_statisticsRegistry
68
9598
  d_resourceManager.reset(nullptr);
69
9598
}
70
71
226203
context::UserContext* Env::getUserContext() { return d_userContext.get(); }
72
73
45650
context::Context* Env::getContext() { return d_context.get(); }
74
75
1439598
NodeManager* Env::getNodeManager() const { return d_nodeManager; }
76
77
ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; }
78
79
30561469
theory::Rewriter* Env::getRewriter() { return d_rewriter.get(); }
80
81
21361
DumpManager* Env::getDumpManager() { return d_dumpManager.get(); }
82
83
41473
const LogicInfo& Env::getLogicInfo() const { return d_logic; }
84
85
9028001
StatisticsRegistry* Env::getStatisticsRegistry()
86
{
87
9028001
  return d_statisticsRegistry.get();
88
}
89
90
29
const Options& Env::getOptions() const { return d_options; }
91
92
6181031
ResourceManager* Env::getResourceManager() const
93
{
94
6181031
  return d_resourceManager.get();
95
}
96
97
12
const Printer& Env::getPrinter()
98
{
99
12
  return *Printer::getPrinter(d_options[options::outputLanguage]);
100
}
101
102
std::ostream& Env::getDumpOut() { return *d_options.getOut(); }
103
104
26676
}  // namespace CVC4