Add solver pre-processing (#374)

For some reason the way we use sat4j seems to be non-optimal, leading to the full 5 seconds of optimising being used. (Removing this limit in the blanketcon pack leads to Sat4j churning for at least 20 mins to "prove" that it's found the most optimal result, with this PR Sat4j only takes ~60ms to solve the [remaining rules and options](https://gist.github.com/AlexIIL/86ba6059b4c6fbbd2b7a151667bf2608)).

This means we can be more confident that we get a fully optimal solution in more cases. (When this isn't the case you'll see this line in the log: `Aborted mod solving optimisation due to timeout`)

This also means we can use the solver system for more features, and be confident that it still finds the optimal solution quickly.

Breaking changes:

- Plugins can no longer override `LoadOption.equals` and `LoadOption.hashCode`

Misc Changes:

- Sat4jWrapper can now have rules changed at anytime, and correctly reverts back to solve it properly.

Other changes from the src/main/resources/changelog/solver-pre-processor.txt file:

* Added a pre-processor step to mod solving.
    * This greatly reduces the time taken for Sat4j to optimise the final mod set (pick the newest possible versions of every mod)
        * Previously this was capped at 5 seconds.
    * Added a warning when picking between two mods when we don't have any reason to pick one over the other.
        * This can happen when two mods provide each other, or two mods provide the same version of a third mod.
    * Added a system property to disable this "loader.mod_solving.disable_pre_processor"
    * Added a system property to explain what this pre-processor is struggling with (partially simplified mod sets)
        * "loader.mod_solving.print_results" prints unsolved sub-problems, and the final chosen options.
        * This is an alternative to the very verbose "loader.debug.mod_solving" property.
    * Made the log line "Aborted mod solving optimisation due to timeout" always print when it happens.

src/main/java/org/quiltmc/loader/api/plugin/solver/LoadOption.java

@@ -16,6 +16,9 @@
 
 package org.quiltmc.loader.api.plugin.solver;
 
+import java.util.Comparator;
+import java.util.concurrent.atomic.AtomicLong;
+
 import org.quiltmc.loader.api.gui.QuiltLoaderText;
 import org.quiltmc.loader.impl.util.QuiltLoaderInternal;
 import org.quiltmc.loader.impl.util.QuiltLoaderInternalType;
@@ -27,4 +30,58 @@ public abstract class LoadOption {
 
 	/** @return A description of this load option, to be shown in the error gui when this load option is involved in a solver error. */
 	public abstract QuiltLoaderText describe();
+
+	public final LoadOption negate() {
+		if (this instanceof NegatedLoadOption) {
+			return ((NegatedLoadOption) this).not;
+		} else {
+			return new NegatedLoadOption(this);
+		}
+	}
+
+	public static boolean isNegated(LoadOption option) {
+		return option instanceof NegatedLoadOption;
+	}
+
+	// Overridden equals and hashCode to prevent solving from having strange behaviour
+
+	@Override
+	public final boolean equals(Object obj) {
+		if (super.equals(obj)) {
+			return true;
+		}
+		if (!(obj instanceof LoadOption)) {
+			return false;
+		}
+		LoadOption other = (LoadOption) obj;
+		if (isNegated(this) && isNegated(other)) {
+			return negate().equals(other.negate());
+		}
+		return false;
+	}
+
+	@Override
+	public final int hashCode() {
+		if (isNegated(this)) {
+			return ~negate().hashCode();
+		}
+		return super.hashCode();
+	}
+
+	// Internals
+
+	/** A {@link Comparator} for any {@link LoadOption}. This is guaranteed to be stable in a single run of a JVM, not
+	 * otherwise. */
+	public static final Comparator<LoadOption> COMPARATOR = (a, b) -> Long.compare(a.order, b.order);
+
+	private static final AtomicLong orderAssignment = new AtomicLong();
+	private final long order;
+
+	public LoadOption() {
+		order = orderAssignment.incrementAndGet();
+	}
+
+	/* package-private */ LoadOption(LoadOption negated) {
+		this.order = -negated.order;
+	}
 }

src/main/java/org/quiltmc/loader/impl/solver/NegatedLoadOption.java → src/main/java/org/quiltmc/loader/api/plugin/solver/NegatedLoadOption.java

@@ -14,21 +14,26 @@
  * limitations under the License.
  */
 
-package org.quiltmc.loader.impl.solver;
+package org.quiltmc.loader.api.plugin.solver;
 
 import org.quiltmc.loader.api.gui.QuiltLoaderText;
-import org.quiltmc.loader.api.plugin.solver.LoadOption;
-import org.quiltmc.loader.api.plugin.solver.Rule;
 import org.quiltmc.loader.impl.util.QuiltLoaderInternal;
 import org.quiltmc.loader.impl.util.QuiltLoaderInternalType;
 
-/** Used for the "inverse load" condition - if this is required by a {@link Rule} then it means the
- * {@link LoadOption} must not be loaded. */
-@QuiltLoaderInternal(QuiltLoaderInternalType.LEGACY_EXPOSED)
-final class NegatedLoadOption extends LoadOption {
-	final LoadOption not;
+/** Used for the "inverse load" condition - if this is required by a {@link Rule} then it means the {@link LoadOption}
+ * must not be loaded.
+ * <p>
+ * Plugins can negate {@link LoadOption}s with {@link LoadOption#negate()}, and test for negation with either
+ * "instanceof NegatedLoadOption" or LoadOption.isNegated */
+@QuiltLoaderInternal(QuiltLoaderInternalType.PLUGIN_API)
+public final class NegatedLoadOption extends LoadOption {
+	public final LoadOption not;
 
-	public NegatedLoadOption(LoadOption not) {
+	/* package-private */ NegatedLoadOption(LoadOption not) {
+		super(not);
+		if (not instanceof NegatedLoadOption) {
+			throw new IllegalArgumentException("Found double-negated negated load option!");
+		}
 		this.not = not;
 	}
 

src/main/java/org/quiltmc/loader/api/plugin/solver/RuleContext.java

@@ -16,7 +16,6 @@
 
 package org.quiltmc.loader.api.plugin.solver;
 
-import org.quiltmc.loader.impl.solver.Sat4jWrapper;
 import org.quiltmc.loader.impl.util.QuiltLoaderInternal;
 import org.quiltmc.loader.impl.util.QuiltLoaderInternalType;
 
@@ -43,14 +42,18 @@ public interface RuleContext {
 	 * {@link LoadOption} currently held, and calls {@link Rule#define(RuleDefiner)} once afterwards. */
 	void addRule(Rule rule);
 
-	/** Clears any current definitions this rule is associated with, and calls {@link Rule#define(RuleDefiner)} */
+	/** Clears any current definitions this rule is associated with, and calls {@link Rule#define(RuleDefiner)} sometime before solving. */
 	void redefine(Rule rule);
 
+	/** @deprecated Replaced by {@link LoadOption#isNegated(LoadOption)} */
+	@Deprecated
 	public static boolean isNegated(LoadOption option) {
-		return Sat4jWrapper.isNegated(option);
+		return LoadOption.isNegated(option);
 	}
 
+	/** @deprecated Replaced by {@link LoadOption#negate()} */
+	@Deprecated
 	public static LoadOption negate(LoadOption option) {
-		return Sat4jWrapper.negate(option);
+		return option.negate();
 	}
 }

src/main/java/org/quiltmc/loader/impl/plugin/QuiltPluginManagerImpl.java

@@ -1313,7 +1313,7 @@ private ModSolveResultImpl runSingleCycle() throws ModResolutionException, Timeo
 
 	}
 
-	private void handleSolverFailure() throws TimeoutException {
+	private void handleSolverFailure() throws TimeoutException, ModSolvingError {
 
 		SolverErrorHelper helper = new SolverErrorHelper(this);
 		boolean failed = false;
@@ -1505,7 +1505,7 @@ private boolean processTentatives(ModSolveResult partialResult) {
 	}
 
 	ModSolveResultImpl getPartialSolution() throws ModSolvingError, TimeoutException {
-		List<LoadOption> solution = solver.getSolution();
+		Collection<LoadOption> solution = solver.getSolution();
 
 		Map<String, ModLoadOption> directModsMap = new HashMap<>();
 		Map<String, ModLoadOption> providedModsMap = new HashMap<>();
@@ -1515,8 +1515,8 @@ ModSolveResultImpl getPartialSolution() throws ModSolvingError, TimeoutException
 		for (LoadOption option : solution) {
 
 			boolean load = true;
-			if (Sat4jWrapper.isNegated(option)) {
-				option = Sat4jWrapper.negate(option);
+			if (LoadOption.isNegated(option)) {
+				option = option.negate();
 				load = false;
 			}
 

src/main/java/org/quiltmc/loader/impl/plugin/SolverErrorHelper.java

@@ -156,7 +156,7 @@ static class OptionLink {
 
 		OptionLink(LoadOption option) {
 			this.option = option;
-			if (RuleContext.isNegated(option)) {
+			if (LoadOption.isNegated(option)) {
 				throw new IllegalArgumentException("Call 'OptionLinkBase.get' instead of this!!");
 			}
 		}

src/main/java/org/quiltmc/loader/impl/solver/RuleComputeResult.java

@@ -0,0 +1,71 @@
+/*
+ * Copyright 2023 QuiltMC
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+package org.quiltmc.loader.impl.solver;
+
+import java.util.Map;
+
+import org.quiltmc.loader.api.plugin.solver.LoadOption;
+
+/** Returned by {@link RuleDefinition#computeConstants(Map)}. Valid values:
+ * <ol>
+ * <li>{@link #CONTRADICTION}</li>
+ * <li>{@link #IDENTICAL}</li>
+ * <li>{@link #TRIVIALLY_REMOVED}</li>
+ * <li>{@link Changed}</li>
+ * <li>{@link Removed}</li>
+ * </ol>
+ */
+/* sealed */ interface RuleComputeResult {
+	static final RuleComputeResult CONTRADICTION = SimpleResult.CONTRADICTION;
+	static final RuleComputeResult IDENTICAL = SimpleResult.IDENTICAL;
+	static final RuleComputeResult TRIVIALLY_REMOVED = SimpleResult.TRIVIALLY_REMOVED;
+
+	enum SimpleResult implements RuleComputeResult {
+		CONTRADICTION,
+		IDENTICAL,
+		TRIVIALLY_REMOVED;
+	}
+
+	static abstract /* sealed */ class DeclaredConstants implements RuleComputeResult {
+		final Map<LoadOption, Boolean> newConstants;
+
+		private DeclaredConstants(Map<LoadOption, Boolean> newConstants) {
+			this.newConstants = newConstants;
+		}
+	}
+
+	/** Indicates that the rule definition fully inlined to constants, and doesn't need to be present in solving any
+	 * more. */
+	static final class Removed extends DeclaredConstants {
+
+		Removed(Map<LoadOption, Boolean> newConstants) {
+			super(newConstants);
+		}
+	}
+
+	/** Indicates that the rule definition partially inlined to constants, and a different rule should now be used
+	 * instead. */
+	static final class Changed extends DeclaredConstants {
+		final RuleDefinition newDefintion;
+
+		Changed(RuleDefinition newDefintion, Map<LoadOption, Boolean> newConstants) {
+			super(newConstants);
+			this.newDefintion = newDefintion;
+		}
+	}
+
+}