Adding Reasoners(How to extend Rodin Tutorial) - Revision history

Guillaume: Antecedent and needed hypotheses were mixed up

2021-09-21T15:43:52Z

Antecedent and needed hypotheses were mixed up

← Older revision		Revision as of 15:43, 21 September 2021
Line 23:		Line 23:
	[[Image:Adding_Reasoners_DBL_INEQ_Reasoner.png\|550px\|center]]		[[Image:Adding_Reasoners_DBL_INEQ_Reasoner.png\|550px\|center]]

	Moreover, <math>\textbf{H}</math> is the set of selected hypotheses from the input sequent, and <math> a ~~\leq~~ b~~,\;b \leq a~~\;\vdash \;\textbf{G}</math> is the antecedent of the rule (i.e. a child node to be proved).		Moreover, <math>\textbf{H}</math> is the set of selected hypotheses from the input sequent, and <math> a = b\;\vdash \;\textbf{G}</math> is the antecedent of the rule (i.e. a child node to be proved).

	=== Step1 ===		=== Step1 ===

imported>Tommy: /* Conclusion */

2013-09-05T14:21:11Z

Conclusion

← Older revision		Revision as of 14:21, 5 September 2013
Line 201:		Line 201:

	N.B: if you don't see any application of our reasoner, you might have forgotten to select the corresponding tactic to the auto tactic profile which is applied.		N.B: if you don't see any application of our reasoner, you might have forgotten to select the corresponding tactic to the auto tactic profile which is applied.
	Go to ''Window > Prefences'', and then in ''Event-B category > Sequent Prover'', select the "Auto/Post Tactic" preferences and create a new profile and add the ''Double Inequality Tactic'' to it.		Go to ''Window > Prefences'', and then in ''Event-B category > Sequent Prover'', select the "Auto/Post Tactic" preferences and create a new profile and add the ''Double Inequality Tactic'' to it.<br />
	~~See~~ the picture below :		You can select it from the list on the left within the profile editor (see the picture below):

	[[Image:DBL_INEQ_Preferences.png\|650px]]		[[Image:DBL_INEQ_Preferences.png\|650px]]

imported>Tommy: /* Conclusion */

2013-09-05T14:19:57Z

Conclusion

← Older revision		Revision as of 14:19, 5 September 2013
Line 201:		Line 201:

	N.B: if you don't see any application of our reasoner, you might have forgotten to select the corresponding tactic to the auto tactic profile which is applied.		N.B: if you don't see any application of our reasoner, you might have forgotten to select the corresponding tactic to the auto tactic profile which is applied.
	Go to ''Window > Prefences'', and then in ''Event-B category > Sequent Prover'', select the "Auto/Post Tactic" preferences and create a new profile ~~from the Default Auto Tactic Profile~~ and add the ''Double Inequality Tactic'' to it.		Go to ''Window > Prefences'', and then in ''Event-B category > Sequent Prover'', select the "Auto/Post Tactic" preferences and create a new profile and add the ''Double Inequality Tactic'' to it.
	See the picture below :		See the picture below :

imported>Tommy: /* Conclusion */

2013-09-05T14:16:50Z

Conclusion

← Older revision		Revision as of 14:16, 5 September 2013
Line 200:		Line 200:
	By running the auto-provers, you should see that the Inequality Rewrites is applied.		By running the auto-provers, you should see that the Inequality Rewrites is applied.

	N.B: if you don't see any application of our reasoner, you might have forgotten to select the corresponding tactic ~~and~~ to ~~put it in~~ the auto ~~tactics preferences !~~		N.B: if you don't see any application of our reasoner, you might have forgotten to select the corresponding tactic to the auto tactic profile which is applied.
	Go to ''Window > Prefences'', and then in ''Event-B category > Sequent Prover'', select the ~~auto-tactics~~ preferences and ~~make~~ the ''Double Inequality Tactic'' ~~be selected~~.		Go to ''Window > Prefences'', and then in ''Event-B category > Sequent Prover'', select the "Auto/Post Tactic" preferences and create a new profile from the Default Auto Tactic Profile and add the ''Double Inequality Tactic'' to it.
	See the picture below :		See the picture below :

imported>Tommy: /* Step7 */

2013-09-05T14:09:50Z

Step7

← Older revision		Revision as of 14:09, 5 September 2013
Line 194:		Line 194:
	4 }		4 }
	where at line 2 we encapsulate the reasoner call, and at line 3, we apply the reasoner.		where at line 2 we encapsulate the reasoner call, and at line 3, we apply the reasoner.

	~~=== Step7 ===~~
	~~This is the last step that we need to accomplish to add our reasoner to the sequent prover.<br>~~
	~~We need to reference our tactic by creating a tactic extension from the <tt>org.eventb.core.pomTactics</tt> extension point.<br>~~
	~~This will inform the proof obligation manager about our tactic. Note that, each added tactic should be reference with the tactic extension of the extension point above.~~

	So simply add the <tt>org.eventb.core.pomTactics</tt> extension point to the plug-in and create a ''tactic'' extension with the (complete) id of our auto-tactic : <tt>org.eventb.doubleInequality.dblIneqTac</tt>.

	=== Conclusion ===		=== Conclusion ===

imported>Tommy: /* Step6 */

2013-09-05T14:09:08Z

Step6

← Older revision		Revision as of 14:09, 5 September 2013
Line 154:		Line 154:
	:- ''name : Double Inequality Tactic'',<br>		:- ''name : Double Inequality Tactic'',<br>
	:- ''description : Applies Double Inequality Rule'',<br>		:- ''description : Applies Double Inequality Rule'',<br>
			:- ''auto : place the boolean to <tt>true</tt> to let the tactic be automatic'',<br>
			:- ''post : place the boolean to <tt>true</tt> so the tactic will no execute as a post tactic'',<br>
	:- And now it remains the tactic ''class'' to create. So, create the tactic class <tt>DoubleInequalityTactic</tt> which <tt>implements ITactic</tt>.<br>		:- And now it remains the tactic ''class'' to create. So, create the tactic class <tt>DoubleInequalityTactic</tt> which <tt>implements ITactic</tt>.<br>

imported>Tommy: /* Step1 */

2013-09-05T14:06:29Z

Step1

← Older revision		Revision as of 14:06, 5 September 2013
Line 27:		Line 27:
	=== Step1 ===		=== Step1 ===
	* Create a new plugin that will host our reasoner and tactic. It will not be any activator for this plug-in but the option "Activate this plug-in when one of its classes is loaded" shall be selected.		* Create a new plugin that will host our reasoner and tactic. It will not be any activator for this plug-in but the option "Activate this plug-in when one of its classes is loaded" shall be selected.
	* Add a dependencies to the plug-ins <tt>org.eclipse.core.resources</tt>, <tt>org.eclipse.core.runtime</tt>, <tt>org.eclipse.ui</tt>, <tt>org.rodinp~~.core</tt>, tt>org.eventb~~.core</tt>, <tt>org.eventb.core.ast</tt>,<tt>org.eventb.core.seqprover</tt> and <tt>org.eventb.core</tt>.		* Add a dependencies to the plug-ins <tt>org.eclipse.core.resources</tt>, <tt>org.eclipse.core.runtime</tt>, <tt>org.eclipse.ui</tt>, <tt>org.rodinp.core</tt>, <tt>org.eventb.core.ast</tt>,<tt>org.eventb.core.seqprover</tt> and <tt>org.eventb.core</tt>.
	* Add the extension point <tt>org.eventb.core.seaqprover.reasoners</tt>, and create a 'reasoner' extension for our reasoner with ''"id : dblIneq"'' and ''"name : Double Inequality"'' and finally,		* Add the extension point <tt>org.eventb.core.seaqprover.reasoners</tt>, and create a 'reasoner' extension for our reasoner with ''"id : dblIneq"'' and ''"name : Double Inequality"'' and finally,
	* Create a new class for the reasoner, called <tt>DoubleInequalityReasoner</tt>.		* Create a new class for the reasoner, called <tt>DoubleInequalityReasoner</tt>.

imported>Tommy: /* Step1 */

2013-09-05T14:05:11Z

Step1

← Older revision		Revision as of 14:05, 5 September 2013
Line 27:		Line 27:
	=== Step1 ===		=== Step1 ===
	* Create a new plugin that will host our reasoner and tactic. It will not be any activator for this plug-in but the option "Activate this plug-in when one of its classes is loaded" shall be selected.		* Create a new plugin that will host our reasoner and tactic. It will not be any activator for this plug-in but the option "Activate this plug-in when one of its classes is loaded" shall be selected.
	* Add a ~~dependency~~ to the plug-in <tt>org.eventb.core</tt>.		* Add a dependencies to the plug-ins <tt>org.eclipse.core.resources</tt>, <tt>org.eclipse.core.runtime</tt>, <tt>org.eclipse.ui</tt>, <tt>org.rodinp.core</tt>, tt>org.eventb.core</tt>, <tt>org.eventb.core.ast</tt>,<tt>org.eventb.core.seqprover</tt> and <tt>org.eventb.core</tt>.
	* Add the extension point <tt>org.eventb.core.seaqprover.reasoners</tt>, and create a 'reasoner' extension for our reasoner with ''"id : dblIneq"'' and ''"name : Double Inequality"'' and finally,		* Add the extension point <tt>org.eventb.core.seaqprover.reasoners</tt>, and create a 'reasoner' extension for our reasoner with ''"id : dblIneq"'' and ''"name : Double Inequality"'' and finally,
	* Create a new class for the reasoner, called <tt>DoubleInequalityReasoner</tt>.		* Create a new class for the reasoner, called <tt>DoubleInequalityReasoner</tt>.

imported>Tommy: /* Step6 */

2010-10-16T16:47:35Z

Step6

← Older revision		Revision as of 16:47, 16 October 2010
Line 163:		Line 163:
	public Object apply(IProofTreeNode ptNode, IProofMonitor pm) {		public Object apply(IProofTreeNode ptNode, IProofMonitor pm) {

	* First, we search for double inequalities ''a <= b'' and ''b <= a'' in the selected hypotheses. To search it, we traverse all the selected hypotheses via <tt>sequent.selectedHypIterable()</tt> then when we encounter one hypothesis of the form E <= F (e.g. hypothesis.getTag() == Formula.LE) then we build the hypothesis F <= E and if the sequent contains this latter hypothesis, we call the reasoner DoubleInequalityReasoner.		* First, we search for double inequalities ''a <= b'' and ''b <= a'' in the selected hypotheses. To search it, we traverse all the selected hypotheses via <tt>sequent.selectedHypIterable()</tt>.

	final IProverSequent sequent = ptNode.getSequent();		final IProverSequent sequent = ptNode.getSequent();
Line 169:		Line 169:
	for (Predicate hyp : sequent.selectedHypIterable()) {		for (Predicate hyp : sequent.selectedHypIterable()) {

	* when we encounter one hypothesis of the form E <= F (e.g. hypothesis.getTag() == Formula.LE), then we build the hypothesis F <= E :		* Then, when we encounter one hypothesis of the form E <= F (e.g. hypothesis.getTag() == Formula.LE), then we build the hypothesis F <= E :
	if (hyp.getTag() == Formula.LE) {		if (hyp.getTag() == Formula.LE) {
	final RelationalPredicate aLEb = (RelationalPredicate) hyp;		final RelationalPredicate aLEb = (RelationalPredicate) hyp;

imported>Tommy: /* Step5 */

2010-10-16T16:44:39Z

Step5

← Older revision		Revision as of 16:44, 16 October 2010
Line 131:		Line 131:
	=== Step5 ===		=== Step5 ===

	As our input is actually a SinglePredInput, which as its name describes, holds a predicate, our reasoner is actually an specialisation of the abstract class SinglePredInputReasoner.		As our input is actually a SinglePredInput, which as its name describes, holds a predicate, our reasoner is actually a specialisation of the abstract class SinglePredInputReasoner.
	Please check the other proposed (e.g. published) types of reasoners corresponding to existing inputs among :		Please check the other proposed (e.g. published) types of reasoners corresponding to existing inputs among :
	* SingleExprInputReasoner,		* SingleExprInputReasoner,