Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Haniel Barbosa, Andrew Reynolds, Gereon Kremer
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
       8                 :            :  * in the top-level source directory and their institutional affiliations.
       9                 :            :  * All rights reserved.  See the file COPYING in the top-level source
      10                 :            :  * directory for licensing information.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * Implementation of lazy trie.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "theory/quantifiers/lazy_trie.h"
      17                 :            : 
      18                 :            : namespace cvc5::internal {
      19                 :            : namespace theory {
      20                 :            : namespace quantifiers {
      21                 :            : 
      22                 :      27651 : Node LazyTrie::add(Node n,
      23                 :            :                    LazyTrieEvaluator* ev,
      24                 :            :                    unsigned index,
      25                 :            :                    unsigned ntotal,
      26                 :            :                    bool forceKeep)
      27                 :            : {
      28                 :      27651 :   LazyTrie* lt = this;
      29         [ +  - ]:      62236 :   while (lt != NULL)
      30                 :            :   {
      31         [ +  + ]:      62236 :     if (index == ntotal)
      32                 :            :     {
      33                 :            :       // lazy child holds the leaf data
      34 [ +  + ][ -  + ]:      26161 :       if (lt->d_lazy_child.isNull() || forceKeep)
                 [ +  + ]
      35                 :            :       {
      36                 :       2566 :         lt->d_lazy_child = n;
      37                 :            :       }
      38                 :      53812 :       return lt->d_lazy_child;
      39                 :            :     }
      40         [ +  + ]:      36075 :     if (lt->d_children.empty())
      41                 :            :     {
      42         [ +  + ]:       8538 :       if (lt->d_lazy_child.isNull())
      43                 :            :       {
      44                 :            :         // no one has been here, we are done
      45                 :       1490 :         lt->d_lazy_child = n;
      46                 :       1490 :         return lt->d_lazy_child;
      47                 :            :       }
      48                 :            :       // evaluate the lazy child
      49                 :       7048 :       Node e_lc = ev->evaluate(lt->d_lazy_child, index);
      50                 :            :       // store at next level
      51                 :       7048 :       lt->d_children[e_lc].d_lazy_child = lt->d_lazy_child;
      52                 :            :       // replace
      53                 :       7048 :       lt->d_lazy_child = Node::null();
      54                 :            :     }
      55                 :            :     // recurse
      56                 :      34585 :     Node e = ev->evaluate(n, index);
      57                 :      34585 :     lt = &lt->d_children[e];
      58                 :      34585 :     index = index + 1;
      59                 :            :   }
      60                 :          0 :   return Node::null();
      61                 :            : }
      62                 :            : 
      63                 :       1786 : void LazyTrieMulti::addClassifier(LazyTrieEvaluator* ev, unsigned ntotal)
      64                 :            : {
      65         [ +  - ]:       3572 :   Trace("lazy-trie-multi") << "LazyTrieM: Adding classifier " << ntotal + 1
      66                 :       1786 :                            << "\n";
      67                 :       3572 :   std::vector<IndTriePair> visit;
      68                 :       1786 :   unsigned index = 0;
      69                 :            :   LazyTrie* trie;
      70                 :       1786 :   visit.push_back(IndTriePair(0, &d_trie));
      71         [ +  + ]:       3588 :   while (!visit.empty())
      72                 :            :   {
      73                 :       1802 :     index = visit.back().first;
      74                 :       1802 :     trie = visit.back().second;
      75                 :       1802 :     visit.pop_back();
      76                 :            :     // not at (previous) last level, traverse children
      77         [ +  + ]:       1802 :     if (index < ntotal)
      78                 :            :     {
      79         [ +  + ]:         24 :       for (std::pair<const Node, LazyTrie>& p_nt : trie->d_children)
      80                 :            :       {
      81                 :         16 :         visit.push_back(IndTriePair(index + 1, &p_nt.second));
      82                 :            :       }
      83                 :          8 :       continue;
      84                 :            :     }
      85 [ -  + ][ -  + ]:       1794 :     Assert(trie->d_children.empty());
                 [ -  - ]
      86                 :            :     // if last level and no element at leaf, ignore
      87         [ -  + ]:       1794 :     if (trie->d_lazy_child.isNull())
      88                 :            :     {
      89                 :          0 :       continue;
      90                 :            :     }
      91                 :            :     // apply new classifier
      92 [ -  + ][ -  + ]:       1794 :     Assert(d_rep_to_class.find(trie->d_lazy_child) != d_rep_to_class.end());
                 [ -  - ]
      93                 :       3588 :     std::vector<Node> prev_sep_class = d_rep_to_class[trie->d_lazy_child];
      94         [ -  + ]:       1794 :     if (TraceIsOn("lazy-trie-multi"))
      95                 :            :     {
      96         [ -  - ]:          0 :       Trace("lazy-trie-multi") << "...last level. Prev sep class: \n";
      97         [ -  - ]:          0 :       for (const Node& n : prev_sep_class)
      98                 :            :       {
      99         [ -  - ]:          0 :         Trace("lazy-trie-multi") << "...... " << n << "\n";
     100                 :            :       }
     101                 :            :     }
     102                 :            :     // make new sepclass of lc a singleton with itself
     103                 :       1794 :     d_rep_to_class.erase(trie->d_lazy_child);
     104                 :            :     // replace
     105                 :       1794 :     trie->d_lazy_child = Node::null();
     106         [ +  + ]:       8336 :     for (const Node& n : prev_sep_class)
     107                 :            :     {
     108                 :       6542 :       Node eval = ev->evaluate(n, index);
     109                 :       6542 :       std::map<Node, LazyTrie>::iterator it = trie->d_children.find(eval);
     110         [ +  + ]:       6542 :       if (it != trie->d_children.end())
     111                 :            :       {
     112                 :            :         // add n to to map of item in next level
     113         [ +  - ]:       6604 :         Trace("lazy-trie-multi") << "...add " << n << " to the class of "
     114                 :       3302 :                                  << it->second.d_lazy_child << "\n";
     115                 :       3302 :         d_rep_to_class[it->second.d_lazy_child].push_back(n);
     116                 :       3302 :         continue;
     117                 :            :       }
     118                 :            :       // store at next level
     119                 :       3240 :       trie->d_children[eval].d_lazy_child = n;
     120                 :            :       // create new map
     121         [ +  - ]:       3240 :       Trace("lazy-trie-multi") << "...create new class for : " << n << "\n";
     122 [ -  + ][ -  + ]:       3240 :       Assert(d_rep_to_class.find(n) == d_rep_to_class.end());
                 [ -  - ]
     123                 :       3240 :       d_rep_to_class[n].clear();
     124                 :       3240 :       d_rep_to_class[n].push_back(n);
     125                 :            :     }
     126                 :            :   }
     127                 :       1786 : }
     128                 :            : 
     129                 :      25108 : Node LazyTrieMulti::add(Node f, LazyTrieEvaluator* ev, unsigned ntotal)
     130                 :            : {
     131         [ +  - ]:      25108 :   Trace("lazy-trie-multi") << "LazyTrieM: Adding " << f << "\n";
     132                 :      25108 :   Node res = d_trie.add(f, ev, 0, ntotal, false);
     133                 :            :   // f was added to the separation class with representative res
     134         [ +  + ]:      25108 :   if (res != f)
     135                 :            :   {
     136         [ +  - ]:      46588 :     Trace("lazy-trie-multi") << "... added " << f << " to the sepclass of "
     137                 :      23294 :                              << res << "\n";
     138 [ -  + ][ -  + ]:      23294 :     Assert(d_rep_to_class.find(res) != d_rep_to_class.end());
                 [ -  - ]
     139 [ -  + ][ -  + ]:      23294 :     Assert(!d_rep_to_class[res].empty());
                 [ -  - ]
     140                 :      23294 :     d_rep_to_class[res].push_back(f);
     141                 :      23294 :     return res;
     142                 :            :   }
     143                 :            :   // f is the representatitve of a singleton seperation class
     144         [ +  - ]:       3628 :   Trace("lazy-trie-multi") << "... added " << f
     145                 :       1814 :                            << " as the rep of the sepclass with itself\n";
     146 [ -  + ][ -  + ]:       1814 :   Assert(d_rep_to_class.find(res) == d_rep_to_class.end());
                 [ -  - ]
     147                 :       1814 :   d_rep_to_class[res].clear();
     148                 :       1814 :   d_rep_to_class[res].push_back(f);
     149                 :       1814 :   return res;
     150                 :            : }
     151                 :            : 
     152                 :       1814 : void LazyTrieMulti::clear()
     153                 :            : {
     154                 :       1814 :   d_trie.clear();
     155                 :       1814 :   d_rep_to_class.clear();
     156                 :       1814 : }
     157                 :            : 
     158                 :            : }  // namespace quantifiers
     159                 :            : }  // namespace theory
     160                 :            : }  // namespace cvc5::internal