2020-02-17 16:40:30 (GMT)
What is the difference between SimplSet and ActiveSet in proofState.ml? The saturation loop seems to do the same operations on both of them.
2020-02-17 17:57:30 (GMT)
They both contain active clauses (in the current discount loop; in Otter loop, they'd be distinct as SimplSet could also contain passive clauses).
The difference is mostly seen in superposition.ml where their content is used for different operations, like demodulation or superposition.
2020-02-18 8:35:33 (GMT)
Ok, I see. So it is an invariant of the current implementation that the passive clauses are never used for simplification, right?
2020-02-18 13:59:17 (GMT)
Yes, because they're not added to SimpSet. That's the only thing to change if we wanted an Otter loop.