Commit f5b65e0c authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add disprover preference to export PO with selected Hyps

parent a85ff678
......@@ -50,20 +50,23 @@ public class DisproverCommand implements IComposableCommand {
private final Set<Predicate> selectedHypotheses;
private final Predicate goal;
private final int timeout;
private final Boolean exportPO
private static ComposedCommand composed;
public DisproverCommand(Set<Predicate> allHypotheses,
Set<Predicate> selectedHypotheses, Predicate goal, int timeout) {
Set<Predicate> selectedHypotheses, Predicate goal, int timeout,
Boolean exportPO) {
this.allHypotheses = allHypotheses;
this.selectedHypotheses = selectedHypotheses;
this.goal = goal;
this.timeout = timeout;
this.exportPO = exportPO;
}
public static ICounterExample disprove(Animator animator,
IEventBProject project, Set<Predicate> allHypotheses,
Set<Predicate> selectedHypotheses, Predicate goal, int timeout,
Set<Predicate> selectedHypotheses, Predicate goal, int timeoutFactor,
AEventBContextParseUnit context, IProofMonitor pm)
throws InterruptedException {
Preferences prefNode = Platform.getPreferencesService().getRootNode()
......@@ -95,8 +98,9 @@ public class DisproverCommand implements IComposableCommand {
StartAnimationCommand start = new StartAnimationCommand();
DisproverCommand disprove = new DisproverCommand(allHypotheses,
selectedHypotheses, goal, timeout
* prefNode.getInt("timeout", 1000));
selectedHypotheses, goal,
timeoutFactor * prefNode.getInt("timeout", 1000),
prefNode.getBoolean("exportpo", false));
composed = new ComposedCommand(clear, setPrefs, setCLPFD, setCHR,
setSMT, setCSE, setCSEPred, setDoubleEval, load, start,
......@@ -140,8 +144,19 @@ public class DisproverCommand implements IComposableCommand {
}
pto.closeList();
pto.printNumber(timeout);
pto.emptyList(); // do not submit extra options because we set the
// preference above
if (this.exportPO) {
pto.openList();
pto.openTerm("disprover_option");
pto.openTerm("export_po_as_machine");// Note: other valid options : wd_prover_timeout(T), unsat_core,...
pto.printAtom("/tmp/ProB_Rodin_PO_SelectedHyps.mch");
// TO DO: provide user preference path; TO DO: we could runProBClassic(prob_location, tmp);
pto.closeTerm();
pto.closeTerm();
pto.closeList();
} else {
pto.emptyList(); // do not submit extra options because we set the
// preference above; we could transmit additional valid_disprover_option
}
pto.printVariable(RESULT);
pto.closeTerm();
}
......
......@@ -54,6 +54,7 @@ public class DisproverPreferences extends PreferencePage implements
private Button checkCSE;
private Button checkSMT;
private Button checkDoubleEval;
private Button checkExportSelectedHyps;
public DisproverPreferences() {
super();
......@@ -151,15 +152,20 @@ public class DisproverPreferences extends PreferencePage implements
checkCSE.setSelection(prefNode.getBoolean("cse", false));
new Label(pageComponent, SWT.NONE)
.setText("Enable SMT Solver Support in Interpreter:");
.setText("Enable SMT solver support in ProB interpreter:");
checkSMT = new Button(pageComponent, SWT.CHECK);
checkSMT.setSelection(prefNode.getBoolean("smt", false));
new Label(pageComponent, SWT.NONE)
.setText("Check (Hypotheses ^ Goal) in addition to (Hypotheses ^ not Goal) to identify contradiction in hypotheses :");
.setText("Check (Hypotheses ^ Goal) in addition to (Hypotheses ^ not Goal) to identify contradiction in hypotheses:");
checkDoubleEval = new Button(pageComponent, SWT.CHECK);
checkDoubleEval.setSelection(prefNode.getBoolean("doubleeval", false));
new Label(pageComponent, SWT.NONE)
.setText("Export selected hypotheses to B text file (/tmp/ProB_Rodin_PO_SelectedHyps.mch):");
checkExportSelectedHyps = new Button(pageComponent, SWT.CHECK);
checkExportSelectedHyps.setSelection(prefNode.getBoolean("exportpo", false));
return pageComponent;
}
......@@ -171,6 +177,7 @@ public class DisproverPreferences extends PreferencePage implements
prefNode.putBoolean("cse", checkCSE.getSelection());
prefNode.putBoolean("smt", checkSMT.getSelection());
prefNode.putBoolean("doubleeval", checkDoubleEval.getSelection());
prefNode.putBoolean("exportpo", checkExportSelectedHyps.getSelection());
try {
prefNode.flush();
} catch (BackingStoreException e) {
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment