src/theory/decision_manager.cpp

   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-2020 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 DecisionManager::DecisionManager(context::Context* userContext)
  26     : d_strategyCacheC(userContext)
  27 {
  28 }
  29
  30 void DecisionManager::presolve()
  31 {
  32   Trace("dec-manager") << "DecisionManager: presolve." << std::endl;
  33   // remove the strategies that are not in this user context
  34   std::unordered_set<DecisionStrategy*> active;
  35   for (DecisionStrategyList::const_iterator i = d_strategyCacheC.begin();
  36        i != d_strategyCacheC.end();
  37        ++i)
  38   {
  39     active.insert(*i);
  40   }
  41   active.insert(d_strategyCache.begin(), d_strategyCache.end());
  42   std::map<StrategyId, std::vector<DecisionStrategy*> > tmp = d_reg_strategy;
  43   d_reg_strategy.clear();
  44   for (std::pair<const StrategyId, std::vector<DecisionStrategy*> >& rs : tmp)
  45   {
  46     for (DecisionStrategy* ds : rs.second)
  47     {
  48       if (active.find(ds) != active.end())
  49       {
  50         // if its active, we keep it
  51         d_reg_strategy[rs.first].push_back(ds);
  52       }
  53     }
  54   }
  55 }
  56
  57 void DecisionManager::registerStrategy(StrategyId id,
  58                                        DecisionStrategy* ds,
  59                                        StrategyScope sscope)
  60 {
  61   Trace("dec-manager") << "DecisionManager: Register strategy : "
  62                        << ds->identify() << ", id = " << id << std::endl;
  63   ds->initialize();
  64   d_reg_strategy[id].push_back(ds);
  65   if (sscope == STRAT_SCOPE_USER_CTX_DEPENDENT)
  66   {
  67     // store it in the user-context-dependent list
  68     d_strategyCacheC.push_back(ds);
  69   }
  70   else if (sscope == STRAT_SCOPE_CTX_INDEPENDENT)
  71   {
  72     // it is context independent
  73     d_strategyCache.insert(ds);
  74   }
  75   else
  76   {
  77     // it is local to this call, we don't cache it
  78     Assert(sscope == STRAT_SCOPE_LOCAL_SOLVE);
  79   }
  80 }
  81
  82 Node DecisionManager::getNextDecisionRequest()
  83 {
  84   Trace("dec-manager-debug")
  85       << "DecisionManager: Get next decision..." << std::endl;
  86   for (const std::pair<const StrategyId, std::vector<DecisionStrategy*> >& rs :
  87        d_reg_strategy)
  88   {
  89     for (unsigned i = 0, size = rs.second.size(); i < size; i++)
  90     {
  91       DecisionStrategy* ds = rs.second[i];
  92       Node lit = ds->getNextDecisionRequest();
  93       if (!lit.isNull())
  94       {
  95         Trace("dec-manager")
  96             << "DecisionManager:  -> literal " << lit << " decided by strategy "
  97             << ds->identify() << std::endl;
  98         return lit;
  99       }
 100       Trace("dec-manager-debug") << "DecisionManager:  " << ds->identify()
 101                                  << " has no decisions." << std::endl;
 102     }
 103   }
 104   Trace("dec-manager-debug")
 105       << "DecisionManager:  -> no decisions." << std::endl;
 106   return Node::null();
 107 }
 108
 109 }  // namespace theory
 110 }  // namespace CVC4