Adding Manual Rewrite Reasoners

Manual rewrite Reasoners of this type apply a rewriting rule for a given formula (or sub-formula) in the goal or in one of the hypotheses. Hence beside the input sequent, reasoners of this type have an extra input to specify the location of the (sub-)formula where the rewriting should carry out. We take the example of which rewrites according to the following rules for implication.

$\begin{array}{rcl} \top \limp P & \Rightarrow & P \\ P \limp \top & \Rightarrow & \top \\ \bot \limp P & \Rightarrow & \top \\ P \limp \bot & \Rightarrow & \neg P \end{array}$

We can reuse some of the code that we already developed for the automatic rewrite reasoner.

Below are the step by step instructions to create an automatic rewrite reasoner:

Create the Reasoner

• Create a new plug-in project, e.g. org.eventb.contributors.seqprover.implrewrites. Deselect the plug-in options for "Generating an activator" and "Contribution to the UI".

• Add dependency on the project org.eventb.core.seqprover

• Add an extension for org.eventb.core.seqprover.reasoners for our implication rewrite reasoner, e.g.

<extension point="org.eventb.core.seqprover.reasoners">
  <reasoner
    class="org.eventb.internal.contributors.seqprover.implrewrites.ManualRewrites"
    id="manualRewrites"
    name="%manualRewritesName"/>
</extension>

(add the key manualRewritesName to the plugin.properties accordingly).

• Click on the class attribute of the newly created extension. A dialog appears for new class wizard.

• The abstract implementation of this class is org.eventb.internal.core.seqprover.eventbExtensions.rewriters.AbstractManualRewrites. Choose this as the Superclass in the new class wizard. (For the moment, the class is internal within the project and subjected to be changed. Clients can make a copy of this class to develop their own implementation).

• Finish the wizard and a new implementation for ManualRewrites class is created.

• The implementation can be as follows:

package org.eventb.internal.contributors.seqprover.implrewrites;

import org.eventb.core.ast.IPosition;
import org.eventb.core.ast.Predicate;
import org.eventb.internal.core.seqprover.eventbExtensions.rewriters.AbstractManualRewrites;

public class ManualRewrites extends AbstractManualRewrites {

  public ManualRewrites() {
    super(new RewriterImpl());
  }

  public static final String REASONER_ID = "org.eventb.contributors.seqprover.implrewrites.manualRewrites";

  @Override
  protected String getDisplayName(Predicate pred, IPosition position) {
    if (pred != null)
      return "implication rewrites in " + pred.getSubFormula(position);
    return "implication rewrites in goal";
  }

  public String getReasonerID() {
    return REASONER_ID;
  }

}

• This reasoner used the same formula rewriter that has been developed for automatic rewrite reasoner. The rewriter is created in the constructor.

• In some cases, more complicated reasoners can be implemented by overriding certain methods of the class AbstractManualRewrites.