Fixed: Boehm GC is used by default.
Removed memory deallocations.

For some reasons:
1. They make (this) code harder to read.
2. They are incomplete anyway.
3. There's no measurable performance benefit when using Boehm GC.
Treating SF literals as normal split variables.

Very bad performance for now:
Increment k by the number of SF literals leads to exponential blowup.
On the other hand the code is simpler and may allow for some heuristic
search.
Fixed performance, broke correctness when splitting SFs.

But broke correctness: Suppose k = 1. When we split an SF literal,
we have k = 0 afterwards and thus cannot do any other split.
This other split could occur in another iteration, but then the SF
cannot be split because then k = 0.

Maybe we shouldn't decrement k when we split an SF.
Splitting SF literals like ordinary literals works now.

All splitting is now in a single function, and SF's are split iff k=0.
The crucial "fix" was not to add SF literals (from the sense axioms) to
PEL, as this would allow further splits of these SF literals which are
not split in the semantics from the paper. Splitting these SF literals
would still be sound, of course, but it's a "fix" as it keeps the
implementation equivalent to the paper.
More efficient use of unit propagation.

We don't manage a split set, but remove from the PEL instead and create
copies of the setups. This allows to memorize the unit propagation.
Optimization of PEL.

Literals from unit clauses are not added to PEL as splitting them is
useless.
Additionally we do one unit propagation on the initial setup.
Support for nested queries (untested). Queries are const now.

A new construct allows for direct evaluation of a given callback
function as part of a query. The idea callback should evaluate the
nested query (wrt the original setup in the single-agent case, and wrt
some other setup in the multi-agent case). Not yet tested.

Also simplified the query rewriting and it's memory management, so that
queries const throughout the API.
Simplified PEL optimization and split-SF computation.

We treat SF of actions in the query as normal split literals except that
they are only split when k = 0 (and thus only when needed). That's why
they are added to the PEL.
The computation of these SF's is now different: before this commit, all
SF atoms for action sequences in the clause but not in context_z were
added.
That won't work well with nested queries because then context_z will
also contain actions from the outer query, not just physically executed
actions.
So the new idea is to base the computation on context_sf, because this
only contains SF results from physically executed actions. However, we
don't want to add trivial SF literals to PEL, because splitting them
won't help but increase complexity. So we just check if the setup
already contains a singleton clause with the SF atom or its negation.

This check also is a more elegant way to compute the initial PEL set, so
we could drop the pel_optimize() function and just do the check in
add_pel_of_clause(). That's shorter and should be even more efficient.
Clearing work, documentation.
Removed nedmalloc. Documentation.

Boehm GC works so well that we probably will stick with it.
Fixed: EVAL queries were not negated properly.
Sped up unit propagation. Added setup_copy_with_new_actions().

Now we reset the set of unit clauses after one iteration over the setup
and only proceed with those unit clauses that were created in the
last iteration.
Fixed profiling test.
Unit propagation minimizes the setup.

Clauses subsumed by new resolvents are removed.
While unit propagation itself becomes more expensive, it generally
improves performance because of smaller setups.
New representation of BATs with macros for simple definition.

Big problem: we have no way to extract names and variables from the
check callback function.

There are two alternative ideas to fix this:
1. Replace the check function with ewffs represented as trees.
   We can extract the names and variables from that tree.
2. Modify the macros so that they add variables and standard names to
   clause specific sets, which are then added to the clause's names and
   variables attributes.
ewffs are now represented as terms instead of callbacks.

The term representation allows to extract variables and names from ewffs
so that H+ can be determined correctly.