src/theory/quantifiers/lazy_trie.cpp

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