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 lazy trie.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/quantifiers/lazy_trie.h"
      14                 :            : 
      15                 :            : namespace cvc5::internal {
      16                 :            : namespace theory {
      17                 :            : namespace quantifiers {
      18                 :            : 
      19                 :      28882 : Node LazyTrie::add(Node n,
      20                 :            :                    LazyTrieEvaluator* ev,
      21                 :            :                    unsigned index,
      22                 :            :                    unsigned ntotal,
      23                 :            :                    bool forceKeep)
      24                 :            : {
      25                 :      28882 :   LazyTrie* lt = this;
      26         [ +  - ]:      64527 :   while (lt != nullptr)
      27                 :            :   {
      28         [ +  + ]:      64527 :     if (index == ntotal)
      29                 :            :     {
      30                 :            :       // lazy child holds the leaf data
      31 [ +  + ][ -  + ]:      27257 :       if (lt->d_lazy_child.isNull() || forceKeep)
                 [ +  + ]
      32                 :            :       {
      33                 :       2584 :         lt->d_lazy_child = n;
      34                 :            :       }
      35                 :      56139 :       return lt->d_lazy_child;
      36                 :            :     }
      37         [ +  + ]:      37270 :     if (lt->d_children.empty())
      38                 :            :     {
      39         [ +  + ]:      10697 :       if (lt->d_lazy_child.isNull())
      40                 :            :       {
      41                 :            :         // no one has been here, we are done
      42                 :       1625 :         lt->d_lazy_child = n;
      43                 :       1625 :         return lt->d_lazy_child;
      44                 :            :       }
      45                 :            :       // evaluate the lazy child
      46                 :       9072 :       Node e_lc = ev->evaluate(lt->d_lazy_child, index);
      47                 :            :       // store at next level
      48                 :       9072 :       lt->d_children[e_lc].d_lazy_child = lt->d_lazy_child;
      49                 :            :       // replace
      50                 :       9072 :       lt->d_lazy_child = Node::null();
      51                 :       9072 :     }
      52                 :            :     // recurse
      53                 :      35645 :     Node e = ev->evaluate(n, index);
      54                 :      35645 :     lt = &lt->d_children[e];
      55                 :      35645 :     index = index + 1;
      56                 :      35645 :   }
      57                 :          0 :   return Node::null();
      58                 :            : }
      59                 :            : 
      60                 :       1798 : void LazyTrieMulti::addClassifier(LazyTrieEvaluator* ev, unsigned ntotal)
      61                 :            : {
      62         [ +  - ]:       3596 :   Trace("lazy-trie-multi") << "LazyTrieM: Adding classifier " << ntotal + 1
      63                 :       1798 :                            << "\n";
      64                 :       1798 :   std::vector<IndTriePair> visit;
      65                 :       1798 :   unsigned index = 0;
      66                 :            :   LazyTrie* trie;
      67                 :       1798 :   visit.push_back(IndTriePair(0, &d_trie));
      68         [ +  + ]:       3612 :   while (!visit.empty())
      69                 :            :   {
      70                 :       1814 :     index = visit.back().first;
      71                 :       1814 :     trie = visit.back().second;
      72                 :       1814 :     visit.pop_back();
      73                 :            :     // not at (previous) last level, traverse children
      74         [ +  + ]:       1814 :     if (index < ntotal)
      75                 :            :     {
      76         [ +  + ]:         24 :       for (std::pair<const Node, LazyTrie>& p_nt : trie->d_children)
      77                 :            :       {
      78                 :         16 :         visit.push_back(IndTriePair(index + 1, &p_nt.second));
      79                 :            :       }
      80                 :          8 :       continue;
      81                 :          8 :     }
      82 [ -  + ][ -  + ]:       1806 :     Assert(trie->d_children.empty());
                 [ -  - ]
      83                 :            :     // if last level and no element at leaf, ignore
      84         [ -  + ]:       1806 :     if (trie->d_lazy_child.isNull())
      85                 :            :     {
      86                 :          0 :       continue;
      87                 :            :     }
      88                 :            :     // apply new classifier
      89 [ -  + ][ -  + ]:       1806 :     Assert(d_rep_to_class.find(trie->d_lazy_child) != d_rep_to_class.end());
                 [ -  - ]
      90                 :       1806 :     std::vector<Node> prev_sep_class = d_rep_to_class[trie->d_lazy_child];
      91         [ -  + ]:       1806 :     if (TraceIsOn("lazy-trie-multi"))
      92                 :            :     {
      93         [ -  - ]:          0 :       Trace("lazy-trie-multi") << "...last level. Prev sep class: \n";
      94         [ -  - ]:          0 :       for (const Node& n : prev_sep_class)
      95                 :            :       {
      96         [ -  - ]:          0 :         Trace("lazy-trie-multi") << "...... " << n << "\n";
      97                 :            :       }
      98                 :            :     }
      99                 :            :     // make new sepclass of lc a singleton with itself
     100                 :       1806 :     d_rep_to_class.erase(trie->d_lazy_child);
     101                 :            :     // replace
     102                 :       1806 :     trie->d_lazy_child = Node::null();
     103         [ +  + ]:       8380 :     for (const Node& n : prev_sep_class)
     104                 :            :     {
     105                 :       6574 :       Node eval = ev->evaluate(n, index);
     106                 :       6574 :       std::map<Node, LazyTrie>::iterator it = trie->d_children.find(eval);
     107         [ +  + ]:       6574 :       if (it != trie->d_children.end())
     108                 :            :       {
     109                 :            :         // add n to to map of item in next level
     110         [ +  - ]:       6620 :         Trace("lazy-trie-multi") << "...add " << n << " to the class of "
     111                 :       3310 :                                  << it->second.d_lazy_child << "\n";
     112                 :       3310 :         d_rep_to_class[it->second.d_lazy_child].push_back(n);
     113                 :       3310 :         continue;
     114                 :            :       }
     115                 :            :       // store at next level
     116                 :       3264 :       trie->d_children[eval].d_lazy_child = n;
     117                 :            :       // create new map
     118         [ +  - ]:       3264 :       Trace("lazy-trie-multi") << "...create new class for : " << n << "\n";
     119 [ -  + ][ -  + ]:       3264 :       Assert(d_rep_to_class.find(n) == d_rep_to_class.end());
                 [ -  - ]
     120                 :       3264 :       d_rep_to_class[n].clear();
     121                 :       3264 :       d_rep_to_class[n].push_back(n);
     122         [ +  + ]:       6574 :     }
     123                 :       1806 :   }
     124                 :       1798 : }
     125                 :            : 
     126                 :      26192 : Node LazyTrieMulti::add(Node f, LazyTrieEvaluator* ev, unsigned ntotal)
     127                 :            : {
     128         [ +  - ]:      26192 :   Trace("lazy-trie-multi") << "LazyTrieM: Adding " << f << "\n";
     129                 :      26192 :   Node res = d_trie.add(f, ev, 0, ntotal, false);
     130                 :            :   // f was added to the separation class with representative res
     131         [ +  + ]:      26192 :   if (res != f)
     132                 :            :   {
     133         [ +  - ]:      48692 :     Trace("lazy-trie-multi")
     134                 :      24346 :         << "... added " << f << " to the sepclass of " << res << "\n";
     135 [ -  + ][ -  + ]:      24346 :     Assert(d_rep_to_class.find(res) != d_rep_to_class.end());
                 [ -  - ]
     136 [ -  + ][ -  + ]:      24346 :     Assert(!d_rep_to_class[res].empty());
                 [ -  - ]
     137                 :      24346 :     d_rep_to_class[res].push_back(f);
     138                 :      24346 :     return res;
     139                 :            :   }
     140                 :            :   // f is the representatitve of a singleton seperation class
     141         [ +  - ]:       3692 :   Trace("lazy-trie-multi") << "... added " << f
     142                 :       1846 :                            << " as the rep of the sepclass with itself\n";
     143 [ -  + ][ -  + ]:       1846 :   Assert(d_rep_to_class.find(res) == d_rep_to_class.end());
                 [ -  - ]
     144                 :       1846 :   d_rep_to_class[res].clear();
     145                 :       1846 :   d_rep_to_class[res].push_back(f);
     146                 :       1846 :   return res;
     147                 :          0 : }
     148                 :            : 
     149                 :       1846 : void LazyTrieMulti::clear()
     150                 :            : {
     151                 :       1846 :   d_trie.clear();
     152                 :       1846 :   d_rep_to_class.clear();
     153                 :       1846 : }
     154                 :            : 
     155                 :            : }  // namespace quantifiers
     156                 :            : }  // namespace theory
     157                 :            : }  // namespace cvc5::internal