Disprover should report needed hypotheses back to Rodin

Description

Currently, when the Disprover is able to discharge a proof obligation, we do not submit which hypotheses were used:

return ProverFactory.makeProofRule(this, input, sequent.goal(),
null, IConfidence.DISCHARGED_MAX,
"ProB (no enumeration / all cases checked)");

We should replace "null" by a set of predicates used to discharge the po. That way, Rodin would be able to replay to proof if the model changes and it is still applicable.

Environment

None

Gliffy Diagrams

Activity

Show:

Details

Assignee

Reporter

Priority

Created June 4, 2014 at 10:37 AM
Updated June 4, 2014 at 10:37 AM