GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/decision_manager.cpp Lines: 47 47 100.0 %
Date: 2021-03-23 Branches: 72 136 52.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file decision_manager.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 Implementation of Decision manager, which manages all decision
13
 ** strategies owned by theory solvers within TheoryEngine.
14
 **/
15
16
#include "theory/decision_manager.h"
17
18
#include "theory/rewriter.h"
19
20
using namespace CVC4::kind;
21
22
namespace CVC4 {
23
namespace theory {
24
25
8997
DecisionManager::DecisionManager(context::Context* userContext)
26
8997
    : d_strategyCacheC(userContext)
27
{
28
8997
}
29
30
12422
void DecisionManager::presolve()
31
{
32
12422
  Trace("dec-manager") << "DecisionManager: presolve." << std::endl;
33
  // remove the strategies that are not in this user context
34
24844
  std::unordered_set<DecisionStrategy*> active;
35
14991
  for (DecisionStrategyList::const_iterator i = d_strategyCacheC.begin();
36
14991
       i != d_strategyCacheC.end();
37
       ++i)
38
  {
39
2569
    active.insert(*i);
40
  }
41
12422
  active.insert(d_strategyCache.begin(), d_strategyCache.end());
42
24844
  std::map<StrategyId, std::vector<DecisionStrategy*> > tmp = d_reg_strategy;
43
12422
  d_reg_strategy.clear();
44
18559
  for (std::pair<const StrategyId, std::vector<DecisionStrategy*> >& rs : tmp)
45
  {
46
12817
    for (DecisionStrategy* ds : rs.second)
47
    {
48
6680
      if (active.find(ds) != active.end())
49
      {
50
        // if its active, we keep it
51
6418
        d_reg_strategy[rs.first].push_back(ds);
52
      }
53
    }
54
  }
55
12422
}
56
57
13233
void DecisionManager::registerStrategy(StrategyId id,
58
                                       DecisionStrategy* ds,
59
                                       StrategyScope sscope)
60
{
61
26466
  Trace("dec-manager") << "DecisionManager: Register strategy : "
62
13233
                       << ds->identify() << ", id = " << id << std::endl;
63
13233
  ds->initialize();
64
13233
  d_reg_strategy[id].push_back(ds);
65
13233
  if (sscope == STRAT_SCOPE_USER_CTX_DEPENDENT)
66
  {
67
    // store it in the user-context-dependent list
68
4578
    d_strategyCacheC.push_back(ds);
69
  }
70
8655
  else if (sscope == STRAT_SCOPE_CTX_INDEPENDENT)
71
  {
72
    // it is context independent
73
8594
    d_strategyCache.insert(ds);
74
  }
75
  else
76
  {
77
    // it is local to this call, we don't cache it
78
61
    Assert(sscope == STRAT_SCOPE_LOCAL_SOLVE);
79
  }
80
13233
}
81
82
2565385
Node DecisionManager::getNextDecisionRequest()
83
{
84
5130770
  Trace("dec-manager-debug")
85
2565385
      << "DecisionManager: Get next decision..." << std::endl;
86
4192683
  for (const std::pair<const StrategyId, std::vector<DecisionStrategy*> >& rs :
87
2565385
       d_reg_strategy)
88
  {
89
9103669
    for (unsigned i = 0, size = rs.second.size(); i < size; i++)
90
    {
91
4910986
      DecisionStrategy* ds = rs.second[i];
92
9767549
      Node lit = ds->getNextDecisionRequest();
93
4910982
      if (!lit.isNull())
94
      {
95
108838
        Trace("dec-manager")
96
54419
            << "DecisionManager:  -> literal " << lit << " decided by strategy "
97
54419
            << ds->identify() << std::endl;
98
54419
        return lit;
99
      }
100
9713126
      Trace("dec-manager-debug") << "DecisionManager:  " << ds->identify()
101
4856563
                                 << " has no decisions." << std::endl;
102
    }
103
  }
104
5021924
  Trace("dec-manager-debug")
105
2510962
      << "DecisionManager:  -> no decisions." << std::endl;
106
2510962
  return Node::null();
107
}
108
109
}  // namespace theory
110
26685
}  // namespace CVC4