GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/decision_manager.cpp Lines: 47 47 100.0 %
Date: 2021-03-22 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
8995
DecisionManager::DecisionManager(context::Context* userContext)
26
8995
    : d_strategyCacheC(userContext)
27
{
28
8995
}
29
30
12420
void DecisionManager::presolve()
31
{
32
12420
  Trace("dec-manager") << "DecisionManager: presolve." << std::endl;
33
  // remove the strategies that are not in this user context
34
24840
  std::unordered_set<DecisionStrategy*> active;
35
14989
  for (DecisionStrategyList::const_iterator i = d_strategyCacheC.begin();
36
14989
       i != d_strategyCacheC.end();
37
       ++i)
38
  {
39
2569
    active.insert(*i);
40
  }
41
12420
  active.insert(d_strategyCache.begin(), d_strategyCache.end());
42
24840
  std::map<StrategyId, std::vector<DecisionStrategy*> > tmp = d_reg_strategy;
43
12420
  d_reg_strategy.clear();
44
18557
  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
12420
}
56
57
13229
void DecisionManager::registerStrategy(StrategyId id,
58
                                       DecisionStrategy* ds,
59
                                       StrategyScope sscope)
60
{
61
26458
  Trace("dec-manager") << "DecisionManager: Register strategy : "
62
13229
                       << ds->identify() << ", id = " << id << std::endl;
63
13229
  ds->initialize();
64
13229
  d_reg_strategy[id].push_back(ds);
65
13229
  if (sscope == STRAT_SCOPE_USER_CTX_DEPENDENT)
66
  {
67
    // store it in the user-context-dependent list
68
4576
    d_strategyCacheC.push_back(ds);
69
  }
70
8653
  else if (sscope == STRAT_SCOPE_CTX_INDEPENDENT)
71
  {
72
    // it is context independent
73
8592
    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
13229
}
81
82
2565306
Node DecisionManager::getNextDecisionRequest()
83
{
84
5130612
  Trace("dec-manager-debug")
85
2565306
      << "DecisionManager: Get next decision..." << std::endl;
86
4192568
  for (const std::pair<const StrategyId, std::vector<DecisionStrategy*> >& rs :
87
2565306
       d_reg_strategy)
88
  {
89
9103425
    for (unsigned i = 0, size = rs.second.size(); i < size; i++)
90
    {
91
4910857
      DecisionStrategy* ds = rs.second[i];
92
9767305
      Node lit = ds->getNextDecisionRequest();
93
4910853
      if (!lit.isNull())
94
      {
95
108810
        Trace("dec-manager")
96
54405
            << "DecisionManager:  -> literal " << lit << " decided by strategy "
97
54405
            << ds->identify() << std::endl;
98
54405
        return lit;
99
      }
100
9712896
      Trace("dec-manager-debug") << "DecisionManager:  " << ds->identify()
101
4856448
                                 << " has no decisions." << std::endl;
102
    }
103
  }
104
5021794
  Trace("dec-manager-debug")
105
2510897
      << "DecisionManager:  -> no decisions." << std::endl;
106
2510897
  return Node::null();
107
}
108
109
}  // namespace theory
110
26676
}  // namespace CVC4