Adding Manual Rewrite Reasoners - Revision history

imported>Nicolas at 17:31, 24 November 2010

2010-11-24T17:31:35Z

← Older revision		Revision as of 17:31, 24 November 2010
Line 1:		Line 1:
	{{TOCright}}		{{TOCright}}
			''Please also have a look at'' [[How_To_Evolve_Reasoners\| 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.		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.

imported>Nicolas: /* Create the Reasoner */ Added link to Versioned Reasoners

2009-10-06T18:01:42Z

Create the Reasoner: Added link to Versioned Reasoners

← Older revision		Revision as of 18:01, 6 October 2009
Line 69:		Line 69:

	* In some cases, more complicated reasoners can be implemented by overriding certain methods of the class ''AbstractManualRewrites''.		* 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 Reasoners\|versioned reasoner]] (one more simple method).

	== Test the Reasoner ==		== Test the Reasoner ==

imported>Mathieu: cat

2008-09-17T16:59:09Z

cat

← Older revision		Revision as of 16:59, 17 September 2008
Line 141:		Line 141:
	=== More Complicated Tests ===		=== 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''.		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''.


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

imported>Mathieu at 16:56, 17 September 2008

2008-09-17T16:56:03Z

← Older revision		Revision as of 16:56, 17 September 2008
Line 1:		Line 1:
			{{TOCright}}
	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.		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.

imported>Son at 13:49, 15 September 2008

2008-09-15T13:49:34Z

← Older revision		Revision as of 13:49, 15 September 2008
Line 1:		Line 1:
	~~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.		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.

	<math>		<math>

imported>Son: /* Test the Reasoner */

2008-09-15T12:15:57Z

Test the Reasoner

← Older revision		Revision as of 12:15, 15 September 2008
Line 70:		Line 70:

	== Test the Reasoner ==		== 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.		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 ===		=== Test the Declaration and Applicable Positions ===
	Follow the steps below to create a test for declaration of the newly created reasoner.		Follow the steps below to create a test for declaration of the newly created reasoner.

Line 132:		Line 132:

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

			* 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 ===		=== Test the Formula Rewriter ===

imported>Son: /* More Complicated Tests */

2008-09-15T12:12:18Z

More Complicated Tests

← Older revision		Revision as of 12:12, 15 September 2008
Line 137:		Line 137:

	=== More Complicated Tests ===		=== More Complicated Tests ===
	For more complicated reasoners (i.e. ones which involves overriding the methods of ''~~AbstractManualReasoner~~''), clients need to implemented the tests accordingly by implementing the corresponding methods of ''AbstractManualReasonerTests''.		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''.

imported>Son: /* More Complicated Tests */

2008-09-15T12:11:51Z

More Complicated Tests

← Older revision		Revision as of 12:11, 15 September 2008
Line 137:		Line 137:

	=== More Complicated Tests ===		=== More Complicated Tests ===
			For more complicated reasoners (i.e. ones which involves overriding the methods of ''AbstractManualReasoner''), clients need to implemented the tests accordingly by implementing the corresponding methods of ''AbstractManualReasonerTests''.

imported>Son: /* Test the Reasoner */

2008-09-15T12:08:10Z

Test the Reasoner

← Older revision		Revision as of 12:08, 15 September 2008
Line 135:		Line 135:
	=== Test the Formula Rewriter ===		=== Test the Formula Rewriter ===
	See [[Adding Automatic Rewrite Reasoners#Test the Formula Rewriter \| Test the Formula Rewriter]] for automatic rewrite reasoners.		See [[Adding Automatic Rewrite Reasoners#Test the Formula Rewriter \| Test the Formula Rewriter]] for automatic rewrite reasoners.

			=== More Complicated Tests ===

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

2008-09-15T12:07:39Z

Test the Formula Rewriter

← Older revision		Revision as of 12:07, 15 September 2008
Line 134:		Line 134:

	=== Test the Formula Rewriter ===		=== Test the Formula Rewriter ===
	~~In order to test~~ the ~~formula rewriter,~~ the ~~formula rewriter implementation needs to be visible to the test project~~.		See [[Adding Automatic Rewrite Reasoners#Test the Formula Rewriter \| Test the Formula Rewriter]] for automatic rewrite reasoners.