Difference between revisions of "Adding Automatic Rewrite Reasoners"

From Event-B
Jump to navigationJump to search
imported>Son
imported>Son
Line 21: Line 21:
 
  <extension point="org.eventb.core.seqprover.reasoners">
 
  <extension point="org.eventb.core.seqprover.reasoners">
 
   <reasoner
 
   <reasoner
     class="org.eventb.contributors.seqprover.autorewrites.AutoRewrites"
+
     class="org.eventb.internal.contributors.seqprover.autorewrites.AutoRewrites"
 
     id="autoRewrites"
 
     id="autoRewrites"
 
     name="%autoRewritesName"/>
 
     name="%autoRewritesName"/>
Line 35: Line 35:
  
 
* The implementation can be as follows:
 
* The implementation can be as follows:
 
+
package org.eventb.internal.contributors.seqprover.autorewrites;
 +
 
  import org.eventb.core.ast.IFormulaRewriter;
 
  import org.eventb.core.ast.IFormulaRewriter;
 
  import org.eventb.internal.core.seqprover.eventbExtensions.rewriters.AbstractAutoRewrites;
 
  import org.eventb.internal.core.seqprover.eventbExtensions.rewriters.AbstractAutoRewrites;
Line 79: Line 80:
 
 
 
 
 
   <property name="rewriter.src"
 
   <property name="rewriter.src"
       location="${src}/org/eventb/contributors/seqprover/autorewrites" />
+
       location="${src}/org/eventb/internal/contributors/seqprover/autorewrites" />
 
   
 
   
 
   <target name="init" description="Create the initial time stamp">
 
   <target name="init" description="Create the initial time stamp">
Line 116: Line 117:
  
 
== Implement the Formula Rewriter ==
 
== Implement the Formula Rewriter ==
* Create a Tom file within the same package as the reasoner. In our example, the file should be ''org.eventb.contributors.seqprover.autorewrites.AutoRewriterImpl.t''
+
* Create a Tom file within the same package as the reasoner. In our example, the file should be ''org.eventb.internal.contributors.seqprover.autorewrites.AutoRewriterImpl.t''
  
 
* The content of the file looks like this (for the above rewriting rules).
 
* The content of the file looks like this (for the above rewriting rules).
  
  package org.eventb.contributors.seqprover.autorewrites;
+
  package org.eventb.internal.contributors.seqprover.autorewrites;
 
   
 
   
 
  import java.util.ArrayList;
 
  import java.util.ArrayList;
Line 160: Line 161:
 
   
 
   
 
   %include {Formula.tom}
 
   %include {Formula.tom}
 
+
 
   @Override
 
   @Override
 
   public Predicate rewrite(BinaryPredicate predicate) {
 
   public Predicate rewrite(BinaryPredicate predicate) {
Line 197: Line 198:
 
  }
 
  }
  
*
+
* For more information about using Tom, you can find from the website for [http://tom.loria.fr/ Tom wiki]. The predefined patterns for Event-B is in ''org.eventb.core.ast'' project at the following location ''/tom/Formula.tom''.
 +
 
 +
* An extensive example is in the implementation of the Simplification Rewriter in the ''org.eventb.core.seqprover'' project at this location ''org.eventb.internal.core.seqprover.eventbExtensions.rewrites/AutoRewriterImpl.t''

Revision as of 14:19, 12 September 2008

Beside the input sequent, reasoners of this type does not have any extra input and automatically rewrites all the occurrences of certain formulas. An example of this is the rewriter which rewrites according to the following rules:


  \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}

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.autorewrites. 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, e.g.
<extension point="org.eventb.core.seqprover.reasoners">
  <reasoner
    class="org.eventb.internal.contributors.seqprover.autorewrites.AutoRewrites"
    id="autoRewrites"
    name="%autoRewritesName"/>
</extension>

(add the key autoRewritesName 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.AbstractAutoRewrites. 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 AutoRewrite class is created.
  • The implementation can be as follows:
package org.eventb.internal.contributors.seqprover.autorewrites;

import org.eventb.core.ast.IFormulaRewriter;
import org.eventb.internal.core.seqprover.eventbExtensions.rewriters.AbstractAutoRewrites;
import org.eventb.core.seqprover.IReasoner;

public class AutoRewrites extends AbstractAutoRewrites {

  public AutoRewrites() {
    super(new AutoRewriterImpl(), true);
  }

  public static String REASONER_ID = "org.evenb.contributors.seqprover.autoRewrites";

  public String getReasonerID() {
    return REASONER_ID;
  }

  @Override
  protected String getDisplayName() {
    return "simplification rewrites";
  }

}

The constructor must call the super constructor method super(IFormulaRewriter, boolean) to specify the formula rewriter to use and the resulting reasoner should hide the source of the rewritten hypothesis or not. Clients need to implement two methods. The first one, namely getReasonerID(), return the string ID of this reasoner. This must be the same ID as declared in the plugin.xml file (do not forget the project name prefix). The second method is getDisplayName() which return the display name of the reasoner, which will be used for displaying in the UI.

What left is to implement the formula rewriter which is used in the constructor of the reasoner. This is very convenient by using Tom.

Setting up Tom

  • Create a file named build-tom.xml within your project. The content of the file looks like this.
<project name="org.eventb.contributors.seqprover.autorewrites" default="tom" basedir=".">
  <description>
    Generates derived files in the Sequent Prover.
  </description>

  <property name="src" location="src" />

  <property name="org.eventb.core.ast.home" location="../org.eventb.core.ast" />
  <import file="${org.eventb.core.ast.home}/tom/tom-task.xml"/>
	
  <property name="rewriter.src"
      location="${src}/org/eventb/internal/contributors/seqprover/autorewrites" />

  <target name="init" description="Create the initial time stamp">
    <tstamp />
  </target>

  <target name="tom" depends="init"
      description="Launch tom for all files">
    <tom config="${tom.home}/Tom.xml"
        srcdir="${src}"
        destdir="${src}"
        options="-I ${org.eventb.core.ast.home}/tom --static"
        pretty="true"
        optimize="true">
      <include name="**/*.t" />
    </tom>
  </target>

  <target name="clean" description="clean up">
    <delete file="${rewriter.src}/AutoRewriterImpl.java" />
  </target>
	
</project>

The best way to create this file is to copy from org.eventb.core.seqprover project, and modify this accordingly.

  • Right click on the name of your project and choose Properties.
  • Choose "Builders", then click on "New" and choose "Ant Build" and click OK. A dialog will open for new builder wizard.
  • At the "Main" tab:
    • Enter the name of the builder, e.g. Tom Builder.
    • Buildfile: Browse Workspace to your build-tom.xml.
    • Base Directory: Variables and choose build_project.
  • At the "Targets" tab:
    • Auto Build: Click Set Targets and choose "tom" from the list.
    • During a "clean": Click "Set Targets" and choose clean (unchecked tom).

Implement the Formula Rewriter

  • Create a Tom file within the same package as the reasoner. In our example, the file should be org.eventb.internal.contributors.seqprover.autorewrites.AutoRewriterImpl.t
  • The content of the file looks like this (for the above rewriting rules).
package org.eventb.internal.contributors.seqprover.autorewrites;

import java.util.ArrayList;
import java.util.Collection;
import java.math.BigInteger;

import org.eventb.core.ast.AssociativeExpression;
import org.eventb.core.ast.AssociativePredicate;
import org.eventb.core.ast.AtomicExpression;
import org.eventb.core.ast.BinaryExpression;
import org.eventb.core.ast.BinaryPredicate;
import org.eventb.core.ast.BoolExpression;
import org.eventb.core.ast.BoundIdentDecl;
import org.eventb.core.ast.BoundIdentifier;
import org.eventb.core.ast.DefaultRewriter;
import org.eventb.core.ast.Expression;
import org.eventb.core.ast.Formula;
import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.FreeIdentifier;
import org.eventb.core.ast.Identifier;
import org.eventb.core.ast.IntegerLiteral;
import org.eventb.core.ast.LiteralPredicate;
import org.eventb.core.ast.Predicate;
import org.eventb.core.ast.QuantifiedExpression;
import org.eventb.core.ast.QuantifiedPredicate;
import org.eventb.core.ast.RelationalPredicate;
import org.eventb.core.ast.SetExtension;
import org.eventb.core.ast.SimplePredicate;
import org.eventb.core.ast.UnaryExpression;
import org.eventb.core.ast.UnaryPredicate;
import org.eventb.core.seqprover.eventbExtensions.Lib;

@SuppressWarnings("unused")
public class AutoRewriterImpl extends DefaultRewriter {

  public AutoRewriterImpl() {
    super(true, FormulaFactory.getDefault());
  }

  %include {Formula.tom}

  @Override
  public Predicate rewrite(BinaryPredicate predicate) {
    %match (Predicate predicate) {
      /**
       * Implication 1: ⊤ ⇒ P == P
       */
      Limp(BTRUE(), P) -> {
        return `P;
      }

      /**
       * Implication 2: ⊥ ⇒ P == ⊤
       */
      Limp(BFALSE(), _) -> {
        return Lib.True;
      }

      /**
       * Implication 3: P ⇒ ⊤ == ⊤
       */
      Limp(_, BTRUE()) -> {
        return predicate.getRight();
      }
    	
      /**
       * Implication 4: P ⇒ ⊥ == ¬P
       */
      Limp(P, BFALSE()) -> {
        return Lib.makeNeg(`P);
      }
    }

    return predicate;
  }
}
  • For more information about using Tom, you can find from the website for Tom wiki. The predefined patterns for Event-B is in org.eventb.core.ast project at the following location /tom/Formula.tom.
  • An extensive example is in the implementation of the Simplification Rewriter in the org.eventb.core.seqprover project at this location org.eventb.internal.core.seqprover.eventbExtensions.rewrites/AutoRewriterImpl.t