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                 :            :  * Stores learned information
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "prop/learned_db.h"
      14                 :            : 
      15                 :            : #include <sstream>
      16                 :            : 
      17                 :            : namespace cvc5::internal {
      18                 :            : namespace prop {
      19                 :            : 
      20                 :        451 : LearnedDb::LearnedDb(context::Context* c)
      21                 :        451 :     : d_preprocessSolvedLits(c),
      22                 :        451 :       d_preprocessLits(c),
      23                 :        451 :       d_inputLits(c),
      24                 :        451 :       d_solvableLits(c),
      25                 :        451 :       d_cpropLits(c),
      26                 :        451 :       d_internalLits(c)
      27                 :            : {
      28                 :        451 : }
      29                 :            : 
      30                 :        449 : LearnedDb::~LearnedDb() {}
      31                 :            : 
      32                 :        791 : void LearnedDb::addLearnedLiteral(const Node& lit, modes::LearnedLitType ltype)
      33                 :            : {
      34                 :        791 :   NodeSet& lset = getLiteralSet(ltype);
      35                 :        791 :   lset.insert(lit);
      36                 :        791 : }
      37                 :            : 
      38                 :        657 : std::vector<Node> LearnedDb::getLearnedLiterals(
      39                 :            :     modes::LearnedLitType ltype) const
      40                 :            : {
      41                 :        657 :   const NodeSet& lset = getLiteralSet(ltype);
      42                 :        657 :   std::vector<Node> ret;
      43         [ +  + ]:       1098 :   for (const Node& n : lset)
      44                 :            :   {
      45                 :        441 :     ret.push_back(n);
      46                 :        441 :   }
      47                 :        657 :   return ret;
      48                 :          0 : }
      49                 :        195 : size_t LearnedDb::getNumLearnedLiterals(modes::LearnedLitType ltype) const
      50                 :            : {
      51                 :        195 :   const NodeSet& lset = getLiteralSet(ltype);
      52                 :        195 :   return lset.size();
      53                 :            : }
      54                 :            : 
      55                 :        791 : context::CDHashSet<Node>& LearnedDb::getLiteralSet(modes::LearnedLitType ltype)
      56                 :            : {
      57 [ +  + ][ +  + ]:        791 :   switch (ltype)
                 [ +  + ]
      58                 :            :   {
      59                 :          6 :     case modes::LearnedLitType::PREPROCESS_SOLVED:
      60                 :          6 :       return d_preprocessSolvedLits;
      61                 :        252 :     case modes::LearnedLitType::PREPROCESS: return d_preprocessLits;
      62                 :        480 :     case modes::LearnedLitType::INPUT: return d_inputLits;
      63                 :          1 :     case modes::LearnedLitType::SOLVABLE: return d_solvableLits;
      64                 :          2 :     case modes::LearnedLitType::CONSTANT_PROP: return d_cpropLits;
      65 [ -  + ][ -  + ]:         50 :     default: Assert(ltype == modes::LearnedLitType::INTERNAL); break;
                 [ -  - ]
      66                 :            :   }
      67                 :         50 :   return d_internalLits;
      68                 :            : }
      69                 :            : 
      70                 :        852 : const context::CDHashSet<Node>& LearnedDb::getLiteralSet(
      71                 :            :     modes::LearnedLitType ltype) const
      72                 :            : {
      73 [ +  + ][ +  + ]:        852 :   switch (ltype)
                 [ +  + ]
      74                 :            :   {
      75                 :          2 :     case modes::LearnedLitType::PREPROCESS_SOLVED:
      76                 :          2 :       return d_preprocessSolvedLits;
      77                 :        214 :     case modes::LearnedLitType::PREPROCESS: return d_preprocessLits;
      78                 :        618 :     case modes::LearnedLitType::INPUT: return d_inputLits;
      79                 :          8 :     case modes::LearnedLitType::SOLVABLE: return d_solvableLits;
      80                 :          8 :     case modes::LearnedLitType::CONSTANT_PROP: return d_cpropLits;
      81 [ -  + ][ -  + ]:          2 :     default: Assert(ltype == modes::LearnedLitType::INTERNAL); break;
                 [ -  - ]
      82                 :            :   }
      83                 :          2 :   return d_internalLits;
      84                 :            : }
      85                 :            : 
      86                 :          0 : std::string LearnedDb::toStringDebug() const
      87                 :            : {
      88                 :          0 :   std::stringstream ss;
      89                 :          0 :   ss << toStringDebugType(modes::LearnedLitType::PREPROCESS_SOLVED);
      90                 :          0 :   ss << toStringDebugType(modes::LearnedLitType::PREPROCESS);
      91                 :          0 :   ss << toStringDebugType(modes::LearnedLitType::INPUT);
      92                 :          0 :   ss << toStringDebugType(modes::LearnedLitType::SOLVABLE);
      93                 :          0 :   ss << toStringDebugType(modes::LearnedLitType::CONSTANT_PROP);
      94                 :          0 :   ss << toStringDebugType(modes::LearnedLitType::INTERNAL);
      95                 :          0 :   return ss.str();
      96                 :          0 : }
      97                 :            : 
      98                 :          0 : std::string LearnedDb::toStringDebugType(modes::LearnedLitType ltype) const
      99                 :            : {
     100                 :          0 :   std::stringstream ss;
     101                 :          0 :   const NodeSet& lset = getLiteralSet(ltype);
     102         [ -  - ]:          0 :   if (!lset.empty())
     103                 :            :   {
     104                 :          0 :     ss << "#Learned literals (" << ltype << ") = " << lset.size() << std::endl;
     105                 :            :   }
     106                 :          0 :   return ss.str();
     107                 :          0 : }
     108                 :            : 
     109                 :            : }  // namespace prop
     110                 :            : }  // namespace cvc5::internal