Move dstringt documentation to above dstringt

Author: Owen Jones

src/util/README.md

@@ -16,16 +16,11 @@ See \ref irept for more information.
 
 \subsection irep_idt_section Irep_idt and Dstringt
 
-Inside `irept`s, strings are stored as `irep_idt`s, or `irep_namet`s for
-keys to `named_sub` or `comments`. If `USE_STD_STRING` is set then both 
-`irep_idt` and `irep_namet` are `typedef`ed to `std::string`, but by default 
-it is not set and they are `typedef`ed to `dstringt`. `dstringt` has one 
-field, an unsigned integer which is an index into a static table of strings. 
-This makes it expensive to create a new string (because you have to look 
-through the whole table to see if it is already there, and add it if it 
-isn't) but very cheap to compare strings (just compare the two integers). It 
-also means that when you have lots of copies of the same string you only have
-to store the whole string once, which saves space.
+Inside \ref irept, strings are stored as irep_idts, or irep_namets for
+keys to named_sub or comments. By default both irep_idt and irep_namet
+are typedefed to \ref dstringt, unless USE_STD_STRING is set, in which
+case they are typedefed to std::string (this can be used for debugging
+purposes).
 
 \dot
 digraph G {

src/util/dstring.h

@@ -16,8 +16,19 @@ Author: Daniel Kroening, [email protected]
 
 #include "string_container.h"
 
-// Marked final to disable inheritance.
-// No virtual destructor, so runtime-polymorphic use would be unsafe.
+/// `dstringt` has one field, an unsigned integer `no` which is an index into
+/// a static table of strings. This makes it expensive to create a new string
+/// (because you have to look through the whole table to see if it is already
+/// there, and add it if it isn't) but very cheap to compare strings (just
+/// compare the two integers). It also means that when you have lots of copies
+/// of the same string you only have to store the whole string once, which
+/// saves space.
+///
+/// `irep_idt` and `irep_namet` are typedef-ed to `dstringt` in irep.h unless
+///
+///
+/// Note: Marked final to disable inheritance. No virtual destructor, so
+/// runtime-polymorphic use would be unsafe.
 class dstringt final
 {
 public: