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 a trie that store subsets of tuples of term indices
      11                 :            :  * that are not yielding  useful instantiations. of quantifier instantiation.
      12                 :            :  * This is used in the term_tuple_enumerator.
      13                 :            :  */
      14                 :            : #include "theory/quantifiers/index_trie.h"
      15                 :            : 
      16                 :            : namespace cvc5::internal {
      17                 :            : namespace theory {
      18                 :            : namespace quantifiers {
      19                 :            : 
      20                 :      83221 : void IndexTrie::add(const std::vector<bool>& mask,
      21                 :            :                     const std::vector<Node>& values)
      22                 :            : {
      23                 :      83221 :   const size_t cardinality = std::count(mask.begin(), mask.end(), true);
      24 [ +  - ][ +  + ]:      83221 :   if (d_ignoreFullySpecified && cardinality == mask.size())
                 [ +  + ]
      25                 :            :   {
      26                 :      63788 :     return;
      27                 :            :   }
      28                 :            : 
      29                 :      19433 :   d_root = addRec(d_root, 0, cardinality, mask, values);
      30                 :            : }
      31                 :            : 
      32                 :      95970 : void IndexTrie::freeRec(IndexTrieNode* n)
      33                 :            : {
      34         [ +  + ]:      95970 :   if (!n)
      35                 :            :   {
      36                 :      54752 :     return;
      37                 :            :   }
      38         [ +  + ]:      67069 :   for (auto c : n->d_children)
      39                 :            :   {
      40                 :      25851 :     freeRec(c.second);
      41                 :      25851 :   }
      42                 :      41218 :   freeRec(n->d_blank);
      43         [ +  - ]:      41218 :   delete n;
      44                 :            : }
      45                 :            : 
      46                 :     214713 : bool IndexTrie::findRec(const IndexTrieNode* n,
      47                 :            :                         size_t index,
      48                 :            :                         const std::vector<Node>& members,
      49                 :            :                         size_t& nonBlankLength) const
      50                 :            : {
      51 [ +  + ][ -  + ]:     214713 :   if (!n || index >= members.size())
                 [ +  + ]
      52                 :            :   {
      53                 :       4301 :     return true;  // all elements of members matched
      54                 :            :   }
      55 [ +  + ][ +  + ]:     210412 :   if (n->d_blank && findRec(n->d_blank, index + 1, members, nonBlankLength))
                 [ +  + ]
      56                 :            :   {
      57                 :       2539 :     return true;  // found in the blank branch
      58                 :            :   }
      59         [ +  + ]:     207873 :   if (members[index].isNull())
      60                 :            :   {
      61                 :            :     // null is interpreted as "any", must have found in the blank branch
      62                 :      12131 :     return false;
      63                 :            :   }
      64                 :     195742 :   nonBlankLength = index + 1;
      65         [ +  + ]:    1925374 :   for (const auto& c : n->d_children)
      66                 :            :   {
      67                 :    1738437 :     if (c.first == members[index]
      68 [ +  + ][ +  + ]:    1738437 :         && findRec(c.second, index + 1, members, nonBlankLength))
                 [ +  + ]
      69                 :            :     {
      70                 :       8805 :       return true;  // found in the matching subtree
      71                 :            :     }
      72                 :            :   }
      73                 :     186937 :   return false;
      74                 :            : }
      75                 :            : 
      76                 :      60993 : IndexTrieNode* IndexTrie::addRec(IndexTrieNode* n,
      77                 :            :                                  size_t index,
      78                 :            :                                  size_t cardinality,
      79                 :            :                                  const std::vector<bool>& mask,
      80                 :            :                                  const std::vector<Node>& values)
      81                 :            : {
      82         [ -  + ]:      60993 :   if (!n)
      83                 :            :   {
      84                 :          0 :     return nullptr;  // this tree matches everything, no point to add
      85                 :            :   }
      86         [ +  + ]:      60993 :   if (cardinality == 0)  // all blanks, all strings match
      87                 :            :   {
      88                 :      19433 :     freeRec(n);
      89                 :      19433 :     return nullptr;
      90                 :            :   }
      91                 :            : 
      92 [ -  + ][ -  + ]:      41560 :   Assert(index < mask.size());
                 [ -  - ]
      93                 :            : 
      94         [ +  + ]:      41560 :   if (!mask[index])  // blank position in the added vector
      95                 :            :   {
      96         [ +  + ]:      12513 :     auto blank = n->d_blank ? n->d_blank : new IndexTrieNode();
      97                 :      12513 :     n->d_blank = addRec(blank, index + 1, cardinality, mask, values);
      98                 :      12513 :     return n;
      99                 :            :   }
     100 [ -  + ][ -  + ]:      29047 :   Assert(cardinality);
                 [ -  - ]
     101 [ -  + ][ -  + ]:      29047 :   Assert(!values[index].isNull());
                 [ -  - ]
     102         [ +  + ]:     437665 :   for (auto& edge : n->d_children)
     103                 :            :   {
     104         [ +  + ]:     411814 :     if (edge.first == values[index])
     105                 :            :     {
     106                 :            :       // value already amongst the children
     107                 :       3196 :       edge.second =
     108                 :       3196 :           addRec(edge.second, index + 1, cardinality - 1, mask, values);
     109                 :       3196 :       return n;
     110                 :            :     }
     111                 :            :   }
     112                 :            :   // new child needs to be added
     113                 :            :   auto child =
     114                 :      25851 :       addRec(new IndexTrieNode(), index + 1, cardinality - 1, mask, values);
     115                 :      25851 :   n->d_children.push_back(std::make_pair(values[index], child));
     116                 :      25851 :   return n;
     117                 :            : }
     118                 :            : }  // namespace quantifiers
     119                 :            : }  // namespace theory
     120                 :            : }  // namespace cvc5::internal