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...