Skip to content
Snippets Groups Projects
Commit a4b7b7a7 authored by Sebastian Krings's avatar Sebastian Krings
Browse files

fix disprover on rodin3

parent 312b391e
No related branches found
No related tags found
No related merge requests found
package de.prob.eventb.disprover.core; package de.prob.eventb.disprover.core;
import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.ITypeEnvironment;
import org.eventb.core.seqprover.IReasonerInput; import org.eventb.core.seqprover.IReasonerInput;
import org.eventb.core.seqprover.ITranslatableReasonerInput;
import org.eventb.core.seqprover.proofBuilder.ReplayHints; import org.eventb.core.seqprover.proofBuilder.ReplayHints;
/** /**
...@@ -11,7 +14,8 @@ import org.eventb.core.seqprover.proofBuilder.ReplayHints; ...@@ -11,7 +14,8 @@ import org.eventb.core.seqprover.proofBuilder.ReplayHints;
* *
* @author jastram * @author jastram
*/ */
public class DisproverReasonerInput implements IReasonerInput { public class DisproverReasonerInput implements IReasonerInput,
ITranslatableReasonerInput {
@Override @Override
public void applyHints(ReplayHints renaming) { public void applyHints(ReplayHints renaming) {
// TODO Auto-generated method stub // TODO Auto-generated method stub
...@@ -29,4 +33,16 @@ public class DisproverReasonerInput implements IReasonerInput { ...@@ -29,4 +33,16 @@ public class DisproverReasonerInput implements IReasonerInput {
return false; return false;
} }
@Override
public ITypeEnvironment getTypeEnvironment(FormulaFactory arg0) {
// TODO Auto-generated method stub
return null;
}
@Override
public IReasonerInput translate(FormulaFactory arg0) {
// TODO Auto-generated method stub
return null;
}
} }
...@@ -3,12 +3,14 @@ package de.prob.eventb.disprover.ui; ...@@ -3,12 +3,14 @@ package de.prob.eventb.disprover.ui;
import java.util.Collections; import java.util.Collections;
import java.util.List; import java.util.List;
import org.eclipse.swt.graphics.Image;
import org.eventb.core.ast.Predicate; import org.eventb.core.ast.Predicate;
import org.eventb.core.seqprover.IProofTreeNode; import org.eventb.core.seqprover.IProofTreeNode;
import org.eventb.core.seqprover.IReasonerInput; import org.eventb.core.seqprover.IReasonerInput;
import org.eventb.core.seqprover.ITactic; import org.eventb.core.seqprover.ITactic;
import org.eventb.core.seqprover.tactics.BasicTactics; import org.eventb.core.seqprover.tactics.BasicTactics;
import org.eventb.ui.prover.DefaultTacticProvider; import org.eventb.ui.prover.DefaultTacticProvider;
import org.eventb.ui.prover.IPredicateApplication;
import org.eventb.ui.prover.ITacticApplication; import org.eventb.ui.prover.ITacticApplication;
import de.prob.eventb.disprover.core.Disprover; import de.prob.eventb.disprover.core.Disprover;
...@@ -20,22 +22,10 @@ public class DisproverTacticProvider extends DefaultTacticProvider { ...@@ -20,22 +22,10 @@ public class DisproverTacticProvider extends DefaultTacticProvider {
return false; return false;
} }
protected static class MyPredicateApplication implements ITacticApplication { protected static class MyPredicateApplication implements
IPredicateApplication {
private final IProofTreeNode node;
public MyPredicateApplication(IProofTreeNode node) {
this.node = node;
}
@Override @Override
public ITactic getTactic(String[] inputs, String globalInput) { public ITactic getTactic(String[] inputs, String globalInput) {
return getTactic(node, globalInput, inputs);
}
public ITactic getTactic(IProofTreeNode node, String globalInput,
String[] inputs) {
IReasonerInput reasonerInput = new DisproverReasonerInput(); IReasonerInput reasonerInput = new DisproverReasonerInput();
return BasicTactics.reasonerTac( return BasicTactics.reasonerTac(
Disprover.createDisproverReasoner(), reasonerInput); Disprover.createDisproverReasoner(), reasonerInput);
...@@ -46,6 +36,18 @@ public class DisproverTacticProvider extends DefaultTacticProvider { ...@@ -46,6 +36,18 @@ public class DisproverTacticProvider extends DefaultTacticProvider {
return "de.prob.eventb.disprover.ui.disproverTactic"; return "de.prob.eventb.disprover.ui.disproverTactic";
} }
@Override
public Image getIcon() {
// TODO Auto-generated method stub
return null;
}
@Override
public String getTooltip() {
// TODO Auto-generated method stub
return null;
}
} }
public DisproverTacticProvider() { public DisproverTacticProvider() {
...@@ -57,7 +59,7 @@ public class DisproverTacticProvider extends DefaultTacticProvider { ...@@ -57,7 +59,7 @@ public class DisproverTacticProvider extends DefaultTacticProvider {
IProofTreeNode node, Predicate hyp, String globalInput) { IProofTreeNode node, Predicate hyp, String globalInput) {
if (node != null && node.isOpen()) { if (node != null && node.isOpen()) {
ITacticApplication application = new MyPredicateApplication(node); ITacticApplication application = new MyPredicateApplication();
return Collections.singletonList(application); return Collections.singletonList(application);
} }
return Collections.<ITacticApplication> emptyList(); return Collections.<ITacticApplication> emptyList();
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment