Implemented smaller setups.

The idea is to only split those literals that may be relevant for the
query. That is, the split set is the least set that contains
* the query's PEL and SF literals corresponding to actions in the query;
* if l is in the split set and occurs in a clause (possibly negated)
  in the setup, then the non-SF PEL of this clause are in the split set
  as well.

Notice that the SF literals from the query are now added in the
beginning already, whereas we added them after computing the full PEL
in the old version. I think it the ordering didn't matter for the old
version, but for the new version we add them first so that, intuitively
speaking, the RHS of the corresponding instantiated SF axioms will be
split as well.

Renamed setup_with_splits_and_sf_subsumes() to setup_entails(). Makes
more sense (it's not just subsumption) and is shorter.

Added setup_inconsistent(). Other than setup_entails() it uses the full
PEL. It's much slower. For completeness, one hence needs to evaluate
``setup_inconsistent() || setup_entails(s, c, k),'' but the idea is to
test setup_inconsistent() just once at the beginning and when it's
changed, but not for every query (or one just trusts the setup to be
consistent). This bookkeeping shall be done in query.c.

Notice that belief.c performs calls setup_inconsistent() a lot. The idea
is (and was before) to memorize these results to avoid testing
inconsistency for the first plausibility levels again and again.
Enabled warnings.

Removed an unused variable.

setup_would_be_needless_split() is unused in setup.c right now, but it
will be back in the next optimization.
Implemented needless split detection.

When attempting to prove c with given k, an atom a is split only if
(1) there is no unit clause [a] or [~a] in the setup AND
(2) (a) c contains a or ~a OR
    (b) some clause d from the setup contains a or ~a AND
        (i)  |d| <= k+1, i.e., it might trigger unit propagation OR
        (ii) |d\c| <= k, i.e., it might lead to subsumption.

This detection requires iteration over the whole setup and is therefore
quite expensive. Maybe an index atom -> clauses that contain the atom
would help, but maintaining this index might be expensive again, because
it needs to be updated during unit propagation and minimization.
Merge branch 'master' into split-optimization
Actions are added to the setups one by one now.

* Replaced setup_add_actions(), [bsetup|context]_add_actions() with
  context_add_action(), [bsetup|context]_add_action(), which only adds a
  single sensing result. This is simpler and also simplifies consistency
  checking (coming up).
* Removed situation and sensing results arguments from
  [b|k]context_init(). Usually one starts with the initial situation.
  Otherwise one can use context_add_action() to build the current
  situation, which may be pretty slow, though.
* Removed macros SF(...) and CONTEX_ADD_ACTIONS(...) because they are
  obsolete.
* Removed context_remove_undone_sf() because context_prev() now undoes
  the sensing already. The old context_remove_undone_sf() looked buggy
  and was untested anyway.
Removed query construct EVAL.

Wasn't fully implemented. Could it useful at all?
The idea was to use that for nested beliefs.
Updated documentation.
Implemented consistency checks.

Each setup caches consistency results for different k.
Whether or not the setup is consistent is updated in
setup_add_sensing_result() by checking if the negation of the SF literal
is entailed. That should be much faster than checking if the empty
clause is entailed because the relevant PEL for the SF literal is
sufficient.
Renamed setup_get_unit_clauses() to setup_unit_clauses().
Updated documentation.
Gitignore.
Updated documentation and unit test.
Added setup_guarantee_consistency().
Replaced MALLOC with NEW where possible.

Improves the code because (some variables can be eliminated, some are
const now). Found a few bugs:

* Fixed clause_sf(): literal wasn't added
* Fixed query_subsitute(): in the literal case, the variable l was
  shadowed
Added context_guarantee_consistency(). Unified Prolog interface naming.

* context_guarantee_consistency() wraps setup_guarantee_consistency()
  and the newly added bsetup_guarantee_consistency().
* Added context_guarantee_consistency/2.
* It's called context_store/2 now.
* It's called context_retrieve/2 now.
Updated readme.
Cosmetic changes.
Fixed: split literals were deleted too aggressively from PEL

Suppose we need to split p and q to show c.
Before, the following would happen:
1. p
 2. q
 3. ~q
4. ~p
because during 2./3., q was deleted from PEL.
Now, the following happens:
1. p
 2. q
 3. ~q
4. ~p
 5. q
 6. ~q
7. q
8. ~q
Sadly, this is much more expensive, obviously.
Added map_[lazy_]copy().
SF literals are not split anymore.

Important: the recursion then needs to stop when k <= 0.
Before, it was k < 0.

A better way to introduce splitting of SF literals that don't count
towards the k-limit would be to use clause_sf() when k == 0 is reached.

For some reason, the unit test test_morri_example() takes very long and
fails due to timeout. The unit test test_morri_example_with_context()
still works. This issue only occurs when setup_clause_small_pel() uses
clause_pel() which also adds SF literals. It is independent of
consistency checks.