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 trigger trie class.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/quantifiers/ematching/trigger_trie.h"
      14                 :            : 
      15                 :            : namespace cvc5::internal {
      16                 :            : namespace theory {
      17                 :            : namespace quantifiers {
      18                 :            : namespace inst {
      19                 :            : 
      20                 :      83137 : TriggerTrie::TriggerTrie() {}
      21                 :            : 
      22                 :      82805 : TriggerTrie::~TriggerTrie()
      23                 :            : {
      24         [ +  + ]:     120057 :   for (size_t i = 0, ntriggers = d_tr.size(); i < ntriggers; i++)
      25                 :            :   {
      26         [ +  - ]:      37252 :     delete d_tr[i];
      27                 :            :   }
      28                 :      82805 : }
      29                 :            : 
      30                 :      30745 : inst::Trigger* TriggerTrie::getTrigger(const std::vector<Node>& nodes)
      31                 :            : {
      32                 :      30745 :   std::vector<Node> temp;
      33                 :      30745 :   temp.insert(temp.begin(), nodes.begin(), nodes.end());
      34                 :      30745 :   std::sort(temp.begin(), temp.end());
      35                 :      30745 :   TriggerTrie* tt = this;
      36         [ +  + ]:      31152 :   for (const Node& n : temp)
      37                 :            :   {
      38                 :      30958 :     std::map<Node, TriggerTrie>::iterator itt = tt->d_children.find(n);
      39         [ +  + ]:      30958 :     if (itt == tt->d_children.end())
      40                 :            :     {
      41                 :      30551 :       return nullptr;
      42                 :            :     }
      43                 :            :     else
      44                 :            :     {
      45                 :        407 :       tt = &(itt->second);
      46                 :            :     }
      47                 :            :   }
      48         [ -  + ]:        194 :   return tt->d_tr.empty() ? nullptr : tt->d_tr[0];
      49                 :      30745 : }
      50                 :            : 
      51                 :      37252 : void TriggerTrie::addTrigger(const std::vector<Node>& nodes, inst::Trigger* t)
      52                 :            : {
      53                 :      37252 :   std::vector<Node> temp(nodes.begin(), nodes.end());
      54                 :      37252 :   std::sort(temp.begin(), temp.end());
      55                 :      37252 :   TriggerTrie* tt = this;
      56         [ +  + ]:      77868 :   for (const Node& n : temp)
      57                 :            :   {
      58                 :      40616 :     std::map<Node, TriggerTrie>::iterator itt = tt->d_children.find(n);
      59         [ +  + ]:      40616 :     if (itt == tt->d_children.end())
      60                 :            :     {
      61                 :      40583 :       TriggerTrie* ttn = &tt->d_children[n];
      62                 :      40583 :       tt = ttn;
      63                 :            :     }
      64                 :            :     else
      65                 :            :     {
      66                 :         33 :       tt = &(itt->second);
      67                 :            :     }
      68                 :            :   }
      69                 :      37252 :   tt->d_tr.push_back(t);
      70                 :      37252 : }
      71                 :            : 
      72                 :            : }  // namespace inst
      73                 :            : }  // namespace quantifiers
      74                 :            : }  // namespace theory
      75                 :            : }  // namespace cvc5::internal