From f7ffbfcb6f54e46e1531e51be8c2d36834bebd78 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Wed, 22 May 2013 12:07:33 +0200
Subject: [PATCH] provide disprover as an auto tactic
---
de.prob.eventb.disprover.core/plugin.xml | 9 +++++++++
.../core/internal/DisproverAutoTactic.java | 16 ++++++++++++++++
2 files changed, 25 insertions(+)
create mode 100644 de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverAutoTactic.java
diff --git a/de.prob.eventb.disprover.core/plugin.xml b/de.prob.eventb.disprover.core/plugin.xml
index a6445540..30a8c2e7 100644
--- a/de.prob.eventb.disprover.core/plugin.xml
+++ b/de.prob.eventb.disprover.core/plugin.xml
@@ -9,5 +9,14 @@
name="%reasoner.name">
</reasoner>
</extension>
+ <extension
+ point="org.eventb.core.seqprover.autoTactics">
+ <autoTactic
+ class="de.prob.eventb.disprover.core.internal.DisproverAutoTactic"
+ description="%autotactic.desc"
+ id="disproverTactic"
+ name="%autotactic.name">
+ </autoTactic>
+ </extension>
</plugin>
diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverAutoTactic.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverAutoTactic.java
new file mode 100644
index 00000000..8c1e9db7
--- /dev/null
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverAutoTactic.java
@@ -0,0 +1,16 @@
+package de.prob.eventb.disprover.core.internal;
+
+import org.eventb.core.seqprover.ITactic;
+import org.eventb.core.seqprover.eventbExtensions.AutoTactics.AbsractLazilyConstrTactic;
+import org.eventb.core.seqprover.tactics.BasicTactics;
+
+import de.prob.eventb.disprover.core.DisproverReasonerInput;
+
+
+public class DisproverAutoTactic extends AbsractLazilyConstrTactic {
+ @Override
+ protected ITactic getSingInstance() {
+ return BasicTactics.reasonerTac(new DisproverReasoner(),
+ new DisproverReasonerInput());
+ }
+}
\ No newline at end of file
--
GitLab