Remark: Patrik mentions that we can combine his invariant synthesis with Fast
Downward by having his code generate a SAS file suitable for Fast Downward's
preprocessor. The command for that is:

pddlcat -dba-semantics -find-bfs -sas -c -downward -rm

Another domain where invariant synthesis appears to be poor is tidybot from IPC
2011. Patrik's planner has the option of finding its own invariants or using
ours. When using ours, his iPDB implementation solves 1 task; with his
invariants, it solves 12. Here's some info from task #2:

- using Fast Downward representation:

174 atoms (4 goals), 0 resources (0 reusable, 0 consumable), 701
actions, 2 invariants
constructing SAS+ instance...
constructing variables... 169 variables
constructing actions... 701 actions
constructing initial & goal state...
cross referencing and computing graphs...
0.040002 seconds, 4 of 169 variables with goal value
searching for spanning set...
169 of 169 variables in spanning set (0.044002 seconds)

- not using Fast Downward representation:

123 atoms (4 goals), 0 resources (0 reusable, 0 consumable), 701
actions, 39 invariants
constructing SAS+ instance...
constructing variables... 65 variables
constructing actions... 701 actions
constructing initial & goal state...
cross referencing and computing graphs...
0.008001 seconds, 4 of 65 variables with goal value
searching for spanning set...
39 of 65 variables in spanning set (0.092006 seconds)

So it seems it's possible to find much tighter representations there than we do.

I'm attaching a pipesworld-notankage domain file with embedded invariants (using
Patrik's invariant syntax) provided by Patrik. He notes that his invariant
verification algorithm indeed verifies these to be invariants. We only find the
last one (about push-updating/pop-updating/normal).

Since this issue leaves room for lots of different improvements, I decided to
branch off for the different steps. I started this with issue204 for the
inference of additional "!=" constraints (see msg1079).

We should also have a closer look at pipesworld-notankage, because we lose lot
of invariants there and this leads to a much worse performance of the
merge-and-shrink heuristics (cf. issue188).

We also find no invariants at all in Scanalyzer, apparently. This is probably
because of too-heavy tests, and we might be able to fix that by inferring
additional "!=" constraints from static preconditions.

For example, the precondition (CYCLE-2 ?s1 ?s2) implies ?s1 != ?s2 because
CYCLE-2 is static and has no initial state instances with s1 == s2.

Actually, we don't have to restrict this to static predicates but could include
fluent predicates as well by considering all facts in the relaxed reachable set.

Another thing that would be nice to evaluate eventually is how our new code
behaves on the original, buggy version of MPrime (with fuel duplication). If I
recall correctly, we used to have problems in the translator with that version.

We lost some invariants (?) when making the invariant synthesis correct in
issue132. Some of them are actually invariants that can just not be found by the
current algorithm, but could be by an improved algorithm.

As a starting point, we should check, what happens in the domains where the new
invariant synthesis has a negative impact. Attached are the experimental results
for this change and here are some notes, what could be critical changes:

Check point 14. in the evaluation,
"translator_effect_conditions_simplified", with old vs. new values:

airport                         0 	307799
openstacks-strips               0 	54320
pipesworld-notankage 	        0 	24556
pipesworld-tankage 	        0 	248576
psr-small                       0 	226
woodworking-opt08-strips 	0 	2860
woodworking-sat08-strips 	0 	10968


Check point 17. in the evaluation,
"implied_effects_removed", with old vs. new values:

pipesworld-notankage       	0 	10320
pipesworld-tankage 	        0 	13060


Check point 21. in the evaluation,
translator_operators_removed, with old vs. new values:

satellite                     	19935 	16860


Check point 24. in the evaluation,
translator_propositions_removed, with old vs. new values:

airport 	                146272 	59544
openstacks-strips 	        1939 	944
pipesworld-notankage 	        1942 	310
pipesworld-tankage 	        4046 	3152
psr-small 	                964 	835
schedule 	                9254 	2608
woodworking-opt08-strips 	1175 	1132
woodworking-sat08-strips 	2434 	2342


Check point 38. in the evaluation,
translator_time_finding_invariants, with old vs. new values:

airport 	                9.63 	61.57
openstacks-strips 	        1395.16 2932.78
trucks-strips 	                634.3 	2198.89

(If there's something that we should change in the code here later, it
would be good to also test the other domains again since many of these
also have increases in time, though less drastic.)


Check point 53. in the evaluation,
translator_uncovered_facts, with old vs. new values:

airport 	                181 	144317
openstacks-strips 	        1881 	3871
pipesworld-notankage 	        0 	22132
pipesworld-tankage 	        0 	2969
psr-small 	                159 	417
storage 	                1530 	3190
woodworking-opt08-strips 	994 	1998
woodworking-sat08-strips 	2149 	5159


Check point 54. in the evaluation,
translator_vars, with old vs. new values:

airport 	                58168 	115573
openstacks-strips 	        3820 	4815
pipesworld-notankage 	        1134 	22242
pipesworld-tankage 	        3210 	6019
psr-small 	                1123 	1252
schedule 	                43771 	70292
storage 	                1380 	2800
woodworking-opt08-strips        1601    2380
woodworking-sat08-strips        3510    6025

=> Also compare to preprocessor_vars. If variables are added but then
removed by the preprocessor, then we don't need to worry about them.