src/smt/env_obj.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   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  * The base class for everything that nees access to the environment (Env)
  14  * instance, which gives access to global utilities available to internal code.
  15  */
  16
  17 #include "smt/env_obj.h"
  18
  19 #include "options/options.h"
  20 #include "smt/env.h"
  21 #include "theory/rewriter.h"
  22
  23 namespace cvc5 {
  24
  25 EnvObj::EnvObj(Env& env) : d_env(env) {}
  26
  27 Node EnvObj::rewrite(TNode node) const
  28 {
  29   return d_env.getRewriter()->rewrite(node);
  30 }
  31
  32 Node EnvObj::extendedRewrite(TNode node, bool aggr) const
  33 {
  34   return d_env.getRewriter()->extendedRewrite(node, aggr);
  35 }
  36 Node EnvObj::evaluate(TNode n,
  37                       const std::vector<Node>& args,
  38                       const std::vector<Node>& vals,
  39                       bool useRewriter) const
  40 {
  41   return d_env.evaluate(n, args, vals, useRewriter);
  42 }
  43 Node EnvObj::evaluate(TNode n,
  44                       const std::vector<Node>& args,
  45                       const std::vector<Node>& vals,
  46                       const std::unordered_map<Node, Node>& visited,
  47                       bool useRewriter) const
  48 {
  49   return d_env.evaluate(n, args, vals, visited, useRewriter);
  50 }
  51
  52 const Options& EnvObj::options() const { return d_env.getOptions(); }
  53
  54 context::Context* EnvObj::context() const { return d_env.getContext(); }
  55
  56 context::UserContext* EnvObj::userContext() const
  57 {
  58   return d_env.getUserContext();
  59 }
  60
  61 const LogicInfo& EnvObj::logicInfo() const { return d_env.getLogicInfo(); }
  62
  63 ResourceManager* EnvObj::resourceManager() const
  64 {
  65   return d_env.getResourceManager();
  66 }
  67
  68 StatisticsRegistry& EnvObj::statisticsRegistry() const
  69 {
  70   return d_env.getStatisticsRegistry();
  71 }
  72
  73 bool EnvObj::isOutputOn(OutputTag tag) const { return d_env.isOutputOn(tag); }
  74
  75 std::ostream& EnvObj::output(OutputTag tag) const { return d_env.output(tag); }
  76
  77 bool EnvObj::isVerboseOn(int64_t level) const
  78 {
  79   return d_env.isVerboseOn(level);
  80 }
  81
  82 std::ostream& EnvObj::verbose(int64_t level) const
  83 {
  84   return d_env.verbose(level);
  85 }
  86
  87 std::ostream& EnvObj::warning() const { return verbose(0); }
  88
  89 }  // namespace cvc5