summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/lazy_trie.h
diff options
context:
space:
mode:
authorHaniel Barbosa <hanielbbarbosa@gmail.com>2018-05-09 16:45:43 -0500
committerGitHub <noreply@github.com>2018-05-09 16:45:43 -0500
commita7393ad4724476d7544483996f65877876698348 (patch)
tree8aec105c230f3279200d3b95c790130876910ad7 /src/theory/quantifiers/lazy_trie.h
parent5adbae1d6aea06f60984c0a7b965f4ee24e5ea6c (diff)
Piecing solutions together in CegisUnif (#1894)
Diffstat (limited to 'src/theory/quantifiers/lazy_trie.h')
-rw-r--r--src/theory/quantifiers/lazy_trie.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/lazy_trie.h b/src/theory/quantifiers/lazy_trie.h
index 2da76d6ef..935b9bec1 100644
--- a/src/theory/quantifiers/lazy_trie.h
+++ b/src/theory/quantifiers/lazy_trie.h
@@ -94,6 +94,8 @@ class LazyTrie
bool forceKeep);
};
+using IndTriePair = std::pair<unsigned, LazyTrie*>;
+
/** Lazy trie with multiple elements per leaf
*
* As the above trie, but allows multiple elements per leaf. This is done by
@@ -157,7 +159,6 @@ class LazyTrieMulti
* containing only itself.
*/
Node add(Node f, LazyTrieEvaluator* ev, unsigned ntotal);
- private:
/** A regular lazy trie */
LazyTrie d_trie;
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback