Feferman-Vaught on MSOL formulas.


Implements algorithm described in the following paper:

Bruno Courcelle, Johann A. Makowsky, Udi Rotics: 
 Linear Time Solvable Optimization Problems on Graphs of Bounded Clique-Width.
 Theory Comput. Syst. 33(2): 125-150 (2000)

I.e. it computes the set of MSOL formulas to check on every node of the 
k-expression in order to verify a MSOL formula on the whole graph.


Wrote in C++. Some things can be improved...