GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/options_manager.cpp Lines: 51 68 75.0 %
Date: 2021-03-23 Branches: 88 252 34.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file options_manager.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Aina Niemetz
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 Module for managing options of an SmtEngine.
13
 **/
14
15
#include "smt/options_manager.h"
16
17
#include "base/output.h"
18
#include "expr/expr_iomanip.h"
19
#include "options/base_options.h"
20
#include "options/expr_options.h"
21
#include "options/smt_options.h"
22
#include "smt/command.h"
23
#include "smt/dump.h"
24
#include "smt/set_defaults.h"
25
#include "util/resource_manager.h"
26
27
namespace CVC4 {
28
namespace smt {
29
30
9622
OptionsManager::OptionsManager(Options* opts, ResourceManager* rm)
31
9623
    : d_options(opts), d_resourceManager(rm)
32
{
33
  // set options that must take effect immediately
34
87121
  if (opts->wasSetByUser(options::defaultExprDepth))
35
  {
36
    notifySetOption(options::defaultExprDepth.getName());
37
  }
38
44908
  if (opts->wasSetByUser(options::defaultDagThresh))
39
  {
40
    notifySetOption(options::defaultDagThresh.getName());
41
  }
42
28461
  if (opts->wasSetByUser(options::dumpModeString))
43
  {
44
4
    notifySetOption(options::dumpModeString.getName());
45
  }
46
28537
  if (opts->wasSetByUser(options::printSuccess))
47
  {
48
7
    notifySetOption(options::printSuccess.getName());
49
  }
50
9621
  if (opts->wasSetByUser(options::diagnosticChannelName))
51
  {
52
    notifySetOption(options::diagnosticChannelName.getName());
53
  }
54
9621
  if (opts->wasSetByUser(options::regularChannelName))
55
  {
56
    notifySetOption(options::regularChannelName.getName());
57
  }
58
9621
  if (opts->wasSetByUser(options::dumpToFileName))
59
  {
60
    notifySetOption(options::dumpToFileName.getName());
61
  }
62
  // set this as a listener to be notified of options changes from now on
63
9621
  opts->setListener(this);
64
9621
}
65
66
19200
OptionsManager::~OptionsManager() {}
67
68
9206
void OptionsManager::notifySetOption(const std::string& key)
69
{
70
18412
  Trace("smt") << "SmtEnginePrivate::notifySetOption(" << key << ")"
71
9206
               << std::endl;
72
9206
  if (key == options::defaultExprDepth.getName())
73
  {
74
    int depth = (*d_options)[options::defaultExprDepth];
75
    Debug.getStream() << expr::ExprSetDepth(depth);
76
    Trace.getStream() << expr::ExprSetDepth(depth);
77
    Notice.getStream() << expr::ExprSetDepth(depth);
78
    Chat.getStream() << expr::ExprSetDepth(depth);
79
    CVC4Message.getStream() << expr::ExprSetDepth(depth);
80
    Warning.getStream() << expr::ExprSetDepth(depth);
81
    // intentionally exclude Dump stream from this list
82
  }
83
9206
  else if (key == options::defaultDagThresh.getName())
84
  {
85
1
    int dag = (*d_options)[options::defaultDagThresh];
86
1
    Debug.getStream() << expr::ExprDag(dag);
87
1
    Trace.getStream() << expr::ExprDag(dag);
88
1
    Notice.getStream() << expr::ExprDag(dag);
89
1
    Chat.getStream() << expr::ExprDag(dag);
90
1
    CVC4Message.getStream() << expr::ExprDag(dag);
91
1
    Warning.getStream() << expr::ExprDag(dag);
92
1
    Dump.getStream() << expr::ExprDag(dag);
93
  }
94
9205
  else if (key == options::dumpModeString.getName())
95
  {
96
3
    const std::string& value = (*d_options)[options::dumpModeString];
97
3
    Dump.setDumpFromString(value);
98
  }
99
9202
  else if (key == options::printSuccess.getName())
100
  {
101
32
    bool value = (*d_options)[options::printSuccess];
102
32
    Debug.getStream() << Command::printsuccess(value);
103
32
    Trace.getStream() << Command::printsuccess(value);
104
32
    Notice.getStream() << Command::printsuccess(value);
105
32
    Chat.getStream() << Command::printsuccess(value);
106
32
    CVC4Message.getStream() << Command::printsuccess(value);
107
32
    Warning.getStream() << Command::printsuccess(value);
108
301113
    *options::out() << Command::printsuccess(value);
109
  }
110
9170
  else if (key == options::regularChannelName.getName())
111
  {
112
    d_managedRegularChannel.set(options::regularChannelName());
113
  }
114
9170
  else if (key == options::diagnosticChannelName.getName())
115
  {
116
    d_managedDiagnosticChannel.set(options::diagnosticChannelName());
117
  }
118
9170
  else if (key == options::dumpToFileName.getName())
119
  {
120
    d_managedDumpChannel.set(options::dumpToFileName());
121
  }
122
  // otherwise, no action is necessary
123
9205
}
124
125
8997
void OptionsManager::finishInit(LogicInfo& logic, bool isInternalSubsolver)
126
{
127
  // set up the timeouts and resource limits
128
17994
  if ((*d_options)[options::perCallResourceLimit] != 0)
129
  {
130
    d_resourceManager->setResourceLimit(options::perCallResourceLimit(), false);
131
  }
132
17994
  if ((*d_options)[options::cumulativeResourceLimit] != 0)
133
  {
134
    d_resourceManager->setResourceLimit(options::cumulativeResourceLimit(),
135
                                        true);
136
  }
137
18013
  if ((*d_options)[options::perCallMillisecondLimit] != 0)
138
  {
139
7
    d_resourceManager->setTimeLimit(options::perCallMillisecondLimit());
140
  }
141
  // ensure that our heuristics are properly set up
142
8997
  setDefaults(logic, isInternalSubsolver);
143
8997
}
144
145
}  // namespace smt
146
505316
}  // namespace CVC4