1 /********************* */
2 /*! \file lazy_trie.cpp
4 ** Top contributors (to current version):
5 ** Haniel Barbosa, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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
12 ** \brief Implementation of lazy trie
15 #include "theory/quantifiers/lazy_trie.h"
19 namespace quantifiers
{
21 Node
LazyTrie::add(Node n
,
22 LazyTrieEvaluator
* ev
,
32 // lazy child holds the leaf data
33 if (lt
->d_lazy_child
.isNull() || forceKeep
)
37 return lt
->d_lazy_child
;
39 if (lt
->d_children
.empty())
41 if (lt
->d_lazy_child
.isNull())
43 // no one has been here, we are done
45 return lt
->d_lazy_child
;
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
;
52 lt
->d_lazy_child
= Node::null();
55 Node e
= ev
->evaluate(n
, index
);
56 lt
= <
->d_children
[e
];
62 void LazyTrieMulti::addClassifier(LazyTrieEvaluator
* ev
, unsigned ntotal
)
64 Trace("lazy-trie-multi") << "LazyTrieM: Adding classifier " << ntotal
+ 1
66 std::vector
<IndTriePair
> visit
;
69 visit
.push_back(IndTriePair(0, &d_trie
));
70 while (!visit
.empty())
72 index
= visit
.back().first
;
73 trie
= visit
.back().second
;
75 // not at (previous) last level, traverse children
78 for (std::pair
<const Node
, LazyTrie
>& p_nt
: trie
->d_children
)
80 visit
.push_back(IndTriePair(index
+ 1, &p_nt
.second
));
84 Assert(trie
->d_children
.empty());
85 // if last level and no element at leaf, ignore
86 if (trie
->d_lazy_child
.isNull())
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"))
95 Trace("lazy-trie-multi") << "...last level. Prev sep class: \n";
96 for (const Node
& n
: prev_sep_class
)
98 Trace("lazy-trie-multi") << "...... " << n
<< "\n";
101 // make new sepclass of lc a singleton with itself
102 d_rep_to_class
.erase(trie
->d_lazy_child
);
104 trie
->d_lazy_child
= Node::null();
105 for (const Node
& n
: prev_sep_class
)
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())
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
);
117 // store at next level
118 trie
->d_children
[eval
].d_lazy_child
= n
;
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
);
128 Node
LazyTrieMulti::add(Node f
, LazyTrieEvaluator
* ev
, unsigned ntotal
)
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
135 Trace("lazy-trie-multi") << "... added " << f
<< " to the sepclass of "
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
);
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
);
151 void LazyTrieMulti::clear()
154 d_rep_to_class
.clear();
157 } /* CVC4::theory::quantifiers namespace */
158 } /* CVC4::theory namespace */
159 } /* CVC4 namespace */