Clause Tracing

[joe-hauns]

This PR implements debugging functionality to easily trace consequences of clauses. Added options:

• --trace_fwd <clause-id>: vampire will output all clauses that are derived from the given clause
• --trace_bwd <clause-id>: vampire will output all clauses that have been used to derive the given clause. the output is tree-like structured The clause tracing is implemented directly in the Clause constructor and will be complied-away in Release mode. In order to implement this the clause constructor had to be refactored a little bit which simplified the codebase overall.

Examples:

❯ vampire --input_syntax smtlib2 --trace_fwd 3 i-challange-u/motivating-1.smt2

forward trace 3: 29. $sum(0.0,X0) = X0 [superposition 3,5]
forward trace 3: 30. 0.0 = $sum(X0,$uminus(X0)) [superposition 3,25]
forward trace 3: 31. $sum(0.0,X0) = X0 [superposition 3,5]
forward trace 3: 32. 0.0 = $sum(X0,$uminus(X0)) [superposition 3,25]
forward trace 3: 33. $sum(0.0,X0) = X0 [superposition 5,3]
forward trace 3: 34. 0.0 = $sum(X0,$uminus(X0)) [superposition 25,3]
forward trace 3: 35. $sum(0.0,X0) = X0 [superposition 5,3]
forward trace 3: 36. 0.0 = $sum(X0,$uminus(X0)) [superposition 25,3]
forward trace 3: 46. $less(X1,$sum(1.0,X0)) | $less(X0,X1) [superposition 12,3]
forward trace 3: 47. $less(X1,$sum(1.0,X0)) | $less(X0,X1) [superposition 12,3]
forward trace 3: 56. $less(X0,$sum(1.0,X0)) [superposition 45,3]
forward trace 3: 57. $less(X0,$sum(1.0,X0)) [superposition 45,3]
...

❯ vampire --input_syntax smtlib2 --trace_bwd 7310 /Users/jo/Downloads/i-challange-u/motivating-1.smt2

backward trace 7310: | | | 4. $sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2) [theory axiom 144]
backward trace 7310: | | | 3. $sum(X0,X1) = $sum(X1,X0) [theory axiom 143]
backward trace 7310: | | 114. $sum(X0,$sum(X1,X2)) = $sum($sum(X1,X0),X2) [superposition 4,3]
backward trace 7310: | | 3. $sum(X0,X1) = $sum(X1,X0) [theory axiom 143]
backward trace 7310: | 535. $sum(X2,$sum(X0,X1)) = $sum(X1,$sum(X0,X2)) [superposition 114,3]
backward trace 7310: | 3. $sum(X0,X1) = $sum(X1,X0) [theory axiom 143]
backward trace 7310: 7310. $sum(X2,$sum(X1,X0)) = $sum($sum(X1,X2),X0) [superposition 535,3]

...

[joe-hauns]

(running regression tests right now)

[MichaelRawson]

Shall I hold off on this while the bugs are fixed? Ping me when it's ready.

[quickbeam123]

Could I please also have a look before it goes in?

[MichaelRawson]

Added you so I can't forget.

[quickbeam123]

@joe-hauns, are you also doing some random tptp/smtlib testing?

Also, just out of curiosity, what are some typical use-cases of this new functionality for you?

[joe-hauns]

Okay so I can't find any significant difference to the behaviour in master anymore. So it's good to review :)

[joe-hauns]

@joe-hauns, are you also doing some random tptp/smtlib testing?

Yess i ran random strategies to look for errors. Couldn't find any bugs that were not already present in master. Also i ran in portfolio mode over a randomized subset of smtlib and we get the same results up to random fluctuations.

Also, just out of curiosity, what are some typical use-cases of this new functionality for you?

Forward tracing: Sometimes I think I can proof something on paper, but vampire can't find the proof. In that case I go through the newly derived clauses step by step and see whether vampire does the same thing as I do, so I can figure out where exactly vampire behaves different from my expectations. Doing this looking at all the new clauses is very long given the amount of clauses derives. This feature lets you look at some relevant subset of all newly derived clauses, to do the same thing much quicker.

Backward tracing: Sometimes looking at what vampire generates i see some rubbish clauses and I wonder how they came about. For that It's useful to see how they've been derived so I can understand what's going on.

[MichaelRawson]

(probably-trivial merge conflicts from #566)