Add TaskSolver as abstraction layer over ModelChecker

[ThomasHaas]

This PR adds a new abstraction layer before the ModelChecker. For now, this layer does not do much apart from choosing the appropriate ModelChecker and managing timeouts.
However, the intend is to make this layer more powerful in the future and enable more interesting solving approaches such as:

• Automatic bound unrolling without external script
• Running SMC for some time and if SMC solves the task in, say, < 1000 explored executions, then we are done. Otherwise, fall back to BMC but exploit information gathered from SMC (loop bounds, indirect call targets, aliasing information, summary of sequential prefix, etc.).
• Parallel solving via decomposition?
• "Proof mode" that first unrolls loops until completion and only then checks the properties of interest. This can be a lot more efficient if the program is likely to be correct.
• State-space exploration mode for compilation correctness.

TODO: Update reflection metadata for native build.

EDIT: I also added a TaskResultAnalyzer class that is now responsible for generating the ResultSummary and witness files. Basically, I moved all output generation from Dartagnan.java to TaskResultAnalyzer

EDIT 2: I took the freedom to clean up Dartagnan.java. I think it is a lot easier to follow the logic of Dartagnan now.

[hernanponcedeleon]

Witness generation is not working with the native build

CFLAGS="-DREL2RX" ./dartagnan/target/dartagnan cat/vmm.cat benchmarks/locks/ttas.c --bound.save=output/bound.csv --bound.load=output/bound.csv --witness=png
Fatal error reported via JNI: Could not allocate library name

...  

[hernanponcedeleon]

Witness generation is not working with the native build

CFLAGS="-DREL2RX" ./dartagnan/target/dartagnan cat/vmm.cat benchmarks/locks/ttas.c --bound.save=output/bound.csv --bound.load=output/bound.csv --witness=png
Fatal error reported via JNI: Could not allocate library name

...  

The problem has nothing to do with this PR (there is already a proposed fix in #1023) and the rest LGTM after the latest commit.