Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Implementation of Decision manager, which manages all decision
      11                 :            :  * strategies owned by theory solvers within TheoryEngine.
      12                 :            :  */
      13                 :            : 
      14                 :            : #include "theory/decision_manager.h"
      15                 :            : 
      16                 :            : #include "theory/rewriter.h"
      17                 :            : 
      18                 :            : using namespace cvc5::internal::kind;
      19                 :            : 
      20                 :            : namespace cvc5::internal {
      21                 :            : namespace theory {
      22                 :            : 
      23                 :      51327 : DecisionManager::DecisionManager(context::Context* userContext)
      24                 :      51327 :     : d_strategyCacheC(userContext)
      25                 :            : {
      26                 :      51327 : }
      27                 :            : 
      28                 :      50759 : void DecisionManager::presolve()
      29                 :            : {
      30         [ +  - ]:      50759 :   Trace("dec-manager") << "DecisionManager: presolve." << std::endl;
      31                 :            :   // remove the strategies that are not in this user context
      32                 :      50759 :   std::unordered_set<DecisionStrategy*> active;
      33                 :      50759 :   for (DecisionStrategyList::const_iterator i = d_strategyCacheC.begin();
      34         [ +  + ]:      55382 :        i != d_strategyCacheC.end();
      35                 :       4623 :        ++i)
      36                 :            :   {
      37                 :       4623 :     active.insert(*i);
      38                 :            :   }
      39                 :      50759 :   active.insert(d_strategyCache.begin(), d_strategyCache.end());
      40                 :      50759 :   std::map<StrategyId, std::vector<DecisionStrategy*> > tmp = d_reg_strategy;
      41                 :      50759 :   d_reg_strategy.clear();
      42         [ +  + ]:      62345 :   for (std::pair<const StrategyId, std::vector<DecisionStrategy*> >& rs : tmp)
      43                 :            :   {
      44         [ +  + ]:      24087 :     for (DecisionStrategy* ds : rs.second)
      45                 :            :     {
      46         [ +  + ]:      12501 :       if (active.find(ds) != active.end())
      47                 :            :       {
      48                 :            :         // if its active, we keep it
      49                 :      12311 :         d_reg_strategy[rs.first].push_back(ds);
      50                 :            :       }
      51                 :            :     }
      52                 :            :   }
      53                 :      50759 : }
      54                 :            : 
      55                 :      53278 : void DecisionManager::registerStrategy(StrategyId id,
      56                 :            :                                        DecisionStrategy* ds,
      57                 :            :                                        StrategyScope sscope)
      58                 :            : {
      59         [ +  - ]:     106556 :   Trace("dec-manager") << "DecisionManager: Register strategy : "
      60 [ -  + ][ -  - ]:      53278 :                        << ds->identify() << ", id = " << id << std::endl;
      61                 :      53278 :   ds->initialize();
      62                 :      53278 :   d_reg_strategy[id].push_back(ds);
      63         [ +  + ]:      53278 :   if (sscope == STRAT_SCOPE_USER_CTX_DEPENDENT)
      64                 :            :   {
      65                 :            :     // store it in the user-context-dependent list
      66                 :       9749 :     d_strategyCacheC.push_back(ds);
      67                 :            :   }
      68         [ +  + ]:      43529 :   else if (sscope == STRAT_SCOPE_CTX_INDEPENDENT)
      69                 :            :   {
      70                 :            :     // it is context independent
      71                 :      43118 :     d_strategyCache.insert(ds);
      72                 :            :   }
      73                 :            :   else
      74                 :            :   {
      75                 :            :     // it is local to this call, we don't cache it
      76 [ -  + ][ -  + ]:        411 :     Assert(sscope == STRAT_SCOPE_LOCAL_SOLVE);
                 [ -  - ]
      77                 :            :   }
      78                 :      53278 : }
      79                 :            : 
      80                 :    7347445 : Node DecisionManager::getNextDecisionRequest()
      81                 :            : {
      82         [ +  - ]:   14694890 :   Trace("dec-manager-debug")
      83                 :    7347445 :       << "DecisionManager: Get next decision..." << std::endl;
      84                 :    7347445 :   for (const std::pair<const StrategyId, std::vector<DecisionStrategy*> >& rs :
      85         [ +  + ]:   23922109 :        d_reg_strategy)
      86                 :            :   {
      87         [ +  + ]:   23263757 :     for (unsigned i = 0, size = rs.second.size(); i < size; i++)
      88                 :            :     {
      89                 :   14036538 :       DecisionStrategy* ds = rs.second[i];
      90                 :   14036538 :       Node lit = ds->getNextDecisionRequest();
      91         [ +  + ]:   14036534 :       if (!lit.isNull())
      92                 :            :       {
      93         [ +  - ]:     333784 :         Trace("dec-manager")
      94                 :          0 :             << "DecisionManager:  -> literal " << lit << " decided by strategy "
      95 [ -  + ][ -  - ]:     166892 :             << ds->identify() << std::endl;
      96                 :     166892 :         return lit;
      97                 :            :       }
      98 [ +  - ][ -  + ]:   27739284 :       Trace("dec-manager-debug") << "DecisionManager:  " << ds->identify()
                 [ -  - ]
      99                 :   13869642 :                                  << " has no decisions." << std::endl;
     100         [ +  + ]:   14036534 :     }
     101                 :            :   }
     102         [ +  - ]:   14361098 :   Trace("dec-manager-debug")
     103                 :    7180549 :       << "DecisionManager:  -> no decisions." << std::endl;
     104                 :    7180549 :   return Node::null();
     105                 :            : }
     106                 :            : 
     107                 :            : }  // namespace theory
     108                 :            : }  // namespace cvc5::internal