Refactor assert orders

trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/assertorders/AssertOrderInsideLoopFirst1.java

@@ -0,0 +1,50 @@
+/*
+ * Copyright (C) 2014-2015 Betim Musa (musab@informatik.uni-freiburg.de)
+ * Copyright (C) 2024 Frank Schüssele (schuessf@informatik.uni-freiburg.de)
+ * Copyright (C) 2024 University of Freiburg
+ *
+ * This file is part of the ULTIMATE TraceCheckerUtils Library.
+ *
+ * The ULTIMATE TraceCheckerUtils Library is free software: you can redistribute it and/or modify it under the
+ * terms of the GNU Lesser General Public License as published by the Free Software Foundation, either version 3
+ * of the License, or (at your option) any later version.
+ *
+ * The ULTIMATE TraceCheckerUtils Library is distributed in the hope that it will be useful, but WITHOUT ANY
+ * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public License along with the
+ * ULTIMATE TraceCheckerUtils Library. If not, see <http://www.gnu.org/licenses/>.
+ *
+ * Additional permission under GNU GPL version 3 section 7: If you modify the ULTIMATE TraceCheckerUtils Library,
+ * or any covered work, by linking or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
+ * containing parts covered by the terms of the Eclipse Public License, the licensors of the
+ * ULTIMATE TraceCheckerUtils Library grant you additional permission to convey the resulting work.
+ */
+
+package de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.assertorders;
+
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+
+import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IAction;
+import de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.Counterexample;
+
+/**
+ * Assert statements in decremental order by their depth, and check after each step for satisfiability. E.g. first
+ * assert all statements with depth max_depth, then assert all statements of depth max_depth - 1, and so on.
+ *
+ * @author Betim Musa (musab@informatik.uni-freiburg.de)
+ * @author Frank Schüssele (schuessf@informatik.uni-freiburg.de)
+ */
+public class AssertOrderInsideLoopFirst1<L extends IAction> implements IAssertOrder<L> {
+	@Override
+	public List<Set<Integer>> partition(final Counterexample<L> counterexample) {
+		final Map<Integer, Set<Integer>> depth2Statements =
+				AssertOrderUtils.partitionStatementsAccordingDepth(counterexample);
+		// Sort the statements by their depth in descending order (i.e., the most nested statements first).
+		return depth2Statements.keySet().stream().sorted((i1, i2) -> i2.compareTo(i1)).map(depth2Statements::get)
+				.toList();
+	}
+}

trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/assertorders/AssertOrderMixInsideOutside.java

@@ -0,0 +1,64 @@
+/*
+ * Copyright (C) 2014-2015 Betim Musa (musab@informatik.uni-freiburg.de)
+ * Copyright (C) 2024 Frank Schüssele (schuessf@informatik.uni-freiburg.de)
+ * Copyright (C) 2024 University of Freiburg
+ *
+ * This file is part of the ULTIMATE TraceCheckerUtils Library.
+ *
+ * The ULTIMATE TraceCheckerUtils Library is free software: you can redistribute it and/or modify it under the
+ * terms of the GNU Lesser General Public License as published by the Free Software Foundation, either version 3
+ * of the License, or (at your option) any later version.
+ *
+ * The ULTIMATE TraceCheckerUtils Library is distributed in the hope that it will be useful, but WITHOUT ANY
+ * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public License along with the
+ * ULTIMATE TraceCheckerUtils Library. If not, see <http://www.gnu.org/licenses/>.
+ *
+ * Additional permission under GNU GPL version 3 section 7: If you modify the ULTIMATE TraceCheckerUtils Library,
+ * or any covered work, by linking or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
+ * containing parts covered by the terms of the Eclipse Public License, the licensors of the
+ * ULTIMATE TraceCheckerUtils Library grant you additional permission to convey the resulting work.
+ */
+
+package de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.assertorders;
+
+import java.util.ArrayList;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+import java.util.stream.Collectors;
+
+import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IAction;
+import de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.Counterexample;
+
+/**
+ * Assert the statements with the highest depth and lowest depth in alternating order.
+ *
+ * @author Betim Musa (musab@informatik.uni-freiburg.de)
+ * @author Frank Schüssele (schuessf@informatik.uni-freiburg.de)
+ */
+public class AssertOrderMixInsideOutside<L extends IAction> implements IAssertOrder<L> {
+	@Override
+	public List<Set<Integer>> partition(final Counterexample<L> counterexample) {
+		final Map<Integer, Set<Integer>> depth2Statements =
+				AssertOrderUtils.partitionStatementsAccordingDepth(counterexample);
+		final LinkedList<Integer> depthAsQueue =
+				depth2Statements.keySet().stream().sorted().collect(Collectors.toCollection(LinkedList::new));
+		final List<Set<Integer>> result = new ArrayList<>(depth2Statements.size());
+		boolean removeFirst = true;
+		while (!depthAsQueue.isEmpty()) {
+			final int currentDepth;
+			if (removeFirst) {
+				currentDepth = depthAsQueue.removeFirst();
+			} else {
+				currentDepth = depthAsQueue.removeLast();
+			}
+			removeFirst = !removeFirst;
+			result.add(depth2Statements.get(currentDepth));
+		}
+		return result;
+	}
+}

trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/assertorders/AssertOrderNotIncrementally.java

@@ -0,0 +1,48 @@
+/*
+ * Copyright (C) 2014-2015 Betim Musa (musab@informatik.uni-freiburg.de)
+ * Copyright (C) 2024 Frank Schüssele (schuessf@informatik.uni-freiburg.de)
+ * Copyright (C) 2024 University of Freiburg
+ *
+ * This file is part of the ULTIMATE TraceCheckerUtils Library.
+ *
+ * The ULTIMATE TraceCheckerUtils Library is free software: you can redistribute it and/or modify it under the
+ * terms of the GNU Lesser General Public License as published by the Free Software Foundation, either version 3
+ * of the License, or (at your option) any later version.
+ *
+ * The ULTIMATE TraceCheckerUtils Library is distributed in the hope that it will be useful, but WITHOUT ANY
+ * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public License along with the
+ * ULTIMATE TraceCheckerUtils Library. If not, see <http://www.gnu.org/licenses/>.
+ *
+ * Additional permission under GNU GPL version 3 section 7: If you modify the ULTIMATE TraceCheckerUtils Library,
+ * or any covered work, by linking or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
+ * containing parts covered by the terms of the Eclipse Public License, the licensors of the
+ * ULTIMATE TraceCheckerUtils Library grant you additional permission to convey the resulting work.
+ */
+
+package de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.assertorders;
+
+import java.util.List;
+import java.util.Set;
+import java.util.stream.Collectors;
+import java.util.stream.IntStream;
+
+import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IAction;
+import de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.Counterexample;
+
+/**
+ * Partitions the trace into a single partition.
+ *
+ * @author Betim Musa (musab@informatik.uni-freiburg.de)
+ * @author Frank Schüssele (schuessf@informatik.uni-freiburg.de)
+ */
+public class AssertOrderNotIncrementally<L extends IAction> implements IAssertOrder<L> {
+	@Override
+	public List<Set<Integer>> partition(final Counterexample<L> counterexample) {
+		final Set<Integer> partition =
+				IntStream.range(0, counterexample.getWord().length()).boxed().collect(Collectors.toSet());
+		return List.of(partition);
+	}
+}

trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/assertorders/AssertOrderOutsideLoopFirst1.java

@@ -0,0 +1,58 @@
+/*
+ * Copyright (C) 2014-2015 Betim Musa (musab@informatik.uni-freiburg.de)
+ * Copyright (C) 2024 Frank Schüssele (schuessf@informatik.uni-freiburg.de)
+ * Copyright (C) 2024 University of Freiburg
+ *
+ * This file is part of the ULTIMATE TraceCheckerUtils Library.
+ *
+ * The ULTIMATE TraceCheckerUtils Library is free software: you can redistribute it and/or modify it under the
+ * terms of the GNU Lesser General Public License as published by the Free Software Foundation, either version 3
+ * of the License, or (at your option) any later version.
+ *
+ * The ULTIMATE TraceCheckerUtils Library is distributed in the hope that it will be useful, but WITHOUT ANY
+ * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public License along with the
+ * ULTIMATE TraceCheckerUtils Library. If not, see <http://www.gnu.org/licenses/>.
+ *
+ * Additional permission under GNU GPL version 3 section 7: If you modify the ULTIMATE TraceCheckerUtils Library,
+ * or any covered work, by linking or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
+ * containing parts covered by the terms of the Eclipse Public License, the licensors of the
+ * ULTIMATE TraceCheckerUtils Library grant you additional permission to convey the resulting work.
+ */
+
+package de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.assertorders;
+
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+
+import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IAction;
+import de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.Counterexample;
+
+/**
+ * First, assert all statements which don't occur inside of a loop. Then, check for satisfiability. If the result of the
+ * satisfiability check is not unsatisfiable, then assert the rest of the statements, and return the result of the
+ * unsatisfiability check.
+ *
+ * @author Betim Musa (musab@informatik.uni-freiburg.de)
+ * @author Frank Schüssele (schuessf@informatik.uni-freiburg.de)
+ */
+public class AssertOrderOutsideLoopFirst1<L extends IAction> implements IAssertOrder<L> {
+	@Override
+	public List<Set<Integer>> partition(final Counterexample<L> counterexample) {
+		final Map<Integer, Set<Integer>> depth2Statements =
+				AssertOrderUtils.partitionStatementsAccordingDepth(counterexample);
+		// Statements outside of a loop have depth 0.
+		// First, annotate and assert the statements, which doesn't occur within a loop
+		final Set<Integer> stmtsOutsideOfLoop = depth2Statements.get(0);
+		if (stmtsOutsideOfLoop.size() == counterexample.getWord().length()) {
+			return List.of(stmtsOutsideOfLoop);
+		}
+		// Then assert the other statements.
+		final Set<Integer> stmtsWithinLoop =
+				AssertOrderUtils.getTraceDifference(counterexample.getWord(), stmtsOutsideOfLoop);
+		return List.of(stmtsOutsideOfLoop, stmtsWithinLoop);
+	}
+}

trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/assertorders/AssertOrderOutsideLoopFirst2.java

@@ -0,0 +1,49 @@
+/*
+ * Copyright (C) 2014-2015 Betim Musa (musab@informatik.uni-freiburg.de)
+ * Copyright (C) 2024 Frank Schüssele (schuessf@informatik.uni-freiburg.de)
+ * Copyright (C) 2024 University of Freiburg
+ *
+ * This file is part of the ULTIMATE TraceCheckerUtils Library.
+ *
+ * The ULTIMATE TraceCheckerUtils Library is free software: you can redistribute it and/or modify it under the
+ * terms of the GNU Lesser General Public License as published by the Free Software Foundation, either version 3
+ * of the License, or (at your option) any later version.
+ *
+ * The ULTIMATE TraceCheckerUtils Library is distributed in the hope that it will be useful, but WITHOUT ANY
+ * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public License along with the
+ * ULTIMATE TraceCheckerUtils Library. If not, see <http://www.gnu.org/licenses/>.
+ *
+ * Additional permission under GNU GPL version 3 section 7: If you modify the ULTIMATE TraceCheckerUtils Library,
+ * or any covered work, by linking or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
+ * containing parts covered by the terms of the Eclipse Public License, the licensors of the
+ * ULTIMATE TraceCheckerUtils Library grant you additional permission to convey the resulting work.
+ */
+
+package de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.assertorders;
+
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+
+import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IAction;
+import de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.Counterexample;
+
+/**
+ * Assert statements in incremental order by their depth, and check after each step for satisfiability. E.g. first
+ * assert all statements with depth 0, then assert all statements at depth 1, and so on.
+ *
+ * @author Betim Musa (musab@informatik.uni-freiburg.de)
+ * @author Frank Schüssele (schuessf@informatik.uni-freiburg.de)
+ */
+public class AssertOrderOutsideLoopFirst2<L extends IAction> implements IAssertOrder<L> {
+	@Override
+	public List<Set<Integer>> partition(final Counterexample<L> counterexample) {
+		final Map<Integer, Set<Integer>> depth2Statements =
+				AssertOrderUtils.partitionStatementsAccordingDepth(counterexample);
+		// Sort the statements by their depth in ascending order (i.e., the less nested statements first).
+		return depth2Statements.keySet().stream().sorted().map(depth2Statements::get).toList();
+	}
+}

trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/assertorders/AssertOrderSmallConstantsFirst.java

@@ -0,0 +1,106 @@
+/*
+ * Copyright (C) 2014-2015 Betim Musa (musab@informatik.uni-freiburg.de)
+ * Copyright (C) 2024 Frank Schüssele (schuessf@informatik.uni-freiburg.de)
+ * Copyright (C) 2024 University of Freiburg
+ *
+ * This file is part of the ULTIMATE TraceCheckerUtils Library.
+ *
+ * The ULTIMATE TraceCheckerUtils Library is free software: you can redistribute it and/or modify it under the
+ * terms of the GNU Lesser General Public License as published by the Free Software Foundation, either version 3
+ * of the License, or (at your option) any later version.
+ *
+ * The ULTIMATE TraceCheckerUtils Library is distributed in the hope that it will be useful, but WITHOUT ANY
+ * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public License along with the
+ * ULTIMATE TraceCheckerUtils Library. If not, see <http://www.gnu.org/licenses/>.
+ *
+ * Additional permission under GNU GPL version 3 section 7: If you modify the ULTIMATE TraceCheckerUtils Library,
+ * or any covered work, by linking or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
+ * containing parts covered by the terms of the Eclipse Public License, the licensors of the
+ * ULTIMATE TraceCheckerUtils Library grant you additional permission to convey the resulting work.
+ */
+
+package de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.assertorders;
+
+import java.math.BigDecimal;
+import java.math.BigInteger;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
+
+import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWord;
+import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IAction;
+import de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.Counterexample;
+import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm;
+import de.uni_freiburg.informatik.ultimate.logic.ConstantTerm;
+import de.uni_freiburg.informatik.ultimate.logic.Rational;
+import de.uni_freiburg.informatik.ultimate.logic.Term;
+
+/**
+ * Assert statements that with small constants first. Then, check for satisfiability. If the result of the
+ * satisfiability check is not unsatisfiable, then assert the rest of the statements, and return the result of the
+ * unsatisfiability check.
+ *
+ * @author Betim Musa (musab@informatik.uni-freiburg.de)
+ * @author Frank Schüssele (schuessf@informatik.uni-freiburg.de)
+ */
+public class AssertOrderSmallConstantsFirst<L extends IAction> implements IAssertOrder<L> {
+	private static final int CONSTANT_SIZE = 10;
+
+	/**
+	 * Determines whether the given term 't' contains a constant (a (real/natural) number) that is greater than the
+	 * given size 'constantSize'.
+	 */
+	private static boolean termHasConstantGreaterThan(final Term t, final int constantSize) {
+		if (t instanceof ApplicationTerm) {
+			final Term[] args = ((ApplicationTerm) t).getParameters();
+			for (final Term arg : args) {
+				if (termHasConstantGreaterThan(arg, constantSize)) {
+					return true;
+				}
+			}
+		} else if (t instanceof ConstantTerm) {
+			final Object val = ((ConstantTerm) t).getValue();
+			if (val instanceof BigInteger) {
+				return ((BigInteger) val).compareTo(BigInteger.valueOf(constantSize)) > 0;
+			} else if (val instanceof BigDecimal) {
+				return ((BigDecimal) val).compareTo(BigDecimal.valueOf(constantSize)) > 0;
+			} else if (val instanceof Rational) {
+				return ((Rational) val).compareTo(Rational.valueOf(constantSize, 1)) > 0;
+			} else {
+				throw new UnsupportedOperationException(
+						"ConstantTerm is neither BigInter nor BigDecimal, therefore comparison is not possible!");
+			}
+
+		}
+		return false;
+	}
+
+	/**
+	 * Partition the statements of the given trace into two sets. The first set consists of the statements, which
+	 * contain only constants smaller than or equal to 'constantSize'. The second set contains the statements, which
+	 * contain only constants greater than 'constantSize'.
+	 */
+	private Set<Integer> partitionStmtsAccordingToConstantSize(final NestedWord<L> trace, final int constantSize) {
+		final Set<Integer> result = new HashSet<>();
+
+		for (int i = 0; i < trace.length(); i++) {
+			final Term t = trace.getSymbol(i).getTransformula().getFormula();
+			if (!termHasConstantGreaterThan(t, constantSize)) {
+				result.add(i);
+			}
+		}
+		return result;
+	}
+
+	@Override
+	public List<Set<Integer>> partition(final Counterexample<L> counterexample) {
+		final NestedWord<L> trace = counterexample.getWord();
+		// Choose statements that contains only constants <= constantSize and assert them
+		final Set<Integer> stmtsWithSmallConstant = partitionStmtsAccordingToConstantSize(trace, CONSTANT_SIZE);
+		// Then assert the rest of statements
+		return List.of(stmtsWithSmallConstant, AssertOrderUtils.getTraceDifference(trace, stmtsWithSmallConstant));
+	}
+}