Symbolic implementation of partial strings

The idea is to use SMT solvers to reason about partial strings
as set out in the paper "Concurrent Kleene Algebra of Partial
Strings" [1].

This implementation eagerly evaluates the composition of
partial strings. Since this is space inefficient, we are
also planning to experiment with a lazy approach where
partial strings are shared in memory (if possible).

Benchmarks can be automatically generated with the newly
added Bash script "generate_cka_benchmarks.sh" This script
uses the Seed tool [2] to randomly generate star-free CKA
expressions according to the context-free grammar defined
in the new XML file "test/CKA-benchmark.xml".

Here is an example of a program refinement check that uses
our implementation of partial strings:

  Program U{'u'};
  Program V{'v'};
  Program X{'x'};
  Program Y{'y'};

  Program P{((U | V) , (X | Y))};
  Program Q{((U , X) | (V , Y))};

  assert(P <= Q);
  assert(lfp<','>(P) <= lfp<','>(Q));
  assert(lfp<'|'>(P) <= lfp<'|'>(Q));

The example relies on the "Program" class and the overloaded
binary operators "|" and "," for concurrent and sequential
program composition, respectively. The overloaded binary
operator "+" denotes the nondeterministic choice of two programs.
The least fixed point of a program is represented by the
return value of the template function "lfp" whose template
parameter corresponds to the "bowtie" placeholder in [1].

The three assertions above use the overloaded binary relational
operator "<=" to check the refinement of the given programs.
In this example, all three assertions always hold because our
partial string model of CKA provably satisfies the program
exchange law [1] (including some other desirable properties).

[1] http://arxiv.org/abs/1407.0385
[2] http://www-igm.univ-mlv.fr/~nicaud/seed/