Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Mathias Preiner
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 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                 :            :  * Implementation of Decision manager, which manages all decision
      14                 :            :  * strategies owned by theory solvers within TheoryEngine.
      15                 :            :  */
      16                 :            : 
      17                 :            : #include "theory/decision_manager.h"
      18                 :            : 
      19                 :            : #include "theory/rewriter.h"
      20                 :            : 
      21                 :            : using namespace cvc5::internal::kind;
      22                 :            : 
      23                 :            : namespace cvc5::internal {
      24                 :            : namespace theory {
      25                 :            : 
      26                 :      50193 : DecisionManager::DecisionManager(context::Context* userContext)
      27                 :      50193 :     : d_strategyCacheC(userContext)
      28                 :            : {
      29                 :      50193 : }
      30                 :            : 
      31                 :      49628 : void DecisionManager::presolve()
      32                 :            : {
      33         [ +  - ]:      49628 :   Trace("dec-manager") << "DecisionManager: presolve." << std::endl;
      34                 :            :   // remove the strategies that are not in this user context
      35                 :      99256 :   std::unordered_set<DecisionStrategy*> active;
      36                 :      54167 :   for (DecisionStrategyList::const_iterator i = d_strategyCacheC.begin();
      37         [ +  + ]:      54167 :        i != d_strategyCacheC.end();
      38                 :       4539 :        ++i)
      39                 :            :   {
      40                 :       4539 :     active.insert(*i);
      41                 :            :   }
      42                 :      49628 :   active.insert(d_strategyCache.begin(), d_strategyCache.end());
      43                 :      99256 :   std::map<StrategyId, std::vector<DecisionStrategy*> > tmp = d_reg_strategy;
      44                 :      49628 :   d_reg_strategy.clear();
      45         [ +  + ]:      61145 :   for (std::pair<const StrategyId, std::vector<DecisionStrategy*> >& rs : tmp)
      46                 :            :   {
      47         [ +  + ]:      23921 :     for (DecisionStrategy* ds : rs.second)
      48                 :            :     {
      49         [ +  + ]:      12404 :       if (active.find(ds) != active.end())
      50                 :            :       {
      51                 :            :         // if its active, we keep it
      52                 :      12214 :         d_reg_strategy[rs.first].push_back(ds);
      53                 :            :       }
      54                 :            :     }
      55                 :            :   }
      56                 :      49628 : }
      57                 :            : 
      58                 :      51984 : void DecisionManager::registerStrategy(StrategyId id,
      59                 :            :                                        DecisionStrategy* ds,
      60                 :            :                                        StrategyScope sscope)
      61                 :            : {
      62         [ +  - ]:     103968 :   Trace("dec-manager") << "DecisionManager: Register strategy : "
      63 [ -  + ][ -  - ]:      51984 :                        << ds->identify() << ", id = " << id << std::endl;
      64                 :      51984 :   ds->initialize();
      65                 :      51984 :   d_reg_strategy[id].push_back(ds);
      66         [ +  + ]:      51984 :   if (sscope == STRAT_SCOPE_USER_CTX_DEPENDENT)
      67                 :            :   {
      68                 :            :     // store it in the user-context-dependent list
      69                 :       9573 :     d_strategyCacheC.push_back(ds);
      70                 :            :   }
      71         [ +  + ]:      42411 :   else if (sscope == STRAT_SCOPE_CTX_INDEPENDENT)
      72                 :            :   {
      73                 :            :     // it is context independent
      74                 :      42000 :     d_strategyCache.insert(ds);
      75                 :            :   }
      76                 :            :   else
      77                 :            :   {
      78                 :            :     // it is local to this call, we don't cache it
      79 [ -  + ][ -  + ]:        411 :     Assert(sscope == STRAT_SCOPE_LOCAL_SOLVE);
                 [ -  - ]
      80                 :            :   }
      81                 :      51984 : }
      82                 :            : 
      83                 :    6924420 : Node DecisionManager::getNextDecisionRequest()
      84                 :            : {
      85         [ +  - ]:   13848800 :   Trace("dec-manager-debug")
      86                 :    6924420 :       << "DecisionManager: Get next decision..." << std::endl;
      87                 :    8846820 :   for (const std::pair<const StrategyId, std::vector<DecisionStrategy*> >& rs :
      88         [ +  + ]:   24618000 :        d_reg_strategy)
      89                 :            :   {
      90         [ +  + ]:   22603300 :     for (unsigned i = 0, size = rs.second.size(); i < size; i++)
      91                 :            :     {
      92                 :   13756500 :       DecisionStrategy* ds = rs.second[i];
      93                 :   13756500 :       Node lit = ds->getNextDecisionRequest();
      94         [ +  + ]:   13756500 :       if (!lit.isNull())
      95                 :            :       {
      96         [ +  - ]:     253374 :         Trace("dec-manager")
      97                 :          0 :             << "DecisionManager:  -> literal " << lit << " decided by strategy "
      98 [ -  + ][ -  - ]:     126687 :             << ds->identify() << std::endl;
      99                 :     126687 :         return lit;
     100                 :            :       }
     101 [ +  - ][ -  + ]:   27259600 :       Trace("dec-manager-debug") << "DecisionManager:  " << ds->identify()
                 [ -  - ]
     102                 :   13629800 :                                  << " has no decisions." << std::endl;
     103                 :            :     }
     104                 :            :   }
     105         [ +  - ]:   13595500 :   Trace("dec-manager-debug")
     106                 :    6797730 :       << "DecisionManager:  -> no decisions." << std::endl;
     107                 :    6797730 :   return Node::null();
     108                 :            : }
     109                 :            : 
     110                 :            : }  // namespace theory
     111                 :            : }  // namespace cvc5::internal