summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/lazy_trie.h
diff options
context:
space:
mode:
authorHaniel Barbosa <hanielbbarbosa@gmail.com>2018-05-15 12:20:13 -0500
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-05-15 12:20:13 -0500
commit3ca59fea3c2ddbe170830a0fc499254605e1d3c4 (patch)
treed26fae7931845236a69aa441cc7c28ca033b142e /src/theory/quantifiers/lazy_trie.h
parent5d660404622a1fa35b228dd691849a64d365d677 (diff)
Building and refining solutions with dynamic condition generation in CegisUnif (#1920)
Diffstat (limited to 'src/theory/quantifiers/lazy_trie.h')
-rw-r--r--src/theory/quantifiers/lazy_trie.h3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/quantifiers/lazy_trie.h b/src/theory/quantifiers/lazy_trie.h
index 935b9bec1..3585247c6 100644
--- a/src/theory/quantifiers/lazy_trie.h
+++ b/src/theory/quantifiers/lazy_trie.h
@@ -159,6 +159,9 @@ class LazyTrieMulti
* containing only itself.
*/
Node add(Node f, LazyTrieEvaluator* ev, unsigned ntotal);
+ /** clear the trie */
+ void clear();
+
/** A regular lazy trie */
LazyTrie d_trie;
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback