Adding Manual Rewrite Reasoners

Please also have a look at How To Evolve Reasoners.

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.

Note: in order to avoid problems with subsequent reasoner implementation evolutions, it would be wise to implement a versioned reasoner (one more simple method).

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), the applicable positions, and the formula rewriter used for this reasoner has been implemented correctly.

Test the Declaration and Applicable Positions

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.

• Moreover, the client need to implement the method for testing applicable position. The return value is an array of string where every pair of strings represent the input formula and the expected output which represent a lists of positions. The applicable position is get from getPositions(Predicate predicate) method. In our case, it just uses the utility method to return the applicable rewrite position with the corresponding rewriter.

Test the Formula Rewriter

See Test the Formula Rewriter for automatic rewrite reasoners.

More Complicated Tests

For more complicated reasoners (i.e. ones which involves overriding the methods of AbstractManualRewrites), clients need to implemented the tests accordingly by implementing the corresponding methods of AbstractManualReasonerTests.