edit and verify on smt dags

This is a big TODO, probably to be split in smaller pieces.

The plan to port the Fx7 edit&verify implementation to FreeBoogie is the 
following. 
 1. Implement --only-queries. This precludes the use of mechanisms such as 
BG_PUSH. It's not clear how prover assumptions should be handled so we just 
get rid of them as in the case of the ESC/Java & Fx7 experiments.
 2. Normalize the SMT dag.
    2.1. rename variables bound by quantifiers
    2.2. use sets for /\ and \/
    2.3. flatten \/ below \/; same for /\
    2.4. push ¬ below \/ and /\
 3. save and load SMT dag (it's not clear what format is best)
 4. pruning
 5. matching
    5.1. approach
    5.2. bipartite matching (hungarian or maxflow with bfs?)
    5.3. similarity between strings
    5.4. similarity between locations
 6. substitution on SMT dags

The order of operations should be:
 1. Find a correspondence.
 2. Unshare old and new queries together. (e.g. apply unsharing on their 
implication)
 3. Do pruning.

Original issue reported on code.google.com by radugrig...@gmail.com on 16 Mar 2010 at 9:43

rgrig / freeboogie

edit and verify on smt dags #63