Define logging

[krobelus]

The runtime option for logging (-v) should allow for a reasonable amount of introspection of the checker's behavior. At least we should output the status of each lemma (skipped/RUP/RAT/...). Printing the trail is probably too much though.

[krobelus]

Looks like this after b8ffb4a:

$ cargo run --bin rate benchmarks/crafted/example1.{cnf,drat} -v | grep -v '^c'
add premise [0] 1 2 3 0
add premise [1] -1 2 3 0
add premise [2] -2 1 3 0
add premise [3] -2 -1 3 0
add premise [4] -3 1 2 0
add premise [5] -3 -1 2 0
add premise [6] -3 -2 1 0
add premise [7] -3 -2 -1 0
add lemma [8] 1 2 0
add lemma [9] 1 0
add lemma [10] -1 4 0
del (shrinking trail by 1) [10] 4 -1 0
add lemma [11] -4 -1 0
add lemma [12] 1 4 0
add lemma [13] 2 4 0
lemma RUP [13] 2 0
lemma skipped (not in core) [12] 1 4 0
lemma RAT [11] -4 0
lemma skipped (not in core) [10] 4 -1 0
lemma RUP [9] 1 0
lemma RUP [8] 2 1 0
s VERIFIED

$ cargo run --bin rate benchmarks/crafted/example1.{cnf,drat} --skip-unit-deletions -v | grep -v '^c'
add premise [0] 1 2 3 0
add premise [1] -1 2 3 0
add premise [2] -2 1 3 0
add premise [3] -2 -1 3 0
add premise [4] -3 1 2 0
add premise [5] -3 -1 2 0
add premise [6] -3 -2 1 0
add premise [7] -3 -2 -1 0
add lemma [8] 1 2 0
add lemma [9] 1 0
add lemma [10] -1 4 0
del (skipped) [10] -1 4 0
add lemma [11] -4 -1 0
s NOT VERIFIED