Tries allow for efficient storage of lists of elements. The prefixes are shared so it is space efficient.
I am looking for a similar way to efficiently store trees. I would like to be able to check for membership and to add elements, knowing if a given tree is a subtree of some stored trees or if there exists a stored tree being a subtree of the given tree is also desirable.
I would typically store about 500 unbalanced binary trees of height less than 50.
My application is some kind of model checker using some sort of memoization. Imagine I have a state $s$ and the following formulae: $f = \phi$ and $g = (\phi \vee \psi)$ with $\phi$ being a complex subformula, and imagine I first want to know if $f$ holds in $s$. I check if $\phi$ holds and after a lengthy process I obtain that it is the case. Now, I want to know if $g$ holds in $s$. I would like to remember the fact that $f$ holds and to notice that $g \Rightarrow f$ so that I can derive $g$ in $s$ almost instantly.
Conversely, if I have proved that $g$ does not hold in $t$, then I want to tell that $f$ does not hold in $t$ almost instantly.
We can build a partial order on formulae, and have $g \geq f$ iff $g \Rightarrow f$. For each state $s$, we store two sets of formulae; $L(s)$ stores the maximal formulae that hold and $l(s)$ stores the minimal formulae that do not hold. Now given a state $s$ and a formula $g$, I can see if $\exists f \in L(s), f \Rightarrow g$, or if $\exists f \in l(s), g \Rightarrow f$ in which case I am done and I know directly whether $g$ holds in $s$.
Currently, $L$ and $l$ are implemented as lists and this is clearly not optimal because I need to iterate through all stored formulae individually. If my formulae were sequences, and if the partial order was "is a prefix of" then a trie could prove much faster. Unfortunately my formulae have a tree like structure based on $\neg, \wedge$, a modal operator, and atomic propositions.
As @Raphael and @Jack points out, I could sequentialise the trees, but I fear it would not solve the problem because the partial order I am interested in would not correspond to "is a prefix of".