Adding Automatic Rewrite Reasoners - Revision history

imported>Nicolas at 17:33, 24 November 2010

2010-11-24T17:33:31Z

← Older revision		Revision as of 17:33, 24 November 2010
Line 1:		Line 1:
	{{TOCright}}		{{TOCright}}
			''Please also have a look at'' [[How_To_Evolve_Reasoners\| How To Evolve Reasoners]].


	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:		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:

imported>Nicolas: /* Create the Reasoner */

2009-10-06T18:00:14Z

Create the Reasoner

← Older revision		Revision as of 18:00, 6 October 2009
Line 64:		Line 64:

	What left is to implement the formula rewriter which is used in the constructor of the reasoner. This is very convenient by using [http://tom.loria.fr/ Tom].		What left is to implement the formula rewriter which is used in the constructor of the reasoner. This is very convenient by using [http://tom.loria.fr/ Tom].

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

	== Setting up Tom ==		== Setting up Tom ==

imported>Wohuai at 13:14, 7 July 2009

2009-07-07T13:14:09Z

← Older revision		Revision as of 13:14, 7 July 2009
Line 260:		Line 260:

	* 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.		* 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.

			* Run AutoReasonerTests as a JUnit Plug-in Test.

	=== Test the Formula Rewriter ===		=== Test the Formula Rewriter ===
Line 317:		Line 319:

	}		}

			* Run AutoRewriterTests as a JUnit Plug-in Test.

	* The constructor should call the super constructor with an instance of the rewriter under test.		* The constructor should call the super constructor with an instance of the rewriter under test.

imported>Mathieu: cat

2008-09-17T16:53:58Z

cat

← Older revision		Revision as of 16:53, 17 September 2008
Line 325:		Line 325:

	* More instructions about how to use the method predicateTest and expressionTest (along with some other utility methods) can be found in ''org.eventb.core.seqprover.rewriterTests.AbstractFormulaRewriterTests'' class.		* More instructions about how to use the method predicateTest and expressionTest (along with some other utility methods) can be found in ''org.eventb.core.seqprover.rewriterTests.AbstractFormulaRewriterTests'' class.



			[[Category:Developer documentation]]
			[[Category:Rodin Platform]]

imported>Son: /* Setting up Tom */

2008-09-15T17:59:46Z

Setting up Tom

← Older revision		Revision as of 17:59, 15 September 2008
Line 115:		Line 115:
	* At the "Targets" tab:		* At the "Targets" tab:
	** Auto Build: Click ''Set Targets'' and choose "tom" from the list.		** Auto Build: Click ''Set Targets'' and choose "tom" from the list.
	** During a "clean": Click "Set Targets" and choose ''clean'' (unchecked ''tom'').		** During a "clean": Click "Set Targets" and choose ''clean'' (unchecked ''tom'').

	== Implement the Formula Rewriter ==		== Implement the Formula Rewriter ==

imported>Son at 20:53, 14 September 2008

2008-09-14T20:53:05Z

← Older revision		Revision as of 20:53, 14 September 2008
Line 45:		Line 45:

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

Line 100:		Line 100:

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

Line 118:		Line 118:

	== 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.internal.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.implrewrites.RewriterImpl.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).
Line 155:		Line 155:

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

	public ~~AutoRewriterImpl~~() {		public RewriterImpl() {
	super(true, FormulaFactory.getDefault());		super(true, FormulaFactory.getDefault());
	}		}
Line 201:		Line 201:
	* 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''.		* 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''		* 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/RewriterImpl.t''

	== Modify the Tom Task ==		== Modify the Tom Task ==
Line 208:		Line 208:
	* ''Refresh'' tab: Choose "Refresh resource upon completion", and "Specific resources". Click "Specify Resources" and browse to the location of the folder contains the Tom file. In our example, it will be ''src/org/eventb/internal/contributors/seqprover/implrewrites''		* ''Refresh'' tab: Choose "Refresh resource upon completion", and "Specific resources". Click "Specify Resources" and browse to the location of the folder contains the Tom file. In our example, it will be ''src/org/eventb/internal/contributors/seqprover/implrewrites''

	* ''Build Options'' tab: Click "Specify working set of relevant resources". Click "Specify Resources" and browse to the Tom file, i.e. "~~AutoRewriterImpl~~.t".		* ''Build Options'' tab: Click "Specify working set of relevant resources". Click "Specify Resources" and browse to the Tom file, i.e. "RewriterImpl.t".

	* Click Apply and OK to close the dialog.		* Click Apply and OK to close the dialog.

	* The Tom Builder should run and generate the Java implementation for ~~AutoRewriterImpl~~.java in the specified folder.		* The Tom Builder should run and generate the Java implementation for RewriterImpl.java in the specified folder.

	== Test the Reasoner ==		== Test the Reasoner ==
Line 284:		Line 284:
	import org.eventb.core.ast.IFormulaRewriter;		import org.eventb.core.ast.IFormulaRewriter;
	import org.eventb.core.seqprover.rewriterTests.AbstractFormulaRewriterTests;		import org.eventb.core.seqprover.rewriterTests.AbstractFormulaRewriterTests;
	import org.eventb.internal.contributors.seqprover.implrewrites.~~AutoRewriterImpl~~;		import org.eventb.internal.contributors.seqprover.implrewrites.RewriterImpl;
	import org.junit.Test;		import org.junit.Test;

	public class AutoRewriterTests extends AbstractFormulaRewriterTests {		public class AutoRewriterTests extends AbstractFormulaRewriterTests {
	// The automatic rewriter for testing.		// The automatic rewriter for testing.
	private static final IFormulaRewriter rewriter = new ~~AutoRewriterImpl~~();		private static final IFormulaRewriter rewriter = new RewriterImpl();

	/**		/**

imported>Son: /* Test the Formula Rewriter */

2008-09-14T09:14:38Z

Test the Formula Rewriter

← Older revision		Revision as of 09:14, 14 September 2008
Line 280:		Line 280:
	* The implementation looks like this.		* The implementation looks like this.

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

	import org.eventb.core.ast.IFormulaRewriter;		import org.eventb.core.ast.IFormulaRewriter;
Line 287:		Line 287:
	import org.junit.Test;		import org.junit.Test;

	public class ~~AutoReasonerTests~~ extends AbstractFormulaRewriterTests {		public class AutoRewriterTests extends AbstractFormulaRewriterTests {
	// The automatic rewriter for testing.		// The automatic rewriter for testing.
	private static final IFormulaRewriter rewriter = new AutoRewriterImpl();		private static final IFormulaRewriter rewriter = new AutoRewriterImpl();
Line 297:		Line 297:
	* rewriter.		* rewriter.
	*/		*/
	public ~~AutoReasonerTests~~() {		public AutoRewriterTests() {
	super(rewriter);		super(rewriter);
	}		}

imported>Son: /* Test the Formula Rewriter */

2008-09-14T09:12:20Z

Test the Formula Rewriter

← Older revision		Revision as of 09:12, 14 September 2008
Line 264:		Line 264:
	In order to test the formula rewriter, the formula rewriter implementation needs to be visible to the test project.		In order to test the formula rewriter, the formula rewriter implementation needs to be visible to the test project.

	* Open plugin.xml of the project undertest, e.g. ''org.eventb.contributors.seqprover.~~autorewrites~~''		* Open plugin.xml of the project undertest, e.g. ''org.eventb.contributors.seqprover.implrewrites''

	* Click on ''Runtime'' tab.		* Click on ''Runtime'' tab.

imported>Son at 09:11, 14 September 2008

2008-09-14T09:11:26Z

Show changes

imported>Son at 08:50, 14 September 2008

2008-09-14T08:50:36Z

← Older revision		Revision as of 08:50, 14 September 2008
Line 36:		Line 36:

	* The implementation can be as follows:		* The implementation can be as follows:
	package org.eventb.internal.contributors.seqprover.~~autorewrites~~;
			package org.eventb.internal.contributors.seqprover.implrewrites;

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

	public class ~~ImplRewrites~~ extends AbstractAutoRewrites {		public class AutoRewrites extends AbstractAutoRewrites implements IReasoner {

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

	public static String REASONER_ID = "org.eventb.contributors.seqprover.~~autorewrites~~.~~implRewrites~~";		public static String REASONER_ID = "org.eventb.contributors.seqprover.implrewrites.autoRewrites";

	public String getReasonerID() {		public String getReasonerID() {
Line 55:		Line 57:
	@Override		@Override
	protected String getDisplayName() {		protected String getDisplayName() {
	return "implication rewrites";		return "automatic implication rewrites";
	}		}