Merged KeyUpdate branch.

de.tu-bs.cs.isf.cbc.mutation/META-INF/MANIFEST.MF

@@ -6,10 +6,10 @@ Bundle-Version: 1.0.0.qualifier
 Automatic-Module-Name: de.tu.bs.cs.isf.cbc.mutation
 Bundle-RequiredExecutionEnvironment: JavaSE-16
 Require-Bundle: org.junit,
+ org.apache.commons.commons-io;bundle-version="2.13.0",
  org.eclipse.graphiti.ui;bundle-version="0.18.0",
- org.eclipse.ui.views.properties.tabbed,
- org.eclipse.graphiti;bundle-version="0.18.0",
- org.apache.commons.commons-io
+ org.eclipse.ui.views.properties.tabbed;bundle-version="3.10.100",
+ org.eclipse.graphiti;bundle-version="0.18.0"
 Import-Package: de.tu_bs.cs.isf.cbc.cbcclass,
  de.tu_bs.cs.isf.cbc.cbcmodel,
  de.tu_bs.cs.isf.cbc.exceptions,

de.tu-bs.cs.isf.cbc.util/.classpath

@@ -15,5 +15,6 @@
 	<classpathentry kind="lib" path="lib/junit-platform-commons-1.9.1.jar"/>
 	<classpathentry kind="lib" path="lib/mockito-core-4.8.1.jar"/>
 	<classpathentry kind="lib" path="lib/mockito-inline-4.8.1.jar"/>
+	<classpathentry exported="true" kind="lib" path="lib/key-2.13.0-exe.jar"/>
 	<classpathentry kind="output" path="bin"/>
 </classpath>

de.tu-bs.cs.isf.cbc.util/META-INF/MANIFEST.MF

@@ -4,16 +4,13 @@ Bundle-Name: Parser
 Bundle-SymbolicName: de.tu-bs.cs.isf.cbc.util
 Bundle-Version: 1.0.0.qualifier
 Bundle-RequiredExecutionEnvironment: JavaSE-16
-Require-Bundle: org.key_project.core,
- org.key_project.util,
- org.eclipse.core.resources,
+Require-Bundle: org.eclipse.core.resources,
  org.eclipse.core.runtime,
  org.eclipse.graphiti.mm,
  org.eclipse.core.filesystem,
  org.eclipse.ui,
  org.eclipse.ui.console,
  org.emftext.language.java,
- org.key_project.ui,
  com.google.guava,
  org.mockito.mockito-core;bundle-version="4.8.1";resolution:=optional,
  org.junit;bundle-version="4.13.2",
@@ -35,4 +32,5 @@ Import-Package: de.tu_bs.cs.isf.corc.predicateWizard,
 Bundle-ClassPath: lib/antlr-3.4.jar,
  lib/de.ovgu.featureide.lib.fm-v3.6.2.jar,
  lib/org.sat4j.core.jar,
+ lib/key-2.13.0-exe.jar,
  .

de.tu-bs.cs.isf.cbc.util/build.properties

@@ -4,4 +4,5 @@ bin.includes = META-INF/,\
                .,\
                lib/antlr-3.4.jar,\
                lib/de.ovgu.featureide.lib.fm-v3.6.2.jar,\
-               lib/org.sat4j.core.jar
+               lib/org.sat4j.core.jar,\
+               lib/key-2.13.0-exe.jar

de.tu-bs.cs.isf.cbc.util/src/de/tu_bs/cs/isf/cbc/util/CounterExampleGenerator.java

@@ -6,22 +6,24 @@
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.pp.LogicPrinter;
 import de.uka.ilkd.key.pp.NotationInfo;
-
 import java.util.ArrayList;
 import java.util.HashMap;
 import java.util.Iterator;
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
 
 import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.pp.ProgramPrinter;
 import de.uka.ilkd.key.smt.SMTProblem;
+import de.uka.ilkd.key.smt.SMTSolver;
 import de.uka.ilkd.key.smt.SMTSolverResult;
 import de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth;
 import de.uka.ilkd.key.smt.SolverLauncher;
-import de.uka.ilkd.key.smt.SolverType;
+import de.uka.ilkd.key.smt.solvertypes.SolverType;
+import de.uka.ilkd.key.smt.solvertypes.SolverTypeImplementation;
+import de.uka.ilkd.key.smt.solvertypes.SolverTypes;
+import de.uka.ilkd.key.settings.DefaultSMTSettings;
+import de.uka.ilkd.key.settings.ProofIndependentSMTSettings;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
-import de.uka.ilkd.key.settings.SMTSettings;
 import de.tu_bs.cs.isf.cbc.cbcmodel.Condition;
 import de.tu_bs.cs.isf.cbc.cbcmodel.Variant;
 import de.tu_bs.cs.isf.cbc.exceptions.SettingsException;
@@ -163,7 +165,7 @@ private static HashMap<String, CEType> getConditionMapping() {
 	}
 
 	private static String prettify(Term t)  {
-		LogicPrinter logicPrinter = new LogicPrinter(new ProgramPrinter(), new NotationInfo(), serv);
+		LogicPrinter logicPrinter = LogicPrinter.purePrinter(new NotationInfo(), serv);
 		try {
 			logicPrinter.printTerm(t);
 			String result = logicPrinter.result().toString();
@@ -294,10 +296,10 @@ public static void calculateExample(Proof proof) throws SettingsException {
 
 		for (int i = 0; i < list.size(); i++) {
 			var path = list.get(i);
-			problem = new SMTProblem(proof.getGoal(path.current));
+			problem = new SMTProblem(proof.getOpenGoal(path.current));
 			SMTSolverResult result = runZ3(problem, proof);
 			if (result.isValid() == ThreeValuedTruth.FALSIFIABLE) {
-				String counterexample = problem.getSolvers().iterator().next().getSolverOutput();
+				String counterexample = problem.getSolvers().iterator().next().getRawSolverOutput();
 				SolverOutputCleaner cleaner = new SolverOutputCleaner();
 				cleaner.clean(counterexample);
 				Console.print(cleaner.cleaned(), Colors.BLUE);
@@ -315,10 +317,13 @@ public static void calculateExample(Proof proof) throws SettingsException {
 	}
 
 	private static SMTSolverResult runZ3(SMTProblem problem, Proof proof) {
-			SMTSettings settings = new SMTSettings(proof.getSettings().getSMTSettings(),
-			ProofIndependentSettings.DEFAULT_INSTANCE.getSMTSettings(), proof);
+			ProofIndependentSMTSettings sett = ProofIndependentSettings.DEFAULT_INSTANCE.getSMTSettings();
+			sett.setStoreSMTTranslationToFile(true);
+			DefaultSMTSettings settings = new DefaultSMTSettings(proof.getSettings().getSMTSettings(), sett, proof.getSettings().getNewSMTSettings(), proof);
 			SolverLauncher launcher = new SolverLauncher(settings);
-			launcher.launch(problem, serv, SolverType.Z3_SOLVER); 
+			SolverType z3 = SolverTypes.getSolverTypes().stream().filter(it -> it.getClass().equals(SolverTypeImplementation.class) && it.getName().equals("Z3_CE")).findFirst().orElse(null);
+			launcher.launch(problem, serv, z3); 
+
 			SMTSolverResult result = problem.getFinalResult();
 			return result;
 	}

de.tu-bs.cs.isf.cbc.util/src/de/tu_bs/cs/isf/cbc/util/KeYInteraction.java

@@ -5,9 +5,9 @@
 import java.util.HashMap;
 import java.util.LinkedList;
 import java.util.List;
+import java.util.Map;
 import java.util.Set;
 
-import org.antlr.runtime.RecognitionException;
 import org.eclipse.core.resources.IFile;
 import org.eclipse.core.resources.IWorkspace;
 import org.eclipse.core.resources.ResourcesPlugin;
@@ -28,6 +28,7 @@
 import de.uka.ilkd.key.proof.Statistics;
 import de.uka.ilkd.key.proof.init.ProofInputException;
 import de.uka.ilkd.key.proof.io.ProblemLoaderException;
+import de.uka.ilkd.key.proof.io.ProofSaver;
 import de.uka.ilkd.key.java.ConvertException;
 import de.uka.ilkd.key.java.PosConvertException;
 import de.uka.ilkd.key.settings.ChoiceSettings;
@@ -57,7 +58,7 @@ public static Proof startKeyProof(File location, IProgressMonitor monitor, boole
 			}
 			// Set Taclet options
 			ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings();
-			HashMap<String, String> oldSettings = choiceSettings.getDefaultChoices();
+			Map<String, String> oldSettings = choiceSettings.getDefaultChoices();
 			HashMap<String, String> newSettings = new HashMap<String, String>(oldSettings);
 			newSettings.putAll(MiscTools.getDefaultTacletOptions());
 			newSettings.put("runtimeExceptions", "runtimeExceptions:ban");
@@ -99,7 +100,7 @@ public static Proof startKeyProof(File location, IProgressMonitor monitor, boole
 
 			// Show proof result
 			try {
-				proof.saveToFile(location);
+				ProofSaver.saveToFile(location, proof);
 
 				try {
 					// TODO: inlining may be important too
@@ -213,7 +214,7 @@ public static void startKeYProofFirstContract(File location, int proofCounter) {
 			}
 			// Set Taclet options
 			ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings();
-			HashMap<String, String> oldSettings = choiceSettings.getDefaultChoices();
+			Map<String, String> oldSettings = choiceSettings.getDefaultChoices();
 			HashMap<String, String> newSettings = new HashMap<String, String>(oldSettings);
 			newSettings.putAll(MiscTools.getDefaultTacletOptions());
 			newSettings.put("runtimeExceptions", "runtimeExceptions:ban");
@@ -271,7 +272,7 @@ public static void startKeYProofFirstContract(File location, int proofCounter) {
 						String locationWithoutFileEnding = location.toString().substring(0,
 								location.toString().indexOf("."));
 						keyFile = new File(locationWithoutFileEnding + ".proof");
-						proof.saveToFile(keyFile);
+						ProofSaver.saveToFile(keyFile, proof);
 						IWorkspace workspace = ResourcesPlugin.getWorkspace();
 						IPath iLocation = Path.fromOSString(keyFile.getAbsolutePath());
 						IFile ifile = workspace.getRoot().getFileForLocation(iLocation);

de.tu-bs.cs.isf.cbc.util/src/de/tu_bs/cs/isf/cbc/util/ProveWithKey.java

@@ -111,7 +111,7 @@ public ProveWithKey(AbstractStatement statement, Diagram diagram, IProgressMonit
 		if (uri.contains(MetaNames.FOLDER_NAME)) {
 			String className = uri.substring(0, uri.lastIndexOf("/"));
 			className = className.substring(className.lastIndexOf("/") + 1, className.length());
-			this.sourceFolder = "/" + MetaNames.FOLDER_NAME; /*+ "/" + className;*/
+			this.sourceFolder = MetaNames.FOLDER_NAME; /*+ "/" + className;*/
 		} else {
 			this.sourceFolder = srcFolder;
 		}

de.tu_bs.cs.isf.cbc.statistics/META-INF/MANIFEST.MF

@@ -13,8 +13,7 @@ Require-Bundle: org.eclipse.core.runtime,
  de.tu-bs.cs.isf.cbc.model,
  org.eclipse.core.resources,
  com.google.guava,
- org.eclipse.graphiti,
- org.key_project.core.symbolic_execution
+ org.eclipse.graphiti
 Bundle-ActivationPolicy: lazy
 Export-Package: de.tu_bs.cs.isf.cbc.statistics,
  de.tu_bs.cs.isf.cbc.statistics.impl,