Eval literals in formulas and CNF to invert evaluation order.

For some reason, that doesn't work well.

The following table shows number of Setup::Entails() calls and the
milliseconds that took for test_formula.cc's morri_regression test and
the total test time. The first columns refer to debug mode, the last
ones to production mode.

Old w/o min.: 199  2686 ms   6592 ms total  198   77 ms  136 ms total
Old w/  min.: 200  2545 ms   6490 ms total  199   58 ms  120 ms total
New w/o min.: 432  6854 ms  10301 ms total  437  152 ms  215 ms total
New w/  min.: 138  6899 ms  10587 ms total  131  131 ms  193 ms total
Further tried profiling Eval nodes.

The just seem to be no good idea.
Objective level literals in Formulas get special treatment.

The objective level literals should only be SF literals (which occur
there due to regression of K or B literals).
After regression, but before reduction, we check for each literal
outside of any K or B modality whether or not it is entailed and
replace the literal with True or False, respectively. For this to work,
regression skips these literals. When checking their truth, we do
regress the literal alone given that the BAT is in regression mode.

Notice that maintaining a set of SF literals is not sufficient, because
we usually don't add trivially true SF literals for non-sensing actions.

By the way, these trivially true SF literals lead to no additional
entailments because due to regression we end up with a trivially true
formula.

An open problem is how to integrate this with the ESL style, i.e., when
not using regression.