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.

Test the Reasoner

If clients just use the simple implementation above, they only need to test if the reasoner has been declared correctly (testing the reasoner ID), and the formula rewriter used for this reasoner has been implemented correctly.

Test the Declaration

Follow the steps below to create a test for declaration of the newly created reasoner.

• Create a test plug-in project, e.g. org.eventb.contributors.seqprover.implrewrites.tests

• Create dependencies on org.eventb.core.seqprover.tests and the project under test (in our example, it is org.eventb.contributors.seqprover.implrewrites.

• Create a package for the tests, e.g. org.eventb.internal.contributors.seqprover.implrewrites.tests

• Create a new class within the newly created package. This class will extend this abstract test class org.eventb.core.seqprover.rewriterTests.AbstractAutomaticReasonerTests.

• The content of the test class is as follows

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

import java.util.List;

import org.eventb.core.ast.IPosition;
import org.eventb.core.ast.Predicate;
import org.eventb.core.seqprover.eventbExtensions.Tactics;
import org.eventb.core.seqprover.eventbExtentionTests.AbstractManualReasonerTests;
import org.eventb.internal.contributors.seqprover.implrewrites.RewriterImpl;

public class ManualReasonerTests extends AbstractManualReasonerTests {

  @Override
  public String getReasonerID() {
    return "org.eventb.contributors.seqprover.implrewrites.manualRewrites";
  }

  @Override
  protected List<IPosition> getPositions(Predicate predicate) {
    return Tactics.getPositions(new RewriterImpl(), predicate);
  }

  @Override
  protected String[] getTestGetPositions() {
    return new String[] {
        "⊤ ⇒ x = 1", "ROOT",
        "x = 1 ⇒ ⊤", "ROOT",
        "⊥ ⇒ x = 1", "ROOT",
        "x = 1 ⇒ ⊥", "ROOT",
        "(x = 1 ⇒ ⊥) ∧ (x = 1 ⇒ ⊤)", "0\n" + "1",
        "((x = 1 ⇒ ⊥) ∧ x = 1) ⇒ ⊤", "ROOT\n" + "0.0",
    };
  }

  @Override
  public SuccessfullReasonerApplication[] getSuccessfulReasonerApplications() {
    return new SuccessfullReasonerApplication[] {};
  }

  @Override
  public UnsuccessfullReasonerApplication[] getUnsuccessfullReasonerApplications() {
    return new UnsuccessfullReasonerApplication[]{};
  }

}

• As mentioned before, clients only need to test if the reasoner ID has been declared correctly. This is done by implemented the method String getReasonerID() which should return the correct reasoner ID.

Test the Formula Rewriter

In order to test the formula rewriter, the formula rewriter implementation needs to be visible to the test project.