Previously, we did not have a way to produce a proof of unsatisfiability from the Spacer engine.
I thought of two possibilities: either log the proof obligations, building the proof from bottom to leaves, or log the must summaries, building the proof from leaves to bottom.
I decided to go for the latter, since it seems like less bookkeeping. For each must summary, we now also remember what were its premises, i.e., from which constrained predicates and using which edge we can derive the current must summary (constrained fact in current node). This is almost the same as our proof format, but not quite. Single must summary can cover a large set of states, in the proof format we want to pick single state.
We solve this by post-processing the database of must summaries to pick for each one a single state.
Previously, we did not have a way to produce a proof of unsatisfiability from the Spacer engine. I thought of two possibilities: either log the proof obligations, building the proof from bottom to leaves, or log the must summaries, building the proof from leaves to bottom. I decided to go for the latter, since it seems like less bookkeeping. For each must summary, we now also remember what were its premises, i.e., from which constrained predicates and using which edge we can derive the current must summary (constrained fact in current node). This is almost the same as our proof format, but not quite. Single must summary can cover a large set of states, in the proof format we want to pick single state. We solve this by post-processing the database of must summaries to pick for each one a single state.