Merge branch 'develop' into rodin3

de.prob.core/src/de/prob/eventb/translator/internal/TranslationVisitor.java

@@ -616,10 +616,8 @@ public class TranslationVisitor implements ISimpleVisitor {
 			// I've encountered null types. Maybe that was a bug but just to be
 			// sure (in most cases, missing type information won't hurt):
 			if (type != null) {
-				// put a translation of the identifier on the stack ...
-				decl.accept(this);
-				// ... and take it
-				final PExpression expr = expressions.pop();
+				final PExpression expr = createIdentifierExpression(decl
+						.getName());
 				// construct "expr:type"
 				final PPredicate member = new AMemberPredicate(expr,
 						translateType(type));

de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverCommand.java

@@ -2,10 +2,13 @@ package de.prob.eventb.disprover.core.internal;
 
 import java.util.Set;
 
+import org.eclipse.core.runtime.Platform;
 import org.eclipse.core.runtime.jobs.Job;
+import org.eclipse.core.runtime.preferences.InstanceScope;
 import org.eventb.core.IEventBProject;
 import org.eventb.core.ast.Predicate;
 import org.eventb.core.seqprover.IProofMonitor;
+import org.osgi.service.prefs.Preferences;
 
 import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
 import de.be4.classicalb.core.parser.node.AEventBContextParseUnit;
@@ -39,36 +42,47 @@ public class DisproverCommand implements IComposableCommand {
 	private final Set<Predicate> allHypotheses;
 	private final Set<Predicate> selectedHypotheses;
 	private final Predicate goal;
-	private final int timeoutFactor;
+	private final int timeout;
 
 	private static ComposedCommand composed;
 
 	public DisproverCommand(Set<Predicate> allHypotheses,
-			Set<Predicate> selectedHypotheses, Predicate goal, int timeoutFactor) {
+			Set<Predicate> selectedHypotheses, Predicate goal, int timeout) {
 		this.allHypotheses = allHypotheses;
 		this.selectedHypotheses = selectedHypotheses;
 		this.goal = goal;
-		this.timeoutFactor = timeoutFactor;
+		this.timeout = timeout;
 	}
 
 	public static ICounterExample disprove(Animator animator,
 			IEventBProject project, Set<Predicate> allHypotheses,
-			Set<Predicate> selectedHypotheses, Predicate goal,
-			int timeoutFactor, AEventBContextParseUnit context, IProofMonitor pm)
+			Set<Predicate> selectedHypotheses, Predicate goal, int timeout,
+			AEventBContextParseUnit context, IProofMonitor pm)
 			throws ProBException, InterruptedException {
+		Preferences prefNode = Platform.getPreferencesService().getRootNode()
+				.node(InstanceScope.SCOPE).node("prob_disprover_preferences");
 
 		final ClearMachineCommand clear = new ClearMachineCommand();
+
 		final SetPreferencesCommand setPrefs = SetPreferencesCommand
 				.createSetPreferencesCommand(animator);
 
+		// set clpfd and chr preference
+		final SetPreferenceCommand setCLPFD = new SetPreferenceCommand("CLPFD",
+				Boolean.toString(prefNode.getBoolean("clpfd", true)));
+		final SetPreferenceCommand setCHR = new SetPreferenceCommand("CHR",
+				Boolean.toString(prefNode.getBoolean("clpfd", true)));
+
 		DisproverLoadCommand load = new DisproverLoadCommand(project, context);
 
 		StartAnimationCommand start = new StartAnimationCommand();
 
 		DisproverCommand disprove = new DisproverCommand(allHypotheses,
-				selectedHypotheses, goal, timeoutFactor);
+				selectedHypotheses, goal, timeout
+						* prefNode.getInt("timeout", 1000));
 
-		composed = new ComposedCommand(clear, setPrefs, load, start, disprove);
+		composed = new ComposedCommand(clear, setPrefs, setCLPFD, setCHR, load,
+				start, disprove);
 
 		final Job job = new ProBCommandJob("Disproving", animator, composed);
 		job.setUser(true);
@@ -107,7 +121,7 @@ public class DisproverCommand implements IComposableCommand {
 			translatePredicate(pto, p);
 		}
 		pto.closeList();
-		pto.printNumber(timeoutFactor);
+		pto.printNumber(timeout);
 		pto.printVariable(RESULT);
 		pto.closeTerm();
 	}

de.prob.eventb.disprover.ui/plugin.xml

@@ -64,42 +64,13 @@
             tooltip="%tactic.disprover.tooltip-relevant" /> -->
    </extension>
    <extension
-         point="org.eclipse.ui.commands">
-      <command
-            id="de.prob.eventb.disprover.exportastest"
-            name="Export as ProB Disprover Testcase">
-      </command>
-   </extension>
-   <extension
-         point="org.eclipse.ui.handlers">
-      <handler
-            commandId="de.prob.eventb.disprover.exportastest">
-         <class
-               class="de.prob.eventb.disprover.ui.export.ExportAsTestHandler">
-         </class>
-      </handler>
-   </extension>
-   <extension
-         point="org.eclipse.ui.menus">
-      <menuContribution
-            locationURI="popup:fr.systerel.explorer.navigator.view">
-         <command
-               commandId="de.prob.eventb.disprover.exportastest"
-               label="Export as ProB Disprover Testcase"
-               style="push">
-            <visibleWhen>
-               <with
-                     variable="selection">
-                  <iterate
-                        operator="or">
-                     <instanceof
-                           value="org.eventb.core.IPSStatus">
-                     </instanceof>
-                  </iterate>
-               </with>
-            </visibleWhen>
-         </command>
-      </menuContribution>
+         point="org.eclipse.ui.preferencePages">
+      <page
+            category="probpreferences"
+            class="de.prob.eventb.disprover.ui.DisproverPreferences"
+            id="de.prob.ui.probclassic"
+            name="ProB (Dis-)Prover">
+      </page>
    </extension>
 
 </plugin>

de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/DisproverPreferences.java

+package de.prob.eventb.disprover.ui;
+
+import org.eclipse.core.runtime.Platform;
+import org.eclipse.core.runtime.preferences.InstanceScope;
+import org.eclipse.jface.preference.PreferencePage;
+import org.eclipse.jface.resource.ImageDescriptor;
+import org.eclipse.swt.SWT;
+import org.eclipse.swt.events.*;
+import org.eclipse.swt.layout.*;
+import org.eclipse.swt.widgets.*;
+import org.eclipse.ui.*;
+import org.osgi.service.prefs.*;
+
+public class DisproverPreferences extends PreferencePage implements
+		IWorkbenchPreferencePage {
+
+	public static final class PushButton extends SelectionAdapter {
+
+		private final Text text;
+		private final Shell shell;
+
+		public PushButton(final Shell shell, final Text text) {
+			this.shell = shell;
+			this.text = text;
+		}
+
+		@Override
+		public void widgetSelected(final SelectionEvent e) {
+			super.widgetSelected(e);
+			FileDialog dialog = new FileDialog(shell, SWT.OPEN);
+			String open = dialog.open();
+			text.setText(open);
+		}
+
+	}
+
+	private Preferences prefNode;
+	private Text timeoutTextField;
+	private Button checkCLPFD;
+	private Button checkCHR;
+
+	public DisproverPreferences() {
+		super();
+	}
+
+	public DisproverPreferences(final String title) {
+		super(title);
+	}
+
+	public DisproverPreferences(final String title, final ImageDescriptor image) {
+		super(title, image);
+	}
+
+	@Override
+	protected Control createContents(final Composite parent) {
+		Composite pageComponent = new Composite(parent, SWT.NULL);
+
+		GridLayout layout = new GridLayout();
+		layout.numColumns = 2;
+		layout.marginHeight = 0;
+		layout.marginWidth = 0;
+
+		pageComponent.setLayout(layout);
+
+		new Label(pageComponent, SWT.NONE).setText("Time-out:");
+		timeoutTextField = new Text(pageComponent, SWT.NONE);
+		int timeout = prefNode.getInt("timeout", 1000);
+		timeoutTextField.setText(Integer.toString(timeout));
+		timeoutTextField.addVerifyListener(new VerifyListener() {
+			@Override
+			public void verifyText(VerifyEvent e) {
+				if (e.text.length() >= 1) {
+					e.doit = true;
+					for (int i = 0; i < e.text.length(); i++) {
+						if (!Character.isDigit(e.text.charAt(i))) {
+							e.doit = false;
+						}
+					}
+				}
+			}
+		});
+
+		Label timeoutRemark = new Label(pageComponent, SWT.WRAP);
+		timeoutRemark
+				.setText("Note: The time-out is applied to each constraint-solving action.\nThe maximum time-out is thus twice as long (solving with all hypotheses and with the selected hypotheses only).");
+		GridData gridData2 = new GridData();
+		gridData2.horizontalSpan = 2;
+		timeoutRemark.setLayoutData(gridData2);
+
+		new Label(pageComponent, SWT.NONE).setText("Use CLP(FD) Solver:");
+		checkCLPFD = new Button(pageComponent, SWT.CHECK);
+		checkCLPFD.setSelection(prefNode.getBoolean("clpfd", true));
+		checkCLPFD.addSelectionListener(new SelectionListener() {
+			@Override
+			public void widgetSelected(SelectionEvent e) {
+				if (!checkCLPFD.getSelection()) {
+					checkCHR.setSelection(false);
+				}
+			}
+
+			@Override
+			public void widgetDefaultSelected(SelectionEvent e) {
+				// TODO Auto-generated method stub
+
+			}
+		});
+
+		new Label(pageComponent, SWT.NONE).setText("Use CHR Solver:");
+		checkCHR = new Button(pageComponent, SWT.CHECK);
+		checkCHR.setSelection(prefNode.getBoolean("chr", true));
+		checkCHR.addSelectionListener(new SelectionListener() {
+			@Override
+			public void widgetSelected(SelectionEvent e) {
+				if (checkCHR.getSelection()) {
+					checkCLPFD.setSelection(true);
+				}
+			}
+
+			@Override
+			public void widgetDefaultSelected(SelectionEvent e) {
+				// TODO Auto-generated method stub
+
+			}
+		});
+
+		Label chrRemark = new Label(pageComponent, SWT.WRAP);
+		chrRemark
+				.setText("Note: The CHR Solver can only be used in conjunction with the CLP(FD) solver.");
+
+		return pageComponent;
+	}
+
+	@Override
+	public boolean performOk() {
+		prefNode.put("timeout", timeoutTextField.getText());
+		prefNode.putBoolean("clpfd", checkCLPFD.getSelection());
+		prefNode.putBoolean("chr", checkCHR.getSelection());
+		try {
+			prefNode.flush();
+		} catch (BackingStoreException e) {
+			e.printStackTrace();
+		}
+		return super.performOk();
+	}
+
+	@Override
+	public void init(final IWorkbench workbench) {
+		prefNode = Platform.getPreferencesService().getRootNode()
+				.node(InstanceScope.SCOPE).node("prob_disprover_preferences");
+	}
+
+}

de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/export/ExportAsTestHandler.java

-package de.prob.eventb.disprover.ui.export;
-
-import java.io.*;
-
-import org.eclipse.core.commands.*;
-import org.eclipse.core.runtime.Platform;
-import org.eclipse.core.runtime.preferences.InstanceScope;
-import org.eclipse.jface.dialogs.MessageDialog;
-import org.eclipse.jface.viewers.*;
-import org.eclipse.swt.SWT;
-import org.eclipse.swt.widgets.*;
-import org.eclipse.ui.handlers.HandlerUtil;
-import org.eventb.core.*;
-import org.eventb.core.ast.Predicate;
-import org.eventb.core.pm.*;
-import org.eventb.core.seqprover.*;
-import org.osgi.service.prefs.*;
-import org.rodinp.core.*;
-
-import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
-import de.be4.classicalb.core.parser.node.AEventBContextParseUnit;
-import de.prob.eventb.disprover.core.translation.DisproverContextCreator;
-import de.prob.eventb.translator.internal.TranslationVisitor;
-import de.prob.logging.Logger;
-import de.prob.prolog.output.*;
-
-public class ExportAsTestHandler extends AbstractHandler implements IHandler {
-	@Override
-	public Object execute(final ExecutionEvent event) throws ExecutionException {
-		try {
-			final IPOSequent poSequent = getSelectedSequent(event);
-			final IProverSequent sequent = toProverSequent(poSequent);
-
-			if (sequent != null) {
-				final Preferences prefs = Platform.getPreferencesService()
-						.getRootNode().node(InstanceScope.SCOPE)
-						.node("prob_export_preferences");
-				final Shell shell = HandlerUtil.getActiveShell(event);
-				final String fileName = askForExportFile(prefs, shell, sequent);
-				if (fileName != null) {
-					StringBuffer sb;
-
-					sb = toDisproverMachine(sequent);
-					appendDisproverTestCase(sb, sequent, poSequent);
-					dumpStringBufferToFile(sb, fileName);
-				}
-			}
-		} catch (RodinDBException e) {
-			throw new ExecutionException(e.getMessage());
-		}
-		return null;
-	}
-
-	private void dumpStringBufferToFile(StringBuffer sb, String fileName) {
-		final boolean isSafeToWrite = isSafeToWrite(fileName);
-
-		if (isSafeToWrite) {
-			PrintWriter out = null;
-			try {
-				out = new PrintWriter(new FileWriter(fileName));
-				out.println(sb.toString());
-			} catch (IOException e) {
-				Logger.notifyUser("Unable to append to file '" + fileName + "'");
-			} finally {
-				if (out != null) {
-					out.close();
-				}
-			}
-		}
-
-	}
-
-	public static IProverSequent toProverSequent(IPOSequent sequent)
-			throws RodinDBException {
-		IPORoot poRoot = (IPORoot) sequent.getRoot();
-		IProofManager pm = EventBPlugin.getProofManager();
-		IProofComponent pc = pm.getProofComponent(poRoot);
-		IProofAttempt pa = pc.createProofAttempt(sequent.getElementName(),
-				"Disprover Translation", null);
-		IProofTree proofTree = pa.getProofTree();
-
-		IProverSequent proverSequent = proofTree.getSequent();
-		pa.dispose();
-
-		return proverSequent;
-	}
-
-	private void appendDisproverTestCase(StringBuffer export,
-			IProverSequent sequent, IPOSequent poSequent)
-			throws RodinDBException {
-
-		StringWriter st = new StringWriter();
-		PrintWriter pw = new PrintWriter(st);
-		PrologTermOutput pto = new PrologTermOutput(pw, false);
-
-		pto.openTerm("disprover_test");
-		predicateToProlog(pto, sequent.goal());
-
-		pto.openList();
-		for (Predicate p : sequent.hypIterable()) {
-			predicateToProlog(pto, p);
-		}
-		pto.closeList();
-
-		pto.printAtom("unknown");
-
-		pto.closeTerm();
-
-		if (pw != null) {
-			pw.close();
-		}
-
-		// add new testcase terms to the additional information list
-		int index = export.indexOf("],_Error)).");
-		export.insert(index, "," + st.toString());
-	}
-
-	private void predicateToProlog(IPrologTermOutput pto, Predicate pred) {
-		TranslationVisitor v = new TranslationVisitor();
-		pred.accept(v);
-		ASTProlog p = new ASTProlog(pto, null);
-		v.getPredicate().apply(p);
-	}
-
-	private IPOSequent getSelectedSequent(final ExecutionEvent event) {
-		final ISelection fSelection = HandlerUtil.getCurrentSelection(event);
-		IPSStatus status = null;
-		if (fSelection instanceof IStructuredSelection) {
-			final IStructuredSelection ssel = (IStructuredSelection) fSelection;
-			if (ssel.size() == 1 && ssel.getFirstElement() instanceof IPSStatus) {
-				status = (IPSStatus) ssel.getFirstElement();
-			}
-		}
-
-		return status.getPOSequent();
-	}
-
-	private String askForExportFile(final Preferences prefs, final Shell shell,
-			final IProverSequent sequent) {
-		final String path = prefs.get("dir", System.getProperty("user.home"));
-
-		final FileDialog dialog = new FileDialog(shell, SWT.SAVE);
-		dialog.setFilterExtensions(new String[] { "*.eventb" });
-
-		dialog.setFilterPath(path);
-		dialog.setFileName("disprover_testcase.eventb");
-		String result = dialog.open();
-		if (result != null) {
-			final String newPath = dialog.getFilterPath();
-			if (!path.equals(newPath)) {
-				prefs.put("dir", newPath);
-				try {
-					prefs.flush();
-				} catch (BackingStoreException e) {
-					// Ignore, if preferences are not stored correctly we simply
-					// ignore it (annoying, but not critical)
-				}
-			}
-			if (!result.endsWith(".eventb")) {
-				result += ".eventb";
-			}
-		}
-		return result;
-	}
-
-	public static StringBuffer toDisproverMachine(final IProverSequent sequent)
-			throws RodinDBException {
-		AEventBContextParseUnit context = DisproverContextCreator
-				.createDisproverContext(sequent);
-
-		StringWriter st = new StringWriter();
-		PrintWriter pw = new PrintWriter(st);
-		PrologTermOutput pto = new PrologTermOutput(pw, false);
-
-		pto.openTerm("package");
-		pto.openTerm("load_event_b_project");
-		pto.emptyList();
-
-		pto.openList();
-		ASTProlog modelAst = new ASTProlog(pto, null);
-		context.apply(modelAst);
-		pto.closeList();
-
-		pto.openList();
-
-		pto.openTerm("exporter_version");
-		pto.printNumber(3);
-		pto.closeTerm();
-
-		// try to export theories if available
-		IPOSequent x = (IPOSequent) sequent.getOrigin();
-		IRodinProject project = x.getSources()[0].getRodinProject();
-
-		pto.closeList();
-
-		pto.printVariable("_Error");
-		pto.closeTerm();
-		pto.closeTerm();
-
-		st.append(".");
-
-		return st.getBuffer();
-	}
-
-	private static boolean isSafeToWrite(final String filename) {
-		if (new File(filename).exists()) {
-			final MessageDialog dialog = new MessageDialog(null, "File exists",
-					null, "The file exists. Do you want to overwrite it?",
-					MessageDialog.QUESTION, new String[] { "Yes", "No" }, 0);
-			return dialog.open() == 0;
-		} else
-			return true;
-	}
-}