String refinement class

Inherits from `bv_refinementt`. It implements a string solver by
creating string constraints via a `string_constraint_generatort`
objects, and sove them by progressively instantiating universal
constraints as needed.

Author: romainbrenguier