src/smt/env.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Gereon Kremer, Aina Niemetz
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   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.
  11  * ****************************************************************************
  12  *
  13  * Smt Environment, main access to global utilities available to
  14  * internal code.
  15  */
  16
  17 #include "smt/env.h"
  18
  19 #include "context/context.h"
  20 #include "expr/node.h"
  21 #include "options/base_options.h"
  22 #include "options/smt_options.h"
  23 #include "printer/printer.h"
  24 #include "proof/conv_proof_generator.h"
  25 #include "smt/dump_manager.h"
  26 #include "smt/smt_engine_stats.h"
  27 #include "theory/evaluator.h"
  28 #include "theory/rewriter.h"
  29 #include "theory/trust_substitutions.h"
  30 #include "util/resource_manager.h"
  31 #include "util/statistics_registry.h"
  32
  33 using namespace cvc5::smt;
  34
  35 namespace cvc5 {
  36
  37 Env::Env(NodeManager* nm, const Options* opts)
  38     : d_context(new context::Context()),
  39       d_userContext(new context::UserContext()),
  40       d_nodeManager(nm),
  41       d_proofNodeManager(nullptr),
  42       d_rewriter(new theory::Rewriter()),
  43       d_evalRew(new theory::Evaluator(d_rewriter.get())),
  44       d_eval(new theory::Evaluator(nullptr)),
  45       d_topLevelSubs(new theory::TrustSubstitutionMap(d_userContext.get())),
  46       d_dumpManager(new DumpManager(d_userContext.get())),
  47       d_logic(),
  48       d_statisticsRegistry(std::make_unique<StatisticsRegistry>(*this)),
  49       d_options(),
  50       d_originalOptions(opts),
  51       d_resourceManager()
  52 {
  53   if (opts != nullptr)
  54   {
  55     d_options.copyValues(*opts);
  56   }
  57   d_statisticsRegistry->registerTimer("global::totalTime").start();
  58   d_resourceManager = std::make_unique<ResourceManager>(*d_statisticsRegistry, d_options);
  59 }
  60
  61 Env::~Env() {}
  62
  63 void Env::setProofNodeManager(ProofNodeManager* pnm)
  64 {
  65   Assert(pnm != nullptr);
  66   Assert(d_proofNodeManager == nullptr);
  67   d_proofNodeManager = pnm;
  68   d_rewriter->setProofNodeManager(pnm);
  69   d_topLevelSubs->setProofNodeManager(pnm);
  70 }
  71
  72 void Env::shutdown()
  73 {
  74   d_rewriter.reset(nullptr);
  75   d_dumpManager.reset(nullptr);
  76   // d_resourceManager must be destroyed before d_statisticsRegistry
  77   d_resourceManager.reset(nullptr);
  78 }
  79
  80 context::UserContext* Env::getUserContext() { return d_userContext.get(); }
  81
  82 context::Context* Env::getContext() { return d_context.get(); }
  83
  84 NodeManager* Env::getNodeManager() const { return d_nodeManager; }
  85
  86 ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; }
  87
  88 bool Env::isSatProofProducing() const
  89 {
  90   return d_proofNodeManager != nullptr
  91          && (!d_options.smt.unsatCores
  92              || (d_options.smt.unsatCoresMode
  93                      != options::UnsatCoresMode::ASSUMPTIONS
  94                  && d_options.smt.unsatCoresMode
  95                         != options::UnsatCoresMode::PP_ONLY));
  96 }
  97
  98 bool Env::isTheoryProofProducing() const
  99 {
 100   return d_proofNodeManager != nullptr
 101          && (!d_options.smt.unsatCores
 102              || d_options.smt.unsatCoresMode
 103                     == options::UnsatCoresMode::FULL_PROOF);
 104 }
 105
 106 theory::Rewriter* Env::getRewriter() { return d_rewriter.get(); }
 107
 108 theory::Evaluator* Env::getEvaluator(bool useRewriter)
 109 {
 110   return useRewriter ? d_evalRew.get() : d_eval.get();
 111 }
 112
 113 theory::TrustSubstitutionMap& Env::getTopLevelSubstitutions()
 114 {
 115   return *d_topLevelSubs.get();
 116 }
 117
 118 DumpManager* Env::getDumpManager() { return d_dumpManager.get(); }
 119
 120 const LogicInfo& Env::getLogicInfo() const { return d_logic; }
 121
 122 StatisticsRegistry& Env::getStatisticsRegistry()
 123 {
 124   return *d_statisticsRegistry;
 125 }
 126
 127 const Options& Env::getOptions() const { return d_options; }
 128
 129 const Options& Env::getOriginalOptions() const { return *d_originalOptions; }
 130
 131 ResourceManager* Env::getResourceManager() const
 132 {
 133   return d_resourceManager.get();
 134 }
 135
 136 const Printer& Env::getPrinter()
 137 {
 138   return *Printer::getPrinter(d_options.base.outputLanguage);
 139 }
 140
 141 std::ostream& Env::getDumpOut() { return *d_options.base.out; }
 142
 143 bool Env::isOutputOn(options::OutputTag tag) const
 144 {
 145   return d_options.base.outputTagHolder[static_cast<size_t>(tag)];
 146 }
 147 bool Env::isOutputOn(const std::string& tag) const
 148 {
 149   return isOutputOn(options::stringToOutputTag(tag));
 150 }
 151 std::ostream& Env::getOutput(options::OutputTag tag) const
 152 {
 153   if (isOutputOn(tag))
 154   {
 155     return *d_options.base.out;
 156   }
 157   return cvc5::null_os;
 158 }
 159 std::ostream& Env::getOutput(const std::string& tag) const
 160 {
 161   return getOutput(options::stringToOutputTag(tag));
 162 }
 163
 164 Node Env::evaluate(TNode n,
 165                    const std::vector<Node>& args,
 166                    const std::vector<Node>& vals,
 167                    bool useRewriter) const
 168 {
 169   std::unordered_map<Node, Node> visited;
 170   return evaluate(n, args, vals, visited, useRewriter);
 171 }
 172
 173 Node Env::evaluate(TNode n,
 174                    const std::vector<Node>& args,
 175                    const std::vector<Node>& vals,
 176                    const std::unordered_map<Node, Node>& visited,
 177                    bool useRewriter) const
 178 {
 179   if (useRewriter)
 180   {
 181     return d_evalRew->eval(n, args, vals, visited);
 182   }
 183   return d_eval->eval(n, args, vals, visited);
 184 }
 185
 186 Node Env::rewriteViaMethod(TNode n, MethodId idr)
 187 {
 188   if (idr == MethodId::RW_REWRITE)
 189   {
 190     return d_rewriter->rewrite(n);
 191   }
 192   if (idr == MethodId::RW_EXT_REWRITE)
 193   {
 194     return d_rewriter->extendedRewrite(n);
 195   }
 196   if (idr == MethodId::RW_REWRITE_EQ_EXT)
 197   {
 198     return d_rewriter->rewriteEqualityExt(n);
 199   }
 200   if (idr == MethodId::RW_EVALUATE)
 201   {
 202     return evaluate(n, {}, {}, false);
 203   }
 204   if (idr == MethodId::RW_IDENTITY)
 205   {
 206     // does nothing
 207     return n;
 208   }
 209   // unknown rewriter
 210   Unhandled() << "Env::rewriteViaMethod: no rewriter for " << idr
 211               << std::endl;
 212   return n;
 213 }
 214
 215 }  // namespace cvc5