Major Section: ACL2 Documentation
This documentation topic relates to an experimental extension of ACL2 that
hons, memoization, and fast alists. See hons-and-memoization.
Thanks to Jared Davis for contributing the ``serialization'' routines for
saving ACL2 objects in files for later loading.
We implement some routines for writing arbitrary ACL2 objects to files, and for loading those files later. We usually call these ".sao" files, which stands for (S)erialized (A)CL2 (O)bject.
Our serialization scheme uses a compact, binary format that preserves structure sharing in the original object. We optimize for read performance.