diff --git a/.github/workflows/maven-test.yml b/.github/workflows/maven-test.yml index acf9a8fb93..af74ccc25f 100644 --- a/.github/workflows/maven-test.yml +++ b/.github/workflows/maven-test.yml @@ -62,7 +62,7 @@ jobs: strategy: #fail-fast: false matrix: - group: [ "xcsp", "dimacs", "mps" ] + group: [ "xcsp", "dimacs", "mps", "spec" ] # The different steps steps: diff --git a/codegen/pom.xml b/codegen/pom.xml new file mode 100644 index 0000000000..ad35393d92 --- /dev/null +++ b/codegen/pom.xml @@ -0,0 +1,46 @@ + + + + 4.0.0 + + + org.choco-solver + choco + 6.0.2-SNAPSHOT + + + org.choco-solver + choco-codegen + 6.0.2-SNAPSHOT + jar + + choco-codegen + + Annotation processors used to build choco-solver (build-time only). + + + + .${file.separator}.. + + + + + + org.apache.maven.plugins + maven-compiler-plugin + + + none + + + + + diff --git a/codegen/src/main/java/org/chocosolver/codegen/RecordingModelProcessor.java b/codegen/src/main/java/org/chocosolver/codegen/RecordingModelProcessor.java new file mode 100644 index 0000000000..4af811d00e --- /dev/null +++ b/codegen/src/main/java/org/chocosolver/codegen/RecordingModelProcessor.java @@ -0,0 +1,228 @@ +/* + * This file is part of choco-codegen, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.codegen; + +import javax.annotation.processing.AbstractProcessor; +import javax.annotation.processing.RoundEnvironment; +import javax.annotation.processing.SupportedAnnotationTypes; +import javax.lang.model.SourceVersion; +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.AnnotationValue; +import javax.lang.model.element.Element; +import javax.lang.model.element.ElementKind; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.Modifier; +import javax.lang.model.element.PackageElement; +import javax.lang.model.element.TypeElement; +import javax.lang.model.element.VariableElement; +import javax.lang.model.type.DeclaredType; +import javax.lang.model.type.TypeKind; +import javax.lang.model.type.TypeMirror; +import javax.lang.model.util.ElementFilter; +import javax.tools.Diagnostic; +import java.io.IOException; +import java.io.Writer; +import java.util.ArrayList; +import java.util.Comparator; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.stream.Collectors; +import java.util.stream.IntStream; + +/** + * Generates the recording subclass of a class annotated with {@code org.chocosolver.solver.spec.GenerateRecordingModel}. + *

+ * The generated class extends the annotated class and overrides every default method of the factory interface + * (but the excluded ones) as follows: + * 

{@code
+ * public Constraint arithm(IntVar p0, String p1, int p2) {
+ *     if (!topLevel()) {
+ *         return super.arithm(p0, p1, p2);
+ *     }
+ *     return getRecorder().call(M[i], () -> super.arithm(p0, p1, p2), new Object[]{p0, p1, p2});
+ * }
+ * }
+ * The annotated class must provide {@code topLevel()} and {@code getRecorder()}; the recorder must provide + * {@code call(FactoryMethod, Supplier, Object[])} and {@code run(FactoryMethod, Runnable, Object[])}. + * The generated class also declares a public constructor for each non-private constructor of the annotated class. + * + * @author Charles Prud'homme + */ +@SupportedAnnotationTypes(RecordingModelProcessor.ANNOTATION) +public class RecordingModelProcessor extends AbstractProcessor { + + static final String ANNOTATION = "org.chocosolver.solver.spec.GenerateRecordingModel"; + + @Override + public SourceVersion getSupportedSourceVersion() { + return SourceVersion.latestSupported(); + } + + @Override + public boolean process(Set annotations, RoundEnvironment env) { + for (TypeElement annotation : annotations) { + for (Element e : env.getElementsAnnotatedWith(annotation)) { + if (e.getKind() != ElementKind.CLASS) { + error(e, "@GenerateRecordingModel only applies to classes"); + continue; + } + try { + generate((TypeElement) e, attributes(e, annotation)); + } catch (IOException ex) { + error(e, "Cannot generate the recording model: " + ex.getMessage()); + } + } + } + return true; + } + + private void error(Element e, String message) { + processingEnv.getMessager().printMessage(Diagnostic.Kind.ERROR, message, e); + } + + /** + * @return the attributes of the annotation, with default values + */ + private Map attributes(Element e, TypeElement annotation) { + for (AnnotationMirror am : e.getAnnotationMirrors()) { + if (am.getAnnotationType().asElement().equals(annotation)) { + return processingEnv.getElementUtils().getElementValuesWithDefaults(am).entrySet().stream() + .collect(Collectors.toMap(v -> v.getKey().getSimpleName().toString(), v -> v.getValue().getValue())); + } + } + throw new IllegalStateException("annotation not found on " + e); + } + + private void generate(TypeElement annotated, Map attributes) throws IOException { + TypeElement factories = (TypeElement) ((DeclaredType) attributes.get("factories")).asElement(); + String name = (String) attributes.get("name"); + Set excluded = new HashSet<>(); + for (Object v : (List) attributes.get("excluded")) { + excluded.add((String) ((AnnotationValue) v).getValue()); + } + String pkg = ((PackageElement) annotated.getEnclosingElement()).getQualifiedName().toString(); + + List methods = new ArrayList<>(); + for (ExecutableElement m : ElementFilter.methodsIn(processingEnv.getElementUtils().getAllMembers(factories))) { + Set mods = m.getModifiers(); + if (mods.contains(Modifier.DEFAULT) && !mods.contains(Modifier.STATIC) + && !excluded.contains(m.getSimpleName().toString())) { + methods.add(m); + } + } + methods.sort(Comparator.comparing(this::signature)); + + StringBuilder sb = new StringBuilder(); + sb.append("package ").append(pkg).append(";\n\n") + .append("/**\n") + .append(" * Recording subclass of {@link ").append(annotated.getSimpleName()).append("}: overrides the ") + .append(methods.size()).append(" factory methods of\n") + .append(" * {@link ").append(factories.getQualifiedName()).append("} to journalize them.\n") + .append(" *

\n") + .append(" * GENERATED at compile time by {@code ").append(getClass().getName()).append("}.\n") + .append(" */\n") + .append("public class ").append(name).append(" extends ").append(annotated.getSimpleName()).append(" {\n\n") + .append(" /**\n * Names of the factory methods which are not journalized (no effect on the model).\n */\n") + .append(" public static final java.util.Set EXCLUDED = java.util.Set.of(") + .append(excluded.stream().sorted().map(e -> "\"" + e + "\"").collect(Collectors.joining(", "))) + .append(");\n\n") + .append(" private static final FactoryMethod[] M = new FactoryMethod[").append(methods.size()).append("];\n\n") + .append(" static {\n"); + for (int i = 0; i < methods.size(); i++) { + ExecutableElement m = methods.get(i); + sb.append(" M[").append(i).append("] = FactoryMethod.of(\"").append(m.getSimpleName()).append('"'); + for (VariableElement p : m.getParameters()) { + sb.append(", ").append(erasure(p.asType())).append(".class"); + } + sb.append(");\n"); + } + sb.append(" }\n"); + + for (ExecutableElement c : ElementFilter.constructorsIn(annotated.getEnclosedElements())) { + if (c.getModifiers().contains(Modifier.PRIVATE)) { + continue; + } + sb.append("\n public ").append(name).append('(').append(parameters(c)).append(") {\n") + .append(" super(").append(names(c)).append(");\n") + .append(" }\n"); + } + + for (int i = 0; i < methods.size(); i++) { + ExecutableElement m = methods.get(i); + boolean isVoid = m.getReturnType().getKind() == TypeKind.VOID; + String superCall = "super." + m.getSimpleName() + "(" + names(m) + ")"; + String args = "new Object[]{" + names(m) + "}"; + sb.append("\n @Override\n") + .append(" public ").append(typeParameters(m)).append(m.getReturnType()).append(' ') + .append(m.getSimpleName()) + .append('(').append(parameters(m)).append(") {\n") + .append(" if (!topLevel()) {\n"); + if (isVoid) { + sb.append(" ").append(superCall).append(";\n") + .append(" return;\n") + .append(" }\n") + .append(" getRecorder().run(M[").append(i).append("], () -> ").append(superCall) + .append(", ").append(args).append(");\n"); + } else { + sb.append(" return ").append(superCall).append(";\n") + .append(" }\n") + .append(" return getRecorder().call(M[").append(i).append("], () -> ").append(superCall) + .append(", ").append(args).append(");\n"); + } + sb.append(" }\n"); + } + sb.append("}\n"); + + try (Writer w = processingEnv.getFiler().createSourceFile(pkg + "." + name, annotated).openWriter()) { + w.write(sb.toString()); + } + } + + private String erasure(TypeMirror t) { + return processingEnv.getTypeUtils().erasure(t).toString(); + } + + private String signature(ExecutableElement m) { + return m.getSimpleName() + m.getParameters().stream().map(p -> erasure(p.asType())) + .collect(Collectors.joining(",", "(", ")")); + } + + /** + * @return the declaration of the parameters of m, named p0, p1, ... + */ + private static String parameters(ExecutableElement m) { + List params = m.getParameters(); + return IntStream.range(0, params.size()).mapToObj(k -> { + String t = params.get(k).asType().toString(); + if (m.isVarArgs() && k == params.size() - 1) { + t = t.substring(0, t.length() - 2) + "..."; + } + return t + " p" + k; + }).collect(Collectors.joining(", ")); + } + + /** + * @return the declaration of the type parameters of m, e.g. {@code }, or an empty + * string + */ + private static String typeParameters(ExecutableElement m) { + if (m.getTypeParameters().isEmpty()) { + return ""; + } + return m.getTypeParameters().stream().map(tp -> { + List bounds = tp.getBounds().stream().map(TypeMirror::toString) + .filter(b -> !b.equals("java.lang.Object")).toList(); + return bounds.isEmpty() ? tp.toString() : tp + " extends " + String.join(" & ", bounds); + }).collect(Collectors.joining(", ", "<", "> ")); + } + + private static String names(ExecutableElement m) { + return IntStream.range(0, m.getParameters().size()).mapToObj(k -> "p" + k).collect(Collectors.joining(", ")); + } +} diff --git a/codegen/src/main/resources/META-INF/services/javax.annotation.processing.Processor b/codegen/src/main/resources/META-INF/services/javax.annotation.processing.Processor new file mode 100644 index 0000000000..c00b8c9957 --- /dev/null +++ b/codegen/src/main/resources/META-INF/services/javax.annotation.processing.Processor @@ -0,0 +1 @@ +org.chocosolver.codegen.RecordingModelProcessor diff --git a/etc/spec-bench.sh b/etc/spec-bench.sh new file mode 100755 index 0000000000..03753f73b8 --- /dev/null +++ b/etc/spec-bench.sh @@ -0,0 +1,28 @@ +#!/bin/bash +# +# Equivalence bench of ModelSpec on a set of instances, each one in its own JVM. +# +# Usage: spec-bench.sh

+ * Prints one line: {@code RESULTstatusinstancesecondsdetail}, with status among OK, FAIL, + * SKIP (not journalizable), ERROR, OOM and TIMEOUT. + *

+ * Usage: {@code SpecEquivalenceMain [time limit in seconds]}; the system properties of + * {@link SpecEquivalenceTest} apply. + * + * @author Charles Prud'homme + */ +public class SpecEquivalenceMain { + + public static void main(String[] args) { + String file = args[0]; + long limit = args.length > 1 ? Long.parseLong(args[1]) : 600; + String name = Paths.get(file).getFileName().toString(); + System.setProperty("spec.progress", "false"); + PrintStream out = System.out; + // the parsers and the solver may print: keep stdout for the result only + System.setOut(new PrintStream(java.io.OutputStream.nullOutputStream())); + long start = System.currentTimeMillis(); + Thread watchdog = new Thread(() -> { + try { + Thread.sleep(limit * 1000); + result(out, "TIMEOUT", name, start, "exceeds " + limit + " s"); + Runtime.getRuntime().halt(3); + } catch (InterruptedException ignored) { + // done in time + } + }); + watchdog.setDaemon(true); + watchdog.start(); + SpecEquivalenceTest test = new SpecEquivalenceTest(); + int status = 0; + try { + test.testEquivalence(name, file); + result(out, "OK", name, start, test.usageSummary()); + } catch (SkipException e) { + result(out, "SKIP", name, start, e.getMessage()); + } catch (AssertionError e) { + result(out, "FAIL", name, start, e.getMessage()); + status = 1; + } catch (OutOfMemoryError e) { + result(out, "OOM", name, start, ""); + status = 2; + } catch (Throwable e) { + result(out, "ERROR", name, start, e.toString()); + status = 1; + } + watchdog.interrupt(); + out.flush(); + Runtime.getRuntime().halt(status); + } + + private static void result(PrintStream out, String status, String name, long start, String detail) { + String d = detail == null ? "" : detail.replace('\t', ' ').replace('\n', ' '); + if (d.length() > 500) { + d = d.substring(0, 500) + "..."; + } + out.printf("RESULT\t%s\t%s\t%.1f\t%s%n", status, name, (System.currentTimeMillis() - start) / 1000.0, d); + out.flush(); + } +} diff --git a/parsers/src/test/java/org/chocosolver/parser/spec/SpecEquivalenceTest.java b/parsers/src/test/java/org/chocosolver/parser/spec/SpecEquivalenceTest.java new file mode 100644 index 0000000000..fa35def394 --- /dev/null +++ b/parsers/src/test/java/org/chocosolver/parser/spec/SpecEquivalenceTest.java @@ -0,0 +1,331 @@ +/* + * This file is part of choco-parsers, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.parser.spec; + +import org.chocosolver.solver.Model; +import org.chocosolver.solver.Solver; +import org.chocosolver.solver.constraints.Constraint; +import org.chocosolver.solver.search.strategy.Search; +import org.chocosolver.solver.spec.ModelSpec; +import org.chocosolver.solver.spec.Recorder; +import org.chocosolver.solver.spec.SharedObjects; +import org.chocosolver.solver.spec.SpecException; +import org.chocosolver.solver.spec.Step; +import org.chocosolver.solver.variables.IntVar; +import org.chocosolver.solver.variables.Variable; +import org.testng.Assert; +import org.testng.SkipException; +import org.testng.annotations.AfterClass; +import org.testng.annotations.DataProvider; +import org.testng.annotations.Test; + +import java.io.IOException; +import java.io.PrintStream; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Objects; +import java.util.Set; +import java.util.TreeMap; +import java.util.concurrent.ExecutorService; +import java.util.concurrent.Executors; +import java.util.concurrent.Future; +import java.util.stream.Collectors; +import java.util.stream.Stream; + +/** + * Equivalence bench of {@link ModelSpec}: each instance is parsed into a plain model and into a model recorded + * with {@link Model#record}, whose spec is instantiated twice. All the models must have the same structure and the + * same search (solutions, nodes, fails), and the instances must not share mutable objects with each other or with + * the recorded model. + *

+ * Instances which cannot be journalized are skipped and reported in {@code target/spec-coverage.md}. + *

+ * System properties: + *

    + *
  • {@code spec.dir}: a directory of instances (.fzn, .xml, .xml.lzma) to use instead of the instances of the + * test resources listed in {@code spec-instances.txt} (one per family of problems);
    • + *
  • {@code spec.nodes}: node limit of each resolution (default: 100);
    • + *
  • {@code spec.sharing}: whether shared objects are looked for (default: true);
    • + *
  • {@code spec.sharing.maxsize}: maximum number of variables and constraints of a model in which shared + * objects are looked for (default: 20000);
    • + *
  • {@code spec.filter}: regular expression selecting the instances by file name (default: all).
    • + *
+ * + * @author Charles Prud'homme + */ +public class SpecEquivalenceTest { + + private static final long NODES = Long.getLong("spec.nodes", 100); + + /** + * The instances of the test resources to use, one per family of problems: similar instances add time, not + * coverage. + */ + private static final String INSTANCES = "spec-instances.txt"; + + /** + * Whether shared objects are looked for (memory consuming on large instances). + */ + private static final boolean SHARING = Boolean.parseBoolean(System.getProperty("spec.sharing", "true")); + + /** + * Shared objects are not looked for in models with more variables and constraints (memory consuming). + */ + private static final int SHARING_MAX_SIZE = Integer.getInteger("spec.sharing.maxsize", 20_000); + + /** + * Regular expression selecting the instances by name. + */ + private static final String FILTER = System.getProperty("spec.filter", ".*"); + + /** + * Two models parsed independently own their tuples and diagrams: not worth traversing to find the (global) + * objects they already share. + */ + private static final Set> BASELINE_ALLOWED = Set.of(PrintStream.class, + org.chocosolver.solver.constraints.extension.Tuples.class, + org.chocosolver.util.objects.graphs.MultivaluedDecisionDiagram.class); + + /** + * Types which may be shared by models: immutable, or shared by design. + */ + private static final Set> ALLOWED = Set.of(PrintStream.class); + + // coverage, aggregated over instances + private final Map unsupported = new TreeMap<>(); + private final List skipped = new ArrayList<>(); + private final Map usage = new TreeMap<>(); + private final Map baseline = new TreeMap<>(); + private final List sharingSkipped = new ArrayList<>(); + private int passed; + + @DataProvider + public Object[][] instances() throws IOException { + String dir = System.getProperty("spec.dir"); + List res = new ArrayList<>(); + if (dir != null) { + Path root = Paths.get(dir); + try (Stream files = Files.walk(root)) { + files.map(Path::toString) + .filter(f -> f.endsWith(".fzn") || f.endsWith(".xml") || f.endsWith(".xml.lzma")) + .filter(f -> Paths.get(f).getFileName().toString().matches(FILTER)) + .sorted() + .forEach(f -> res.add(new Object[]{root.relativize(Paths.get(f)).toString(), f})); + } + } else { + Path list = Paths.get(Objects.requireNonNull(getClass().getResource("/" + INSTANCES)).getPath()); + Path root = list.getParent(); + for (String line : Files.readAllLines(list)) { + String name = line.strip(); + if (!name.isEmpty() && !name.startsWith("#") + && Paths.get(name).getFileName().toString().matches(FILTER)) { + res.add(new Object[]{name, root.resolve(name).toString()}); + } + } + } + return res.toArray(new Object[0][]); + } + + @Test(groups = "spec", dataProvider = "instances", timeOut = 120_000) + public void testEquivalence(String name, String file) throws Exception { + progress(name); + // the models are kept alive only when needed, to save memory on large instances + Model direct = build(file, false); + String expected = structure(direct); + Set baseline = Set.of(); + boolean sharing = SHARING && direct.getNbVars() + direct.getNbCstrs() <= SHARING_MAX_SIZE; + if (!sharing) { + reportSharingSkipped(name); + } else { + // objects already shared by two models parsed independently (global singletons): excused by identity + baseline = SharedObjects.common(direct, build(file, false), BASELINE_ALLOWED, List.of()); + reportBaseline(baseline); + } + String stats = solve(direct); + direct = null; + + Model recorded = build(file, true); + ModelSpec spec; + try { + spec = recorded.getRecorder().snapshot(); + } catch (SpecException e) { + reportUnsupported(name, recorded.getRecorder()); + throw new SkipException("cannot be journalized: " + recorded.getRecorder().unsupported().get(0)); + } + assertSame(structure(recorded), expected, "recording changes the model"); + List excused = new ArrayList<>(SharedObjects.constantsOf(spec)); + excused.addAll(baseline); + List shared = new ArrayList<>(); + Model i1 = spec.instantiate().model(); + assertSame(structure(i1), expected, "the instantiated model differs"); + if (sharing) { + shared.addAll(SharedObjects.between(recorded, i1, ALLOWED, excused)); + } + recorded = null; + Model i2 = spec.instantiate().model(); + if (sharing) { + shared.addAll(SharedObjects.between(i1, i2, ALLOWED, excused)); + Assert.assertTrue(shared.isEmpty(), "shared mutable objects: " + shared); + } + + // same search, the instances being solved concurrently + ExecutorService pool = Executors.newFixedThreadPool(2); + try { + Future f1 = pool.submit(() -> solve(i1)); + Future f2 = pool.submit(() -> solve(i2)); + Assert.assertEquals(f1.get(), stats, "the instantiated model searches differently"); + Assert.assertEquals(f2.get(), stats, "the instantiated model searches differently"); + } finally { + pool.shutdownNow(); + } + reportUsage(spec); + } + + /** + * Log the instance being tested, to identify it if the JVM crashes. + */ + private static void progress(String name) throws IOException { + if (!Boolean.parseBoolean(System.getProperty("spec.progress", "true"))) { + return; + } + Path log = Paths.get(System.getProperty("user.dir"), "target", "spec-progress.log"); + Files.createDirectories(log.getParent()); + Files.writeString(log, name + "\n", java.nio.file.StandardOpenOption.CREATE, java.nio.file.StandardOpenOption.APPEND); + } + + /** + * Compare two structures, reporting the first different line. + */ + private static void assertSame(String actual, String expected, String message) { + if (!actual.equals(expected)) { + String[] a = actual.split("\n"); + String[] e = expected.split("\n"); + int i = 0; + while (i < a.length && i < e.length && a[i].equals(e[i])) { + i++; + } + Assert.fail(message + ", line " + i + ": expected <" + (i < e.length ? e[i] : "EOF") + + "> but was <" + (i < a.length ? a[i] : "EOF") + ">"); + } + } + + /** + * Parse file into a plain model, or into a recorded model. + */ + private static Model build(String file, boolean record) { + try { + return SpecParsers.parse(file, 1, record).getModel(); + } catch (IllegalStateException e) { + throw new SkipException(e.getMessage()); + } + } + + /** + * @return a description of the structure of the model: variables and constraints, in order + */ + private static String structure(Model m) { + StringBuilder sb = new StringBuilder(); + sb.append(m.getNbVars()).append(" vars, ").append(m.getNbCstrs()).append(" cstrs, objective: ") + .append(m.getObjective() == null ? "none" : m.getObjective().getName()).append('\n'); + for (Variable v : m.getVars()) { + sb.append(v.getClass().getSimpleName()).append(' ').append(v.getName()); + if (v instanceof IntVar) { + sb.append(' ').append(((IntVar) v).getLB()).append("..").append(((IntVar) v).getUB()) + .append(" #").append(((IntVar) v).getDomainSize()); + } + sb.append('\n'); + } + m.getGroups().forEach(g -> sb.append("group ").append(g.getName()).append(Arrays.stream(g.getVariables()) + .map(Variable::getName).collect(Collectors.joining(",", "[", "]"))).append('\n')); + for (Constraint c : m.getCstrs()) { + sb.append(c.getName()).append(Arrays.stream(c.getPropagators()) + .map(p -> p.getClass().getSimpleName() + "/" + p.getNbVars()) + .collect(Collectors.joining(",", "[", "]"))).append('\n'); + } + return sb.toString(); + } + + /** + * Solve with the default (deterministic) search, limited in nodes. + */ + private static String solve(Model m) { + Solver s = m.getSolver(); + Search.defaultSearch(m); + s.limitNode(NODES); + Number best = null; + while (s.solve()) { + if (m.getObjective() != null) { + best = s.getBestSolutionValue(); + } + } + return s.getSolutionCount() + " sols, " + s.getNodeCount() + " nodes, " + s.getFailCount() + " fails" + + (best == null ? "" : ", best=" + best); + } + + private synchronized void reportUnsupported(String name, Recorder recorder) { + skipped.add(name + " (" + recorder.unsupported().size() + ")"); + Set reasons = new HashSet<>(); + for (Recorder.Unsupported u : recorder.unsupported()) { + reasons.add(u.operation() + ": " + u.reason().replaceAll("variable \\S+", "variable _")); + } + reasons.forEach(r -> unsupported.merge(r, 1, Integer::sum)); + } + + private synchronized void reportSharingSkipped(String name) { + sharingSkipped.add(name); + } + + private synchronized void reportBaseline(Set objects) { + objects.stream().map(o -> o.getClass().getName()).distinct().forEach(t -> baseline.merge(t, 1, Integer::sum)); + } + + private synchronized void reportUsage(ModelSpec spec) { + passed++; + Set used = new HashSet<>(); + for (Step s : spec.steps()) { + used.add(s instanceof Step.Call ? ((Step.Call) s).method().name() : s.getClass().getSimpleName()); + } + used.forEach(u -> usage.merge(u, 1, Integer::sum)); + } + + /** + * @return the kinds of steps used by the journalized instances, and the instances whose sharing was not + * checked + */ + synchronized String usageSummary() { + return String.join(",", usage.keySet()) + (sharingSkipped.isEmpty() ? "" : " [sharing not checked]"); + } + + @AfterClass(alwaysRun = true) + public void writeReport() throws IOException { + StringBuilder sb = new StringBuilder(); + sb.append("# ModelSpec coverage\n\n") + .append("- journalized and equivalent: ").append(passed).append('\n') + .append("- not journalizable: ").append(skipped.size()).append("\n\n") + .append("## Unsupported operations (number of instances)\n\n"); + unsupported.entrySet().stream().sorted(Map.Entry.comparingByValue().reversed()) + .forEach(e -> sb.append("- ").append(e.getValue()).append(" × ").append(e.getKey()).append('\n')); + sb.append("\n## Not journalizable instances\n\n"); + skipped.forEach(s -> sb.append("- ").append(s).append('\n')); + sb.append("\n## Shared objects not looked for (large models): ").append(sharingSkipped.size()).append("\n\n"); + sharingSkipped.forEach(n -> sb.append("- ").append(n).append('\n')); + sb.append("\n## Objects shared by two models parsed independently (number of instances)\n\n"); + baseline.forEach((k, v) -> sb.append("- ").append(k).append(": ").append(v).append('\n')); + sb.append("\n## Steps used by the journalized instances (number of instances)\n\n"); + usage.forEach((k, v) -> sb.append("- ").append(k).append(": ").append(v).append('\n')); + Path out = Paths.get(System.getProperty("user.dir"), "target", "spec-coverage.md"); + Files.createDirectories(out.getParent()); + Files.writeString(out, sb.toString()); + System.out.println(sb); + } +} diff --git a/parsers/src/test/java/org/chocosolver/parser/spec/SpecOverheadBench.java b/parsers/src/test/java/org/chocosolver/parser/spec/SpecOverheadBench.java new file mode 100644 index 0000000000..1593d2dbff --- /dev/null +++ b/parsers/src/test/java/org/chocosolver/parser/spec/SpecOverheadBench.java @@ -0,0 +1,156 @@ +/* + * This file is part of choco-parsers, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.parser.spec; + +import org.chocosolver.solver.Model; +import org.chocosolver.solver.spec.ModelSpec; + +import java.io.PrintStream; +import java.lang.ref.Reference; +import java.lang.management.ManagementFactory; +import java.nio.file.Paths; +import java.util.Arrays; +import java.util.Locale; + +/** + * Measures, on one instance, the overhead of recording the construction of a model: + *
    + *
  • building time: parsing into a plain model ({@code create}) versus into a recorded model + * ({@code record});
    • + *
  • cost of {@code snapshot} and of {@code instantiate} (replay of the spec), compared to parsing;
    • + *
  • memory: the plain model, the recorded model (model and journal), and the spec alone.
    • + *
+ * Times are medians over {@code spec.reps} repetitions (default 5), after a warm-up. + *

+ * To be launched in its own JVM (see {@code etc/spec-bench.sh}, with {@code SPEC_MAIN} set to this class). Prints one + * line: {@code RESULTstatusinstancesecondsmetrics}, metrics being {@code key=value} pairs + * separated by {@code ;}. + *

+ * Usage: {@code SpecOverheadBench

    + *
  • (a) as the parsers currently do: n parsings, one after the other;
    • + *
  • (a') n parsings run concurrently;
    • + *
  • (b) with a {@link ModelSpec}: one recorded parsing (the master, which also solves), then n-1 models + * instantiated concurrently.
    • + *
+ * For each: the building time and the heap used by the n models. Optionally, (a) and (b) are solved with a + * {@link ParallelPortfolio} under the same time limit. + *

+ * To be launched in its own JVM (see {@code etc/spec-bench.sh}, with {@code SPEC_MAIN} set to this class). Prints one + * line: {@code RESULTstatusinstancesecondsmetrics}, metrics being + * {@code key=value} pairs separated by {@code ;}. + *

+ * Usage: {@code SpecPortfolioBench

. +flatzinc/2012/amaze+amaze+2012-07-04.fzn +flatzinc/2012/carpet-cutting+cc_base+mzn_rnd_test.16.fzn +flatzinc/2012/fast-food+fastfood+ff59.fzn +flatzinc/2012/filters+filter+fir_1_1.fzn +flatzinc/2012/league+league+model20-3-5.fzn +flatzinc/2012/mspsp+mspsp+medium_02.fzn +flatzinc/2012/nonogram+non+non_fast_4.fzn +flatzinc/2012/parity-learning+parity-learning+44_22_5.3.fzn +flatzinc/2012/pattern-set-mining-k2+pattern_set_mining_k2+audiology.fzn +flatzinc/2012/project-planning+ProjectPlannertest_12_8.fzn +flatzinc/2012/radiation+radiation+m07_07_20.fzn +flatzinc/2012/ship-schedule+ship-schedule.cp+7ShipsMixed.fzn +flatzinc/2012/solbat+sb+sb_14_14_6_0.fzn +flatzinc/2012/still-life-wastage+still-life+09.fzn +flatzinc/2012/tpp+tpp+tpp_5_3_20_1.fzn +flatzinc/2012/train+train+instance.12.fzn +flatzinc/2012/vrp+vrp+P-n20-k2.vrp.fzn +flatzinc/2015/gfd-schedule+n120f5d50m50k20.fzn +flatzinc/2016/nfc_12_2_10.fzn +flatzinc/2017/tcgc2+k10_34.fzn +flatzinc/2018/oocsp_racks+050_r1n.fzn +flatzinc/2018/rotating-workforce+ex1479.fzn +flatzinc/2018/steiner-tree+es10fst03.stp.fzn +flatzinc/2018/test-scheduling+t30m10r3-15.fzn +flatzinc/2019/ccmcp+3_20_0_25_5.fzn +flatzinc/2019/fm3_3.fzn +flatzinc/2019/foxgeesecorn+54.fzn +flatzinc/2019/group+u6g1pref1.fzn +flatzinc/2019/median_string_dp+p2_10_8-0.fzn +flatzinc/2019/mknapsack_global+mknap2-1.fzn +flatzinc/2019/zephyrus+12_6_6_3.fzn +flatzinc/2020/bnn+inventory_4_8s.fzn +flatzinc/2020/is+v1HjuSBQMb_new.fzn +flatzinc/2020/lot_sizing_cp+pigment15b.psp.fzn +flatzinc/2020/p1f-pjs+10_new.fzn +flatzinc/2020/pentominoes+02.fzn +flatzinc/2020/skill_allocation+mzn_1m_1.fzn +flatzinc/2020/soccer+xIGData_22_12_22_5.fzn +flatzinc/2020/stable-goods-solution+s-d6.fzn +flatzinc/2021/atsp+instance5_0p15.fzn +flatzinc/2021/connect__0018.fzn +flatzinc/2021/feistel.fzn +flatzinc/2021/mapping_mesh2x2_2.fzn +flatzinc/2021/perfect_square+205.fzn +flatzinc/2021/physician-scheduling.fzn +flatzinc/2021/yumi-dynamic+p_10.fzn +xcsp/2024/AztecDiamondSym-12_c24.xml.lzma +xcsp/2024/BinPacking-n1c1w1a_c24.xml.lzma +xcsp/2024/Cargo-01-0s-1913_m17.xml.lzma +xcsp/2024/Charlotte-18-2_c24.xml.lzma +xcsp/2024/Drinking-010000_c24.xml.lzma +xcsp/2024/FoolSolitaire-dec2-0-2.xml.lzma +xcsp/2024/SameQueensKnights-b-15_c24.xml.lzma +xcsp/2024/StillLife-12-12_c24.xml.lzma +xcsp/2024/TestScheduling-t020m10r03-1_c24.xml.lzma +xcsp/2024/TravelingTournament-galaxy06_c24.xml.lzma +flatzinc/2025/hitori_h5-1.fzn +flatzinc/alpha/alpha.fzn +xcsp/basics/AllInterval-005.xml.lzma +xcsp/basics/Allergy.xml.lzma +xcsp/basics/Auction-cnt-example_c18.xml.lzma +xcsp/basics/Auction-sum-example_c18.xml.lzma +xcsp/basics/Bacp-m1-06_c18.xml.lzma +xcsp/basics/Bibd-sc-06-050-25-03-10.xml.lzma +xcsp/basics/Bibd-sum-06-050-25-03-10.xml.lzma +xcsp/basics/BinPacking-mdd-n1c1w4a.xml.lzma +xcsp/basics/BinPacking-sum-n1c1w4a.xml.lzma +xcsp/basics/BinPacking-tab-n1c1w4a.xml.lzma +xcsp/basics/Blackhole-04-3-00.xml.lzma +xcsp/basics/BusScheduling-cnt-t1.xml.lzma +xcsp/basics/CarSequencing-dingbas.xml.lzma +xcsp/basics/ChessboardColoration-07-07.xml.lzma +xcsp/basics/ColouredQueens-07.xml.lzma +xcsp/basics/CostasArray-12.xml.lzma +xcsp/basics/Crossword-lex-vg-5-6.xml.lzma +xcsp/basics/CrosswordDesign-03-4-rom_c18.xml.lzma +xcsp/basics/CryptoPuzzle-cross-roads-danger.xml.lzma +xcsp/basics/Cutstock-small.xml.lzma +xcsp/basics/DistinctVectors-30-050-02.xml.lzma +xcsp/basics/Domino-300-300.xml.lzma +xcsp/basics/Fapp-m2s-ex2_c18.xml.lzma +xcsp/basics/Fastfood-ff10.xml.lzma +xcsp/basics/Filters-dct_2_3.xml.lzma +xcsp/basics/FlexibleJobshop-easy01.xml.lzma +xcsp/basics/Furniture.xml.lzma +xcsp/basics/GolombRuler-09-a3.xml.lzma +xcsp/basics/GracefulGraph-K02-P04.xml.lzma +xcsp/basics/GraphColoring-3-fullins-4.xml.lzma +xcsp/basics/GraphColoring-qwhdec-o5-h10-1.xml.lzma +xcsp/basics/Hanoi-05.xml.lzma +xcsp/basics/Kakuro-easy-000-ext.xml.lzma +xcsp/basics/Kakuro-easy-000-sumdiff.xml.lzma +xcsp/basics/Knapsack-30-100-00.xml.lzma +xcsp/basics/KnightTour-06-ext03.xml.lzma +xcsp/basics/KnightTour-06-int.xml.lzma +xcsp/basics/Langford-3-10.xml.lzma +xcsp/basics/LangfordBin-08.xml.lzma +xcsp/basics/LowAutocorrelation-015.xml.lzma +xcsp/basics/MSPSP-easy_01.xml.lzma +xcsp/basics/MSPSP-hard_01.xml.lzma +xcsp/basics/MagicSequence-008-ca.xml.lzma +xcsp/basics/MagicSequence-008-co.xml.lzma +xcsp/basics/MagicSquare-4-table.xml.lzma +xcsp/basics/MagicSquare-6-mdd.xml.lzma +xcsp/basics/MagicSquare-6-sum.xml.lzma +xcsp/basics/MagicSquare-9-f10-01.xml.lzma +xcsp/basics/Mario-easy-4.xml.lzma +xcsp/basics/MarketSplit-01.xml.lzma +xcsp/basics/MultiKnapsack-1-01.xml.lzma +xcsp/basics/MultiKnapsack-1-0_X2.xml.lzma +xcsp/basics/NFC-12_2_10.xml.lzma +xcsp/basics/Nonogram-001-regular.xml.lzma +xcsp/basics/Nonogram-001-table.xml.lzma +xcsp/basics/NurseRostering-00_c18.xml.lzma +xcsp/basics/Opd-07-007-003.xml.lzma +xcsp/basics/Ortholatin-005.xml.lzma +xcsp/basics/Pb-gr-05.xml.lzma +xcsp/basics/Pb-robin08.xml.lzma +xcsp/basics/PeacableArmies-m2-05_c18.xml.lzma +xcsp/basics/PizzaVoucher-10a_c18.xml.lzma +xcsp/basics/Primes-15-20-2-1.xml.lzma +xcsp/basics/PrizeCollecting-15-3-5-0.xml.lzma +xcsp/basics/QuadraticAssignment-bur26a.xml.lzma +xcsp/basics/QuadraticAssignment-qap.xml.lzma +xcsp/basics/QuadraticAssignment-qap_c18.xml.lzma +xcsp/basics/QuasiGroup-3-04.xml.lzma +xcsp/basics/QueenAttacking-06.xml.lzma +xcsp/basics/Queens-0008-m1.xml.lzma +xcsp/basics/RadarSurveillance-8-24-3-2-00.xml.lzma +xcsp/basics/Ramsey-12.xml.lzma +xcsp/basics/Rcpsp-j30-01-01_c18.xml.lzma +xcsp/basics/Rlfap-graph-04-opt_c18.xml.lzma +xcsp/basics/RoomMate-sr0050-int.xml.lzma +xcsp/basics/Sat-flat200-00-clause.xml.lzma +xcsp/basics/SocialGolfers-4-3-4-cp.xml.lzma +xcsp/basics/Sonet-s2ring02.xml.lzma +xcsp/basics/SportsScheduling-08.xml.lzma +xcsp/basics/SteelMillSlab-m1-simple_c18.xml.lzma +xcsp/basics/SteelMillSlab-m2s-mini-simple_c18.xml.lzma +xcsp/basics/Steiner3-08.xml.lzma +xcsp/basics/StillLife-03-06.xml.lzma +xcsp/basics/StillLife-wastage-03.xml.lzma +xcsp/basics/StripPacking-C1P1.xml.lzma +xcsp/basics/Subisomorphism-A-10.xml.lzma +xcsp/basics/Sudoku-s01a-alldiff.xml.lzma +xcsp/basics/SumColoring-myciel4_c18.xml.lzma +xcsp/basics/Taillard-js-015-15-0.xml.lzma +xcsp/basics/Taillard-os-04-04-0.xml.lzma +xcsp/basics/Tal-01_c18.xml.lzma +xcsp/basics/TeamAssignment-data1_4_6.xml.lzma +xcsp/basics/TemplateDesign-m1s-1_c18.xml.lzma +xcsp/basics/TemplateDesign-m2-1_c18.xml.lzma +xcsp/basics/TestSchedulingM18-t30m10r3-15.xml.lzma +xcsp/basics/Tpp-3-3-20-1.xml.lzma +xcsp/basics/TravelingTournament-a3-galaxy04_c18.xml.lzma +xcsp/basics/TravellingSalesman-13-13-0.xml.lzma +xcsp/basics/Vrp-A-n32-k5.xml.lzma +xcsp/basics/Vrp-P-n16-k8.xml.lzma +xcsp/basics/Warehouse-opl.xml.lzma +xcsp/basics/Zebra.xml.lzma +flatzinc/basics/all_different+test_globals.fzn +flatzinc/basics/basic+test_basic.fzn +flatzinc/basics/basic2+test_basic2+large.fzn +flatzinc/basics/bool_indomain_max+input_order.fzn +flatzinc/basics/circuit+test_globals.fzn +flatzinc/basics/cumulative+test_globals.fzn +xcsp/basics/driverlogw-09.xml.lzma +flatzinc/basics/int_indomain_median+anti_first_fail.fzn +xcsp/basics/qcp-15-120-00_X2.xml.lzma +xcsp/basics/qwh-o30-h374-01.xml.lzma +flatzinc/basics/seq_search_1.fzn +xcsp/basics/testExtension2.xml.lzma +xcsp/basics/testObjective1.xml.lzma +xcsp/basics/testPrimitive.xml.lzma +flatzinc/basics/test_set_lt_2.fzn diff --git a/pom.xml b/pom.xml index 140ba4bf54..8554e1e7d3 100644 --- a/pom.xml +++ b/pom.xml @@ -58,6 +58,7 @@ + codegen solver parsers examples diff --git a/solver/pom.xml b/solver/pom.xml index e3b678fd11..abe156e867 100644 --- a/solver/pom.xml +++ b/solver/pom.xml @@ -36,6 +36,14 @@ + + + org.choco-solver + choco-codegen + ${project.version} + provided + true + dk.brics.automaton automaton @@ -61,6 +69,19 @@ + + org.apache.maven.plugins + maven-compiler-plugin + + + + org.choco-solver + choco-codegen + ${project.version} + + + + maven-assembly-plugin ${maven.assembly.plugin.version} diff --git a/solver/src/main/java/module-info.java b/solver/src/main/java/module-info.java index 0c697c0c8f..4f378291c0 100644 --- a/solver/src/main/java/module-info.java +++ b/solver/src/main/java/module-info.java @@ -92,6 +92,7 @@ exports org.chocosolver.solver.search.strategy.selectors.values.graph.node; exports org.chocosolver.solver.search.strategy.selectors.values.graph.priority; exports org.chocosolver.solver.search.strategy.strategy; + exports org.chocosolver.solver.spec; exports org.chocosolver.solver.variables; exports org.chocosolver.solver.variables.delta; //exports org.chocosolver.solver.variables.delta.monitor; diff --git a/solver/src/main/java/org/chocosolver/solver/Model.java b/solver/src/main/java/org/chocosolver/solver/Model.java index 4e48e165cf..ebb801a392 100755 --- a/solver/src/main/java/org/chocosolver/solver/Model.java +++ b/solver/src/main/java/org/chocosolver/solver/Model.java @@ -19,6 +19,8 @@ import org.chocosolver.solver.objective.IObjectiveManager; import org.chocosolver.solver.objective.ObjectiveFactory; import org.chocosolver.solver.propagation.PropagationEngine; +import org.chocosolver.solver.spec.Recorder; +import org.chocosolver.solver.spec.RecordingModel; import org.chocosolver.solver.variables.*; import org.chocosolver.util.tools.ArrayUtils; import org.chocosolver.util.tools.VariableUtils; @@ -256,6 +258,95 @@ public Model() { this("Model-" + nextModelNum()); } + /** + * Creates a model, as {@link #Model(String, Settings)}. Such a model cannot be duplicated: see + * {@link #record(String, Settings)}. + * + * @param name name of the model + * @param settings settings of the model + * @return a new model + */ + public static Model create(String name, Settings settings) { + return new Model(name, settings); + } + + /** + * Creates a model, as {@link #Model(String)}. Such a model cannot be duplicated: see {@link #record(String)}. + * + * @param name name of the model + * @return a new model + */ + public static Model create(String name) { + return new Model(name); + } + + /** + * Creates a model, as {@link #Model(Settings)}. Such a model cannot be duplicated: see {@link #record(Settings)}. + * + * @param settings settings of the model + * @return a new model + */ + public static Model create(Settings settings) { + return new Model(settings); + } + + /** + * Creates a model, as {@link #Model()}. Such a model cannot be duplicated: see {@link #record()}. + * + * @return a new model + */ + public static Model create() { + return new Model(); + } + + /** + * Creates a model whose construction is recorded, so that it can be duplicated: build it as usual, then call + * {@link #duplicate()} to get independent copies, or use {@link ParallelPortfolio#of(Model, int)} to solve it with + * several threads (it is then the first worker). The copies themselves are not recorded, hence cannot be + * duplicated. Only the construction of the model is recorded, not the configuration of its solver (search, + * limits...), and a model cannot be duplicated once its resolution has started. + *

+ * A custom constraint must be built with {@link #custom(String, Variable[], java.util.function.Function)} (or its + * variant with data), not directly from propagators. + * + * @param name name of the model + * @param settings settings of the model + * @return a model which can be duplicated + * @see org.chocosolver.solver.spec.RecordingModel + */ + public static Model record(String name, Settings settings) { + return new RecordingModel(name, settings); + } + + /** + * Creates a model whose construction is recorded, see {@link #record(String, Settings)}. + * + * @param name name of the model + * @return a model which can be duplicated + */ + public static Model record(String name) { + return new RecordingModel(name); + } + + /** + * Creates a model whose construction is recorded, see {@link #record(String, Settings)}. + * + * @param settings settings of the model + * @return a model which can be duplicated + */ + public static Model record(Settings settings) { + return new RecordingModel(settings); + } + + /** + * Creates a model whose construction is recorded, see {@link #record(String, Settings)}. + * + * @return a model which can be duplicated + */ + public static Model record() { + return new RecordingModel(); + } + /** * For autonumbering anonymous models. */ @@ -968,6 +1059,7 @@ private void _post(boolean permanent, Constraint... cs) throws SolverException { } // specific behavior for dynamic addition and/or reified constraints for (Constraint c : cs) { + assert ownsVariablesOf(c) : "Constraint " + c.getName() + " involves variables of another model"; for (Propagator p : c.getPropagators()) { if (p.isPassive()) { throw new SolverException("Try to add a constraint with a passive propagator"); @@ -983,6 +1075,21 @@ private void _post(boolean permanent, Constraint... cs) throws SolverException { } } + /** + * @return true if all the variables of c belong to this model (e.g., a constraint built by a + * lambda must not capture the variables of another model) + */ + private boolean ownsVariablesOf(Constraint c) { + for (Propagator p : c.getPropagators()) { + for (Variable v : p.getVars()) { + if (v.getModel() != this) { + return false; + } + } + } + return true; + } + /** * Posts constraints cs temporary, that is, they will be unposted upon backtrack. *

@@ -1137,6 +1244,34 @@ public void displayPropagatorOccurrences() { //////////////////////////////////////////// RELATED TO MODELING FACTORIES ///////////////////////////////////////// //////////////////////////////////////////////////////////////////////////////////////////////////////////////////// + /** + * Message of the exception thrown when duplicating a model which is not recorded. + */ + static final String NOT_RECORDED = "This model cannot be duplicated: create it with Model.record(...)"; + + /** + * Internal use only. + * + * @return the recorder of this model, or null if this model is not a + * {@link org.chocosolver.solver.spec.RecordingModel} + */ + public Recorder getRecorder() { + return null; + } + + /** + * Creates an independent copy of this model: same variables, same constraints, same objective, in the same + * order, hence the same resolution with a deterministic search. The copy can be solved in another thread. + * The copy itself cannot be duplicated. + * + * @return a copy of this model + * @throws SolverException if this model was not created with {@link #record(String)}, or if its resolution + * has started, or if one of its constraints was not built by a factory method + */ + public Model duplicate() { + throw new SolverException(NOT_RECORDED); + } + @Override public Model ref() { return this; diff --git a/solver/src/main/java/org/chocosolver/solver/ParallelPortfolio.java b/solver/src/main/java/org/chocosolver/solver/ParallelPortfolio.java index 956fbd551a..3f07945ee5 100644 --- a/solver/src/main/java/org/chocosolver/solver/ParallelPortfolio.java +++ b/solver/src/main/java/org/chocosolver/solver/ParallelPortfolio.java @@ -18,21 +18,31 @@ import org.chocosolver.solver.search.strategy.SearchParams; import org.chocosolver.solver.search.strategy.selectors.values.IntValueSelector; import org.chocosolver.solver.search.strategy.strategy.AbstractStrategy; +import org.chocosolver.solver.spec.ModelSpec; +import org.chocosolver.solver.spec.Recorder; +import org.chocosolver.solver.spec.Resolver; +import org.chocosolver.solver.spec.SpecSolution; +import org.chocosolver.solver.spec.Variant; import org.chocosolver.solver.variables.IntVar; import org.chocosolver.solver.variables.Variable; import java.util.ArrayList; +import java.util.Collections; import java.util.HashMap; +import java.util.IdentityHashMap; import java.util.List; +import java.util.Map; import java.util.Spliterator; import java.util.concurrent.ExecutionException; import java.util.concurrent.ExecutorService; import java.util.concurrent.Executors; +import java.util.concurrent.Future; import java.util.concurrent.atomic.AtomicBoolean; import java.util.concurrent.atomic.AtomicInteger; import java.util.function.BiFunction; import java.util.function.Consumer; import java.util.function.Function; +import java.util.stream.Collectors; import java.util.stream.Stream; import java.util.stream.StreamSupport; @@ -140,6 +150,17 @@ public class ParallelPortfolio { */ private Model finder; + /** + * For a portfolio built from a {@link ModelSpec}: the resolver of each model, which maps the identifiers of the + * spec to its objects. + */ + private final Map resolvers = new IdentityHashMap<>(); + + /** + * For a portfolio built from a recorded model: that model, in whose terms the solutions are expressed. + */ + private Model origin; + //////////////////////////////////////////////////////////////////////////////////////////////////////////////////// /////////////////////////////////////// CONSTRUCTOR ////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////////////////////////////////////////////////// @@ -169,10 +190,175 @@ public ParallelPortfolio() { this(true); } + /** + * Creates a portfolio of n workers: model itself (the first worker) and n-1 copies of it, + * built concurrently. The search heuristics of the copies are diversified, as well as the one of model + * unless a search strategy was declared on it. {@link #getBestSolution()} expresses the solutions found with the + * variables of model. + *

+ * Once its resolution has started, model cannot be duplicated anymore: duplicate it beforehand if needed. + * Note that a worker may not even start if another one completes the search first. + * 

{@code
+     * Model model = Model.record("pb");
+     * // ... variables and constraints ...
+     * ParallelPortfolio portfolio = ParallelPortfolio.of(model, 4);
+     * if (portfolio.solve()) {
+     *     Solution s = portfolio.getBestSolution();
+     * }
+     * }
+ * + * @param model a model created with {@link Model#record(String)} + * @param n number of workers, model included + * @return a portfolio of n workers + * @throws SolverException if model cannot be duplicated + */ + public static ParallelPortfolio of(Model model, int n) { + return of(model, Collections.nCopies(Math.max(0, n - 1), Variant.IDENTITY)); + } + + /** + * Creates a portfolio whose workers are model itself (the first worker) and one copy of it per variant, + * built concurrently, see {@link #of(Model, int)} and {@link #of(ModelSpec, List)}. + * + * @param model a model created with {@link Model#record(String)} + * @param variants one variant per copy + * @return a portfolio of variants.size()+1 workers + * @throws SolverException if model cannot be duplicated + */ + public static ParallelPortfolio of(Model model, List variants) { + Recorder recorder = model.getRecorder(); + if (recorder == null) { + throw new SolverException(Model.NOT_RECORDED); + } + List specs = specs(recorder.snapshot(), variants); + ParallelPortfolio portfolio = new ParallelPortfolio(); + portfolio.origin = model; + portfolio.addModel(model, model.getSolver().getSearch() != null, true); + portfolio.resolvers.put(model, recorder); + portfolio.add(specs, instantiate(specs), 2); + return portfolio; + } + + /** + * Creates a portfolio of n identical models built from spec, whose search heuristics are then + * diversified by the portfolio (see {@link #addModel(Model)}). This is equivalent to adding n models built + * the same way, but the problem is described once and the models are built concurrently. + * + * @param spec the spec of the problem + * @param n number of models + * @return a portfolio of n models + */ + public static ParallelPortfolio of(ModelSpec spec, int n) { + return of(spec, Collections.nCopies(n, Variant.IDENTITY)); + } + + /** + * Creates a portfolio with one model per variant of spec, built concurrently. + * A model whose variant declares a search ({@link ModelSpec#search()}) keeps it; the search heuristics of the + * other models are diversified by the portfolio. + *

+ * The solutions found can be read with the identifiers of the spec: see {@link #getBestSpecSolution()} and + * {@link #resolverOf(Model)}. + * + * @param spec the spec of the problem + * @param variants one variant per model (see {@link Variant#IDENTITY}) + * @return a portfolio with one model per variant + */ + public static ParallelPortfolio of(ModelSpec spec, List variants) { + List specs = specs(spec, variants); + ParallelPortfolio portfolio = new ParallelPortfolio(); + portfolio.add(specs, instantiate(specs), 1); + return portfolio; + } + + private static List specs(ModelSpec spec, List variants) { + return variants.stream().map(spec::with).collect(Collectors.toList()); + } + + /** + * Add the instances of specs, numbered from rank. + */ + private void add(List specs, List instances, int rank) { + for (int i = 0; i < instances.size(); i++) { + Model m = instances.get(i).model(); + m.setName(m.getName() + "_" + (rank + i)); + addModel(m, specs.get(i).search() != null, true); + resolvers.put(m, instances.get(i)); + } + } + + /** + * @return the instances of specs, built concurrently + */ + private static List instantiate(List specs) { + if (specs.isEmpty()) { + return List.of(); + } + ExecutorService pool = Executors.newFixedThreadPool( + Math.min(specs.size(), Runtime.getRuntime().availableProcessors())); + try { + List> futures = new ArrayList<>(specs.size()); + for (ModelSpec s : specs) { + futures.add(pool.submit(() -> s.instantiate())); + } + List instances = new ArrayList<>(specs.size()); + for (Future f : futures) { + instances.add(f.get()); + } + return instances; + } catch (InterruptedException e) { + Thread.currentThread().interrupt(); + throw new SolverException("Interrupted while building the models of the portfolio"); + } catch (ExecutionException e) { + throw e.getCause() instanceof RuntimeException re ? re : new SolverException(e.getCause().getMessage()); + } finally { + pool.shutdownNow(); + } + } + //////////////////////////////////////////////////////////////////////////////////////////////////////////////////// /////////////////////////////////////// API ////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////////////////////////////////////////////////// + /** + * @param model a model of this portfolio + * @return the resolver of model if this portfolio was built from a {@link ModelSpec}, null otherwise + */ + public Resolver resolverOf(Model model) { + return resolvers.get(model); + } + + /** + * To be called once {@link #solve()} returned true. + * + * @return the (best) solution found, expressed with the variables of the recorded model for a portfolio built + * with {@link #of(Model, int)}, with the variables of the model which found it otherwise + * @throws SolverException if no solution was found + */ + public Solution getBestSolution() { + if (finder == null) { + throw new SolverException("No solution found"); + } + return origin == null || finder == origin + ? new Solution(finder).record() + : getBestSpecSolution().toSolution(origin.getRecorder()); + } + + /** + * To be called once {@link #solve()} returned true, on a portfolio built from a {@link ModelSpec} (or a + * recorded model). + * + * @return the (best) solution found, with the identifiers of the spec: it can be read from any model of the spec + * @throws SolverException if this portfolio was not built from a spec, or if no solution was found + */ + public SpecSolution getBestSpecSolution() { + Resolver r = finder == null ? null : resolvers.get(finder); + if (r == null) { + throw new SolverException(finder == null ? "No solution found" : "The portfolio was not built from a ModelSpec"); + } + return SpecSolution.record(r); + } + /** * Calling this method will ensure that workers equipped with a restart policy not only * record nogoods from themselves (based on {@link NogoodFromRestarts}) but also based on diff --git a/solver/src/main/java/org/chocosolver/solver/Solver.java b/solver/src/main/java/org/chocosolver/solver/Solver.java index f317203442..48c3330b0d 100644 --- a/solver/src/main/java/org/chocosolver/solver/Solver.java +++ b/solver/src/main/java/org/chocosolver/solver/Solver.java @@ -1376,6 +1376,9 @@ public void setSearch(AbstractStrategy... strategies) { strategies = Arrays.stream(strategies).filter(Objects::nonNull) .flatMap(s -> (s instanceof StrategiesSequencer) ? Arrays.stream(((StrategiesSequencer) s).getStrategies()) : Stream.of(s)) .toArray(AbstractStrategy[]::new); + assert Arrays.stream(strategies).allMatch(s -> s.getVariables() == null + || Arrays.stream(s.getVariables()).allMatch(v -> v == null || v.getModel() == mModel)) + : "A search strategy involves variables of another model"; if (strategies.length == 0) { M.removeStrategy(); } else if (strategies.length == 1) { diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/Constraint.java b/solver/src/main/java/org/chocosolver/solver/constraints/Constraint.java index 307b742a7b..d8400e9842 100755 --- a/solver/src/main/java/org/chocosolver/solver/constraints/Constraint.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/Constraint.java @@ -10,6 +10,8 @@ import org.chocosolver.solver.constraints.reification.Opposite; import org.chocosolver.solver.exception.SolverException; import org.chocosolver.solver.search.SearchState; +import org.chocosolver.solver.spec.Recorder; +import org.chocosolver.solver.spec.Step; import org.chocosolver.solver.variables.BoolVar; import org.chocosolver.util.ESat; @@ -185,6 +187,15 @@ public final boolean isReified() { * @param bool the variable to reify with */ public void reifyWith(BoolVar bool) { + Recorder r = recorder(); + if (r != null) { + r.link(Step.Link.Kind.REIFY_WITH, this, bool, () -> doReifyWith(bool)); + } else { + doReifyWith(bool); + } + } + + private void doReifyWith(BoolVar bool) { if (boolReif != null) { if (opposite == null) { throw new SolverException("try to reify an implied constraint"); @@ -219,6 +230,11 @@ public void reifyWith(BoolVar bool) { * @return the boolean reifying the constraint */ public final BoolVar reify() { + Recorder r = recorder(); + return r != null ? r.reify(this, this::doReify) : doReify(); + } + + private BoolVar doReify() { if (boolReif == null) { Model model = propagators[0].getModel(); reifyWith(model.boolVar(model.generateName("REIF_"))); @@ -243,7 +259,12 @@ public final BoolVar reify() { * @param r a boolean variable */ public final void implies(BoolVar r) { - this.reify().imp(r).post(); + Recorder rec = recorder(); + if (rec != null) { + rec.link(Step.Link.Kind.IMPLIES, this, r, () -> this.reify().imp(r).post()); + } else { + this.reify().imp(r).post(); + } } /** @@ -262,6 +283,15 @@ public final void implies(BoolVar r) { * @param r a boolean variable */ public final void impliedBy(BoolVar r) { + Recorder rec = recorder(); + if (rec != null) { + rec.link(Step.Link.Kind.IMPLIED_BY, this, r, () -> doImpliedBy(r)); + } else { + doImpliedBy(r); + } + } + + private void doImpliedBy(BoolVar r) { if (boolReif == null) { boolReif = r; if (boolReif.isInstantiatedTo(1) @@ -275,6 +305,15 @@ public final void impliedBy(BoolVar r) { } } + /** + * @return the recorder of the model of this constraint if the current operation must be journalized (the model + * is recorded and the operation is not triggered by another journalized one), null otherwise + */ + private Recorder recorder() { + Recorder r = propagators.length > 0 ? propagators[0].getModel().getRecorder() : null; + return r == null || r.busy() ? null : r; + } + /** * Posts the constraint to its model so that the constraint must be satisfied. * This should not be reified. diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/IConstraintFactory.java b/solver/src/main/java/org/chocosolver/solver/constraints/IConstraintFactory.java index 87c9da500e..b589032fb5 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/IConstraintFactory.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/IConstraintFactory.java @@ -9,6 +9,7 @@ import org.chocosolver.solver.constraints.reification.PropConditional; import org.chocosolver.solver.variables.Variable; +import java.util.function.BiFunction; import java.util.function.Function; import java.util.function.Supplier; @@ -45,4 +46,45 @@ default Constraint conditional( new PropConditional(scope, checker, provider) ); } + + /** + * Create a custom constraint, made of the propagator built by {@code propagator} on {@code vars}. + *

+ * Prefer this factory to {@code new Constraint(name, propagator)}: a model created with + * {@link org.chocosolver.solver.Model#record()} can then be duplicated, provided that {@code propagator} captures + * nothing (e.g., a constructor reference such as {@code PropFoo::new}), since it is shared by all the copies. + * + * @param name name of the constraint + * @param vars variables of the constraint + * @param propagator builds the propagator from the variables; must capture nothing + * @param type of the variables + * @return a custom constraint + */ + default Constraint custom(String name, V[] vars, Function> propagator) { + return new Constraint(name, propagator.apply(vars)); + } + + /** + * Create a custom constraint, made of the propagator built by {@code propagator} on {@code vars} and + * {@code data}, e.g. {@code custom("atMostK", x, 3, PropAtMostK::new)}. + *

+ * Prefer this factory to {@code new Constraint(name, propagator)}: a model created with + * {@link org.chocosolver.solver.Model#record()} can then be duplicated, provided that {@code propagator} captures + * nothing (e.g., a constructor reference such as {@code PropFoo::new}), since it is shared by all the copies. + * What the propagator needs, besides the variables, is passed in {@code data}, which is journalized as any + * constant argument: immutable values and arrays of them, tuples, or a {@code record} of such values (several + * parameters). An array of variables is mapped to the variables of each copy. + * + * @param name name of the constraint + * @param vars variables of the constraint + * @param data the other parameters of the propagator + * @param propagator builds the propagator from the variables and the data; must capture nothing + * @param type of the variables + * @param type of the data + * @return a custom constraint + */ + default Constraint custom(String name, V[] vars, D data, + BiFunction> propagator) { + return new Constraint(name, propagator.apply(vars, data)); + } } diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/extension/Tuples.java b/solver/src/main/java/org/chocosolver/solver/constraints/extension/Tuples.java index 617968f8e2..9b03f82c83 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/extension/Tuples.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/extension/Tuples.java @@ -34,6 +34,10 @@ public class Tuples { private final boolean allowStar; private final int star; private SoftReference cachedMatrix; + /** + * Once frozen, the tuples cannot be modified anymore and can be safely shared among models. + */ + private volatile boolean frozen; //*********************************************************************************** // CONSTRUCTOR @@ -155,6 +159,7 @@ public ESat check(IntVar... vars) { * @throws org.chocosolver.solver.exception.SolverException if the size of the tuple added does not correspond to a the previous ones (if any). */ public void add(int... tuple) { + checkNotFrozen(); if (tuples.isEmpty()) { arity = tuple.length; ranges = new int[2 * arity]; @@ -244,21 +249,52 @@ public String toString() { * @return an array of tuples, each tuple is an int array */ public int[][] toMatrix() { - if (cachedMatrix == null) { + // the cache may have been cleared by the GC, or be computed concurrently when the tuples are shared + SoftReference ref = cachedMatrix; + int[][] matrix = ref == null ? null : ref.get(); + if (matrix == null) { int i = 0; - int[][] matrix = new int[tuples.size()][]; + matrix = new int[tuples.size()][]; for (int[] tuple : tuples) { matrix[i++] = tuple.clone(); } cachedMatrix = new SoftReference<>(matrix); } - return cachedMatrix.get(); + return matrix; } public void sort() { + checkNotFrozen(); tuples.sort(new TupleComparator()); } + /** + * Freeze this set of tuples: any further modification ({@link #add(int...)}, {@link #sort()}) will throw a + * {@link SolverException}. + * A frozen set of tuples can be safely shared among models solved concurrently. + * Freezing is irreversible and idempotent. + * + * @return this + */ + public Tuples freeze() { + this.frozen = true; + return this; + } + + /** + * @return true if this set of tuples is frozen, false otherwise + * @see #freeze() + */ + public boolean isFrozen() { + return frozen; + } + + private void checkNotFrozen() { + if (frozen) { + throw new SolverException("Cannot modify a frozen set of tuples"); + } + } + private static class TupleComparator implements Comparator { @Override diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/extension/hybrid/HybridTuples.java b/solver/src/main/java/org/chocosolver/solver/constraints/extension/hybrid/HybridTuples.java index 321f143387..4c067bb716 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/extension/hybrid/HybridTuples.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/extension/hybrid/HybridTuples.java @@ -50,6 +50,10 @@ public class HybridTuples { * For sanity check only */ private int arity; + /** + * Once frozen, the tuples cannot be modified anymore and can be safely shared among models. + */ + private volatile boolean frozen; /** * Create an empty structure that stores hybrid tuples @@ -68,6 +72,9 @@ public HybridTuples() { * @throws SolverException if the tuple does not the match the arity of previously declared ones. */ public void add(ISupportable... tuple) { + if (frozen) { + throw new SolverException("Cannot modify frozen hybrid tuples"); + } if (hybridTuples.size() == 0) { arity = tuple.length; } else if (arity != tuple.length) { @@ -133,6 +140,26 @@ public void add(ISupportable[]... tuples) { } } + /** + * Freeze these hybrid tuples: any further modification will throw a {@link SolverException}. + * Frozen hybrid tuples can be safely shared among models solved concurrently. + * Freezing is irreversible and idempotent. + * + * @return this + */ + public HybridTuples freeze() { + this.frozen = true; + return this; + } + + /** + * @return true if these hybrid tuples are frozen + * @see #freeze() + */ + public boolean isFrozen() { + return frozen; + } + /** * @return the current tuples as an array of expressions. */ diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/nary/automata/FA/FiniteAutomaton.java b/solver/src/main/java/org/chocosolver/solver/constraints/nary/automata/FA/FiniteAutomaton.java index 8c79805933..84d14c5458 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/nary/automata/FA/FiniteAutomaton.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/nary/automata/FA/FiniteAutomaton.java @@ -37,7 +37,7 @@ public class FiniteAutomaton implements IAutomaton { private ArrayList states; private TIntHashSet alphabet; private int nbStates; - private final HashSet nexts = new HashSet<>(); + private HashSet nexts = new HashSet<>(); private int min = Character.MIN_VALUE; private int max = Character.MAX_VALUE; @@ -595,6 +595,8 @@ public ArrayList _removeSymbolFromAutomaton(int alpha) { public FiniteAutomaton clone() throws CloneNotSupportedException { FiniteAutomaton auto = (FiniteAutomaton) super.clone(); + // working buffer of delta(int, int, TIntHashSet): must not be shared with the clone + auto.nexts = new HashSet<>(); auto.representedBy = new Automaton(); auto.states = new ArrayList<>(); auto.stateToIndex = new TObjectIntHashMap<>(); @@ -613,6 +615,7 @@ public FiniteAutomaton clone() throws CloneNotSupportedException { for (int[] t : transitions) { auto.addTransition(t[0], t[1], t[2]); } + auto.representedBy.setDeterministic(this.representedBy.isDeterministic()); return auto; } diff --git a/solver/src/main/java/org/chocosolver/solver/spec/AbstractRecordingModel.java b/solver/src/main/java/org/chocosolver/solver/spec/AbstractRecordingModel.java new file mode 100644 index 0000000000..941d51f263 --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/spec/AbstractRecordingModel.java @@ -0,0 +1,211 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.IModel; +import org.chocosolver.solver.Model; +import org.chocosolver.solver.Settings; +import org.chocosolver.solver.SettingsBuilder; +import org.chocosolver.solver.constraints.Constraint; +import org.chocosolver.solver.constraints.nary.cnf.SatConstraint; +import org.chocosolver.solver.constraints.real.IbexHandler; +import org.chocosolver.solver.exception.SolverException; +import org.chocosolver.solver.variables.Group; +import org.chocosolver.solver.variables.Variable; + +import java.util.Set; + +/** + * The hand-written part of {@link RecordingModel}: journalization of the operations of {@link Model} which are + * not factory methods. + *

+ * {@link RecordingModel}, which journalizes the factory methods, is generated at compile time. + * + * @author Charles Prud'homme + */ +@GenerateRecordingModel(name = "RecordingModel", factories = IModel.class, + excluded = {"checkIntDomainRange", "checkRealDomainRange", "toBoolVar", "getDomainUnion"}) +public abstract class AbstractRecordingModel extends Model { + + /** + * Hooks managed internally by the solver: never journalized. + */ + private static final Set INTERNAL_HOOKS = Set.of("cinstances", + MINISAT_HOOK_NAME, IBEX_HOOK_NAME, TASK_SET_HOOK_NAME); + + private final Recorder recorder; + + protected AbstractRecordingModel(String name, Settings settings) { + super(name, settings); + this.recorder = new Recorder(this, new Header(name, settings, getSeed())); + } + + protected AbstractRecordingModel(String name) { + this(name, SettingsBuilder.init().build()); + } + + protected AbstractRecordingModel(Settings settings) { + this("RecordingModel", settings); + } + + protected AbstractRecordingModel() { + this("RecordingModel"); + } + + /** + * @return the recorder of this model + */ + @Override + public final Recorder getRecorder() { + return recorder; + } + + /** + * @return the spec of the model built so far + * @throws SpecException if some operations could not be journalized, or if the resolution has started + * @see Recorder#snapshot() + */ + public final ModelSpec snapshot() { + return recorder.snapshot(); + } + + @Override + public final Model duplicate() { + return snapshot().instantiate().model(); + } + + /** + * @return true if the operation must be journalized + */ + protected final boolean topLevel() { + // null while the constructor of Model runs + return recorder != null && !recorder.busy(); + } + + @Override + public void post(Constraint... cs) throws SolverException { + if (topLevel()) { + recorder.post(cs, () -> super.post(cs)); + } else { + super.post(cs); + } + } + + @Override + public void unpost(Constraint... constraints) throws SolverException { + if (topLevel()) { + recorder.unpost(constraints, () -> super.unpost(constraints)); + } else { + super.unpost(constraints); + } + } + + @Override + public void addHook(String hookName, Object hookObject) { + if (topLevel() && !INTERNAL_HOOKS.contains(hookName)) { + recorder.hook(hookName, hookObject, () -> super.addHook(hookName, hookObject)); + } else { + super.addHook(hookName, hookObject); + } + } + + @Override + public void removeHook(String hookName) { + if (topLevel() && !INTERNAL_HOOKS.contains(hookName)) { + recorder.hook(hookName, null, () -> super.removeHook(hookName)); + } else { + super.removeHook(hookName); + } + } + + @Override + public void removeAllHooks() { + if (topLevel()) { + recorder.removeAllHooks(super::removeAllHooks); + } else { + super.removeAllHooks(); + } + } + + @Override + public void setName(String name) { + if (topLevel()) { + recorder.name(name, () -> super.setName(name)); + } else { + super.setName(name); + } + } + + @Override + public void addGroup(Group g) { + if (topLevel()) { + recorder.group(g.getName(), g.getVariables(), () -> super.addGroup(g)); + } else { + super.addGroup(g); + } + } + + @Override + public void setPrecision(double p) { + if (topLevel()) { + recorder.unsupported("setPrecision", "real variables are not supported"); + } + super.setPrecision(p); + } + + @Override + public void setSeed(long seed) { + if (topLevel()) { + recorder.seed(seed, () -> super.setSeed(seed)); + } else { + super.setSeed(seed); + } + } + + @Override + public void setObjective(boolean maximize, Variable objective) { + if (topLevel()) { + recorder.objective(maximize, objective, () -> super.setObjective(maximize, objective)); + } else { + super.setObjective(maximize, objective); + } + } + + @Override + public void clearObjective() { + if (topLevel()) { + recorder.objective(false, null, super::clearObjective); + } else { + super.clearObjective(); + } + } + + // The following methods are not factories: what they do internally must not be journalized. + // Their effects are replayed by the factories which need them. + + @Override + public SatConstraint getMinisat() { + // also called by search monitors (nogoods), which are not part of the model: never journalized + return topLevel() ? recorder.silently(super::getMinisat) : super.getMinisat(); + } + + @Override + public void removeMinisat() { + if (topLevel()) { + recorder.unsupported("removeMinisat", "not supported"); + } + super.removeMinisat(); + } + + @Override + public IbexHandler getIbexHandler() { + if (topLevel()) { + recorder.unsupported("getIbexHandler", "real constraints are not supported"); + } + return super.getIbexHandler(); + } +} diff --git a/solver/src/main/java/org/chocosolver/solver/spec/Arg.java b/solver/src/main/java/org/chocosolver/solver/spec/Arg.java new file mode 100644 index 0000000000..2bbec32b67 --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/spec/Arg.java @@ -0,0 +1,242 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.constraints.nary.cnf.LogOp; +import org.chocosolver.solver.variables.BoolVar; + +import java.util.Arrays; +import java.util.Objects; +import java.util.function.IntConsumer; + +/** + * An argument of a {@link Step.Call}. + * Objects of the model (variables, constraints, tasks) are referred to by identifier, never by name. + *

+ * Arguments are immutable: public accessors return copies, the package reads the arrays directly. + * + * @author Charles Prud'homme + */ +public sealed interface Arg permits Arg.Ref, Arg.RefArray, Arg.RefMatrix, Arg.RefList, Arg.Const, Arg.Logic, + Arg.Literal { + + /** + * Apply action on each identifier this argument refers to. + */ + default void forEachRef(IntConsumer action) { + } + + /** + * A reference to one object of the model. + */ + record Ref(int id) implements Arg { + public Ref { + if (id < 0) throw new SpecException("Negative identifier: " + id); + } + + @Override + public void forEachRef(IntConsumer action) { + action.accept(id); + } + } + + /** + * An array of objects of the model, e.g. an {@code IntVar[]}. + * + * @param componentType type of the elements of the array to build, e.g. {@code IntVar.class} + * @param ids identifiers of the elements + */ + record RefArray(Class componentType, int[] ids) implements Arg { + public RefArray { + Objects.requireNonNull(componentType); + ids = ids.clone(); + } + + @Override + public int[] ids() { + return ids.clone(); + } + + int[] rawIds() { + return ids; + } + + @Override + public void forEachRef(IntConsumer action) { + for (int id : ids) action.accept(id); + } + + @Override + public String toString() { + return componentType.getSimpleName() + Arrays.toString(ids); + } + } + + /** + * A matrix of objects of the model, e.g. an {@code IntVar[][]}. + * + * @param componentType type of the elements of the matrix to build, e.g. {@code IntVar.class} + * @param ids identifiers of the elements, row by row + */ + record RefMatrix(Class componentType, int[][] ids) implements Arg { + public RefMatrix { + Objects.requireNonNull(componentType); + ids = (int[][]) Values.capture(ids); + } + + @Override + public int[][] ids() { + return (int[][]) Values.materialize(ids); + } + + int[][] rawIds() { + return ids; + } + + @Override + public void forEachRef(IntConsumer action) { + for (int[] row : ids) for (int id : row) action.accept(id); + } + + @Override + public String toString() { + return componentType.getSimpleName() + Arrays.deepToString(ids); + } + } + + /** + * A {@link java.util.List} of objects of the model. + */ + record RefList(int[] ids) implements Arg { + public RefList { + ids = ids.clone(); + } + + @Override + public int[] ids() { + return ids.clone(); + } + + int[] rawIds() { + return ids; + } + + @Override + public void forEachRef(IntConsumer action) { + for (int id : ids) action.accept(id); + } + + @Override + public String toString() { + return "List" + Arrays.toString(ids); + } + } + + /** + * A constant, captured according to the sharing policy of {@link Values}. + */ + record Const(Object value) implements Arg { + public Const { + value = Values.capture(value); + } + + /** + * @return the value, shared or copied according to the sharing policy of {@link Values} + */ + @Override + public Object value() { + return Values.materialize(value); + } + + /** + * @return the captured value, as stored in the spec (not to be modified) + */ + Object rawValue() { + return value; + } + + @Override + public String toString() { + if (value instanceof int[] a) return Arrays.toString(a); + if (value instanceof Object[] a) return Arrays.deepToString(a); + return String.valueOf(value); + } + } + + /** + * A logical tree ({@link LogOp}) over boolean variables. + * + * @param and true for a conjunction, false for a disjunction + * @param negated true for the negation of the conjunction (resp. disjunction) + * @param children either references to {@link BoolVar} or nested {@link Logic} + */ + record Logic(boolean and, boolean negated, Arg[] children) implements Arg { + public Logic { + children = children.clone(); + for (Arg c : children) { + if (!(c instanceof Ref) && !(c instanceof Logic)) { + throw new SpecException("A logical tree only accepts references and logical trees, not " + c); + } + } + } + + @Override + public Arg[] children() { + return children.clone(); + } + + Arg[] rawChildren() { + return children; + } + + @Override + public void forEachRef(IntConsumer action) { + for (Arg c : children) c.forEachRef(action); + } + + @Override + public String toString() { + return (negated ? "n" : "") + (and ? "and" : "or") + Arrays.toString(children); + } + } + + /** + * A {@link org.chocosolver.sat.Literalizer}, which binds a variable to a literal of the SAT solver. + * Literalizers are mutable (the SAT solver numbers them): a new one is built for each instance. + * + * @param kind the kind of literalizer + * @param var identifier of the variable + * @param value the value (for {@link Kind#INT_EQ} and {@link Kind#INT_LE} only) + */ + record Literal(Kind kind, int var, int value) implements Arg { + + /** + * The kinds of literalizers: {@code BoolLit}, {@code IntEqLit} and {@code IntLeLit}. + */ + public enum Kind { + BOOL, INT_EQ, INT_LE + } + + public Literal { + Objects.requireNonNull(kind); + if (var < 0) throw new SpecException("Negative identifier: " + var); + } + + @Override + public void forEachRef(IntConsumer action) { + action.accept(var); + } + } + + static Logic and(Arg... children) { + return new Logic(true, false, children); + } + + static Logic or(Arg... children) { + return new Logic(false, false, children); + } +} diff --git a/solver/src/main/java/org/chocosolver/solver/spec/FactoryMethod.java b/solver/src/main/java/org/chocosolver/solver/spec/FactoryMethod.java new file mode 100644 index 0000000000..ef9f4df4cf --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/spec/FactoryMethod.java @@ -0,0 +1,123 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.IModel; +import org.chocosolver.solver.Model; + +import java.lang.invoke.MethodHandle; +import java.lang.invoke.MethodHandles; +import java.lang.invoke.MethodType; +import java.lang.reflect.Method; +import java.lang.reflect.Modifier; +import java.util.Arrays; +import java.util.concurrent.ConcurrentHashMap; +import java.util.stream.Collectors; + +/** + * A factory method of {@link IModel}, identified by its exact signature (the overload is never ambiguous). + * It is replayed on a {@link Model} through a {@link MethodHandle}. + *

+ * Instances are immutable and can be shared among threads. + * + * @author Charles Prud'homme + */ +public final class FactoryMethod { + + private static final ConcurrentHashMap CACHE = new ConcurrentHashMap<>(); + + private final Method method; + private final Class[] types; + /** + * (Model, Object[]) -> Object: the arguments are spread, the result boxed (null for void). + */ + private final MethodHandle invoker; + + private FactoryMethod(Method method) { + if (Modifier.isStatic(method.getModifiers()) + || !method.getDeclaringClass().isInterface() + || !method.getDeclaringClass().isAssignableFrom(IModel.class)) { + throw new SpecException(method + " is not a factory method of IModel"); + } + this.method = method; + this.types = method.getParameterTypes(); + try { + // fixed arity: a varargs parameter receives the array built from the spec, as is + this.invoker = MethodHandles.publicLookup().unreflect(method).asFixedArity() + .asSpreader(Object[].class, types.length) + .asType(MethodType.methodType(Object.class, Model.class, Object[].class)); + } catch (IllegalAccessException e) { + throw new SpecException("Cannot access " + method, e); + } + } + + /** + * @param method a (non-static) method declared by one of the factory interfaces of {@link IModel} + * @return the corresponding factory method + * @throws SpecException if method is not a factory method + */ + public static FactoryMethod of(Method method) { + return CACHE.computeIfAbsent(method, FactoryMethod::new); + } + + /** + * @param name name of the factory method + * @param paramTypes exact parameter types, which select the overload + * @return the corresponding factory method + * @throws SpecException if no such factory method exists + */ + public static FactoryMethod of(String name, Class... paramTypes) { + try { + return of(IModel.class.getMethod(name, paramTypes)); + } catch (NoSuchMethodException e) { + throw new SpecException("No factory method " + signature(name, paramTypes), e); + } + } + + public String name() { + return method.getName(); + } + + public Class[] parameterTypes() { + return types.clone(); + } + + Class[] rawParameterTypes() { + return types; + } + + public int parameterCount() { + return types.length; + } + + public Class returnType() { + return method.getReturnType(); + } + + Object invoke(Model target, Object[] args) throws Throwable { + return (Object) invoker.invokeExact(target, args); + } + + private static String signature(String name, Class[] types) { + return name + Arrays.stream(types).map(Class::getSimpleName).collect(Collectors.joining(", ", "(", ")")); + } + + @Override + public boolean equals(Object o) { + return this == o || (o instanceof FactoryMethod f && method.equals(f.method)); + } + + @Override + public int hashCode() { + return method.hashCode(); + } + + @Override + public String toString() { + return signature(method.getName(), types); + } +} diff --git a/solver/src/main/java/org/chocosolver/solver/spec/GenerateRecordingModel.java b/solver/src/main/java/org/chocosolver/solver/spec/GenerateRecordingModel.java new file mode 100644 index 0000000000..a54c7a3e02 --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/spec/GenerateRecordingModel.java @@ -0,0 +1,38 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +/** + * Asks the annotation processor {@code org.chocosolver.codegen.RecordingModelProcessor} (module choco-codegen) to + * generate, at compile time, a subclass of the annotated class which journalizes every factory method. + * + * @author Charles Prud'homme + */ +@Retention(RetentionPolicy.SOURCE) +@Target(ElementType.TYPE) +@interface GenerateRecordingModel { + + /** + * @return the simple name of the generated class, in the package of the annotated class + */ + String name(); + + /** + * @return the interface whose default methods are the factory methods to journalize + */ + Class factories(); + + /** + * @return names of the factory methods without effect on the model, which are not journalized + */ + String[] excluded() default {}; +} diff --git a/solver/src/main/java/org/chocosolver/solver/spec/Header.java b/solver/src/main/java/org/chocosolver/solver/spec/Header.java new file mode 100644 index 0000000000..a35ae3119c --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/spec/Header.java @@ -0,0 +1,56 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.Settings; +import org.chocosolver.solver.SettingsBuilder; + +import java.util.Objects; + +/** + * What must be set on a model before replaying the steps of a {@link ModelSpec}. + * + * @param name name of the model + * @param settings settings of the model; immutable, hence shared by all instances, which may call its functions + * ({@code modelChecker}, {@code defaultSearch}, {@code environmentSupplier}...) concurrently: they + * must be stateless + * @param seed seed of the model; some propagators draw their random numbers from it when created + * @author Charles Prud'homme + */ +public record Header(String name, Settings settings, long seed) { + + public Header { + Objects.requireNonNull(name); + Objects.requireNonNull(settings); + } + + /** + * @return a header with default settings and seed 0 + */ + public static Header of(String name) { + return of(name, SettingsBuilder.init().build()); + } + + /** + * @return a header with seed 0 + */ + public static Header of(String name, Settings settings) { + return new Header(name, settings, 0L); + } + + public Header withName(String name) { + return new Header(name, settings, seed); + } + + public Header withSeed(long seed) { + return new Header(name, settings, seed); + } + + public Header withSettings(Settings settings) { + return new Header(name, settings, seed); + } +} diff --git a/solver/src/main/java/org/chocosolver/solver/spec/IdTable.java b/solver/src/main/java/org/chocosolver/solver/spec/IdTable.java new file mode 100644 index 0000000000..2bd60d332b --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/spec/IdTable.java @@ -0,0 +1,82 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.Model; + +import java.util.Arrays; +import java.util.IdentityHashMap; + +/** + * The mapping from identifiers to the objects of a model, shared by {@link Recorder} and {@link Replayer}. + * The reverse mapping ({@link #idOf(Object)}) is built on demand. + * + * @author Charles Prud'homme + */ +abstract class IdTable implements Resolver { + + private final Model model; + private Object[] objects = new Object[64]; + private int capacity; + private IdentityHashMap reverse; + + IdTable(Model model) { + this.model = model; + } + + /** + * Bind id to o. + * + * @return the object previously bound to id, or null + */ + final Object put(int id, Object o) { + if (id >= objects.length) { + objects = Arrays.copyOf(objects, Math.max(id + 1, objects.length * 2)); + } + Object prev = objects[id]; + objects[id] = o; + capacity = Math.max(capacity, id + 1); + reverse = null; + return prev; + } + + @Override + public final Model model() { + return model; + } + + @Override + public final Object get(int id) { + if (!isBound(id)) { + throw new SpecException("Unbound identifier " + id); + } + return objects[id]; + } + + @Override + public final int capacity() { + return capacity; + } + + @Override + public final boolean isBound(int id) { + return id >= 0 && id < capacity && objects[id] != null; + } + + @Override + public int idOf(Object o) { + if (reverse == null) { + reverse = new IdentityHashMap<>(); + for (int id = 0; id < capacity; id++) { + if (objects[id] != null) { + reverse.putIfAbsent(objects[id], id); + } + } + } + return reverse.getOrDefault(o, -1); + } +} diff --git a/solver/src/main/java/org/chocosolver/solver/spec/ModelSpec.java b/solver/src/main/java/org/chocosolver/solver/spec/ModelSpec.java new file mode 100644 index 0000000000..d424bdb96b --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/spec/ModelSpec.java @@ -0,0 +1,135 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.Model; +import org.chocosolver.solver.Settings; + +import java.util.BitSet; +import java.util.List; +import java.util.Objects; +import java.util.function.Consumer; + +/** + * An immutable description of a model: a {@link Header} and an ordered journal of {@link Step}s. + *

+ * Each call to {@link #instantiate()} builds a new, independent {@link Model}. Distinct instances can be built and + * solved concurrently, in distinct threads: they only share immutable data (settings, frozen tuples, ...). + *

+ * Replaying the same spec twice produces two models with identical structure (same variables, same constraints, + * in the same order), hence identical search when the search is deterministic. + * + * @param header what must be set on a model before replaying the steps + * @param steps the steps, replayed in order + * @param search the search, applied once the steps are replayed; null for the default search + * @author Charles Prud'homme + */ +public record ModelSpec(Header header, List steps, SearchDecl search) { + + /** + * @param header what must be set on a model before replaying the steps + * @param steps the steps, replayed in order + * @param search the search, applied once the steps are replayed; null for the default search + */ + public ModelSpec { + Objects.requireNonNull(header); + steps = List.copyOf(steps); + checkIdentifiers(steps); + } + + /** + * A spec with the default search. + */ + public ModelSpec(Header header, List steps) { + this(header, steps, null); + } + + /** + * @return this spec with another search + */ + public ModelSpec withSearch(SearchDecl search) { + return new ModelSpec(header, steps, search); + } + + /** + * @return this spec with another header + */ + public ModelSpec withHeader(Header header) { + return new ModelSpec(header, steps, search); + } + + /** + * @return this spec with other steps + */ + public ModelSpec withSteps(List steps) { + return new ModelSpec(header, steps, search); + } + + /** + * @return the spec rewritten by variant + */ + public ModelSpec with(Variant variant) { + return variant.apply(this); + } + + /** + * Build a new model from a variant of this spec. When several models are built from the same variant, prefer + * {@code with(variant)} once, then {@link #instantiate()} on the result. + * + * @return the mapping from the identifiers to the objects of the new model ({@link Resolver#model()}) + */ + public Resolver instantiate(Variant variant) { + return with(variant).instantiate(); + } + + /** + * Record the construction of a model. + * + * @param name name of the model + * @param settings settings of the model + * @param builder builds the model + * @return the spec of the model + * @throws SpecException if some operations could not be journalized + * @see RecordingModel + */ + public static ModelSpec record(String name, Settings settings, Consumer builder) { + RecordingModel model = new RecordingModel(name, settings); + builder.accept(model); + return model.snapshot(); + } + + /** + * Build a new model from this spec. + * + * @return the mapping from the identifiers to the objects of the new model ({@link Resolver#model()}) + * @throws SpecException if a step cannot be replayed + */ + public Resolver instantiate() { + Resolver resolver = new Replayer(header).replay(steps); + if (search != null) { + search.configure(resolver); + } + return resolver; + } + + /** + * Check that each identifier is defined before being used. + */ + private static void checkIdentifiers(List steps) { + BitSet defined = new BitSet(); + for (int i = 0; i < steps.size(); i++) { + Step step = steps.get(i); + final int s = i; + step.forEachUse(id -> { + if (!defined.get(id)) { + throw new SpecException("Step #" + s + " (" + step + ") uses undefined identifier " + id); + } + }); + step.forEachDef(defined::set); + } + } +} diff --git a/solver/src/main/java/org/chocosolver/solver/spec/Recorder.java b/solver/src/main/java/org/chocosolver/solver/spec/Recorder.java new file mode 100644 index 0000000000..f6f208eb6d --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/spec/Recorder.java @@ -0,0 +1,516 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.sat.Literalizer; +import org.chocosolver.solver.Model; +import org.chocosolver.solver.constraints.Constraint; +import org.chocosolver.solver.constraints.nary.cnf.ILogical; +import org.chocosolver.solver.constraints.nary.cnf.LogOp; +import org.chocosolver.solver.search.SearchState; +import org.chocosolver.solver.variables.BoolVar; +import org.chocosolver.solver.variables.IntVar; +import org.chocosolver.solver.variables.Task; +import org.chocosolver.solver.variables.Variable; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.IdentityHashMap; +import java.util.List; +import java.util.function.Supplier; + +/** + * Journalizes the construction of a {@link RecordingModel} into a {@link ModelSpec}. + *

+ * Only top-level operations are journalized: a depth counter ensures that the operations triggered internally by a + * factory (decompositions, intermediate variables, internal posts...) are not, since replaying the top-level + * operation replays them too. + *

+ * An operation that cannot be journalized (unknown object, unsupported argument...) does not interrupt the + * construction of the model: it is reported, and {@link #snapshot()} fails. + *

+ * The recorder is also the {@link Resolver} of the recorded model: identifiers of the spec map to its objects. + *

+ * Not thread-safe: a model is built by a single thread. + * + * @author Charles Prud'homme + */ +public final class Recorder extends IdTable { + + /** + * An operation which could not be journalized. + * + * @param step index of the step at which the operation occurred + * @param operation the operation + * @param reason why it could not be journalized + */ + public record Unsupported(int step, String operation, String reason) { + @Override + public String toString() { + return "#" + step + " " + operation + ": " + reason; + } + } + + /** + * Thrown when an argument cannot be captured. + */ + private static final class Uncapturable extends Exception { + Uncapturable(String message) { + super(message, null, false, false); + } + } + + private static final FactoryMethod INT_CONSTANT = FactoryMethod.of("intVar", int.class); + private static final FactoryMethod BOOL_NOT_VIEW = FactoryMethod.of("boolNotView", BoolVar.class); + + private Header header; + private final List steps = new ArrayList<>(); + private final List unsupported = new ArrayList<>(); + /** + * Reverse mapping, maintained eagerly: it is queried for each argument recorded. + */ + private final IdentityHashMap ids = new IdentityHashMap<>(); + private int depth; + + Recorder(Model model, Header header) { + super(model); + this.header = header; + } + + /** + * @return true when an operation is being journalized: nested operations must not be journalized + */ + public boolean busy() { + return depth > 0; + } + + /** + * @return the operations which could not be journalized so far + */ + public List unsupported() { + return Collections.unmodifiableList(unsupported); + } + + /** + * @param o an object of the model + * @return the identifier of o in the spec, or -1 if o is unknown + */ + @Override + public int idOf(Object o) { + return ids.getOrDefault(o, -1); + } + + /** + * @param vars variables of the recorded model + * @return their identifiers in the spec, e.g. to declare a {@link SearchDecl} + * @throws SpecException if a variable is unknown + */ + public int[] idsOf(Variable... vars) { + int[] r = new int[vars.length]; + for (int i = 0; i < vars.length; i++) { + r[i] = idOf(vars[i]); + if (r[i] < 0) { + throw new SpecException("Unknown variable " + vars[i].getName()); + } + } + return r; + } + + /** + * @return the spec of the model built so far + * @throws SpecException if some operations could not be journalized, or if the resolution has started + */ + public ModelSpec snapshot() { + if (model().getSolver().getSearchState() != SearchState.NEW) { + throw new SpecException("Cannot snapshot a model whose resolution has started"); + } + if (!unsupported.isEmpty()) { + StringBuilder sb = new StringBuilder(); + sb.append(unsupported.size()).append(" operation(s) cannot be journalized:"); + unsupported.stream().limit(10).forEach(u -> sb.append("\n\t").append(u)); + if (unsupported.size() > 10) { + sb.append("\n\t..."); + } + throw new SpecException(sb.toString()); + } + return new ModelSpec(header, steps); + } + + //*********************************************************************************** + // OPERATIONS + //*********************************************************************************** + + /** + * Journalize a call to a factory method. + * + * @param method the factory method + * @param body the actual call + * @param args the arguments of the call + * @return the result of the call + */ + R call(FactoryMethod method, Supplier body, Object[] args) { + Arg[] captured = new Arg[args.length]; + String failure = null; + try { + for (int i = 0; i < args.length; i++) { + captured[i] = capture(args[i]); + } + } catch (Uncapturable e) { + failure = e.getMessage(); + } + R result = nested(body); + int[] out = outputs(result); + if (failure == null) { + steps.add(new Step.Call(out, method, captured)); + } else { + unsupported(method.toString(), failure); + } + return result; + } + + /** + * Journalize a call to a factory method which returns nothing. + */ + void run(FactoryMethod method, Runnable body, Object[] args) { + call(method, () -> { + body.run(); + return null; + }, args); + } + + void post(Constraint[] cstrs, Runnable body) { + int[] cids = constraintIds("post", cstrs); + nested(body); + if (cids != null) { + steps.add(new Step.Post(cids)); + } + } + + void unpost(Constraint[] cstrs, Runnable body) { + int[] cids = constraintIds("unpost", cstrs); + nested(body); + if (cids != null) { + steps.add(new Step.Unpost(cids)); + } + } + + /** + * Journalize {@link Constraint#reify()}. + */ + public BoolVar reify(Constraint cstr, Supplier body) { + int cid = ref("reify", cstr); + BoolVar b = nested(body); + int out = idFor(b); + if (cid >= 0) { + steps.add(new Step.Reify(cid, out)); + } + return b; + } + + /** + * Journalize {@link Constraint#reifyWith}, {@link Constraint#implies} or {@link Constraint#impliedBy}. + */ + public void link(Step.Link.Kind kind, Constraint cstr, BoolVar bool, Runnable body) { + int[] r = refs(kind.name(), cstr, bool); + nested(body); + if (r != null) { + steps.add(new Step.Link(kind, r[0], r[1])); + } + } + + /** + * Journalize the creation of a task with its canonical constructor (the task is already built). + * + * @param performed the performed variable of an optional task, null for a mandatory task + */ + public void newTask(Task task, IntVar start, IntVar duration, IntVar end, BoolVar performed) { + if (busy()) { + return; + } + int[] r = performed == null + ? refs("new Task", start, duration, end) + : refs("new OptionalTask", start, duration, end, performed); + int out = idFor(task); + if (r != null) { + steps.add(new Step.NewTask(out, r[0], r[1], r[2], performed == null ? -1 : r[3])); + } + } + + void hook(String name, Object value, Runnable body) { + Arg captured = tryCapture("addHook(" + name + ")", value); + nested(body); + if (captured != null) { + steps.add(new Step.Hook(name, captured)); + } + } + + void removeAllHooks(Runnable body) { + nested(body); + steps.add(new Step.Hook(null, new Arg.Const(null))); + } + + void name(String name, Runnable body) { + nested(body); + header = header.withName(name); + } + + void group(String name, Variable[] vars, Runnable body) { + Arg captured = tryCapture("addGroup(" + name + ")", vars); + nested(body); + if (captured instanceof Arg.RefArray a) { + steps.add(new Step.Group(name, a)); + } else if (captured != null) { + unsupported("addGroup(" + name + ")", "not an array of variables"); + } + } + + void seed(long seed, Runnable body) { + nested(body); + steps.add(new Step.Seed(seed)); + } + + void objective(boolean maximize, Variable objective, Runnable body) { + int id = objective == null ? -1 : ref("setObjective", objective); + nested(body); + if (objective == null || id >= 0) { + steps.add(new Step.Objective(maximize, id)); + } + } + + /** + * Run body without journalizing what it does. + */ + R silently(Supplier body) { + return nested(body); + } + + void unsupported(String operation, String reason) { + unsupported.add(new Unsupported(steps.size(), operation, reason)); + } + + //*********************************************************************************** + // INTERNALS + //*********************************************************************************** + + private R nested(Supplier body) { + depth++; + try { + return body.get(); + } finally { + depth--; + } + } + + private void nested(Runnable body) { + nested(() -> { + body.run(); + return null; + }); + } + + /** + * @return the captured argument, or null (and the operation is reported) if it cannot be captured + */ + private Arg tryCapture(String operation, Object value) { + try { + return capture(value); + } catch (Uncapturable e) { + unsupported(operation, e.getMessage()); + return null; + } + } + + /** + * @return the identifier of o, or -1 (and the operation is reported) if o is unknown + */ + private int ref(String operation, Object o) { + try { + return refOf(o); + } catch (Uncapturable e) { + unsupported(operation, e.getMessage()); + return -1; + } + } + + /** + * @return the identifiers of objects, or null (and the operation is reported) if one is unknown + */ + private int[] refs(String operation, Object... objects) { + int[] r = new int[objects.length]; + for (int i = 0; i < objects.length; i++) { + r[i] = ref(operation, objects[i]); + if (r[i] < 0) { + return null; + } + } + return r; + } + + private int[] constraintIds(String operation, Constraint[] cstrs) { + return cstrs == null ? Specs.NO_INT : refs(operation, (Object[]) cstrs); + } + + private static boolean isModelType(Class c) { + return Variable.class.isAssignableFrom(c) || Constraint.class.isAssignableFrom(c) || Task.class.isAssignableFrom(c); + } + + private static boolean isModelObject(Object o) { + return o != null && isModelType(o.getClass()); + } + + private Arg capture(Object v) throws Uncapturable { + if (isModelObject(v)) { + return new Arg.Ref(refOf(v)); + } + if (v instanceof LogOp op) { + return logic(op); + } + if (v instanceof Literalizer.BoolLit l) { + return new Arg.Literal(Arg.Literal.Kind.BOOL, refOf(l.cpVar), 0); + } + if (v instanceof Literalizer.IntEqLit l) { + return new Arg.Literal(Arg.Literal.Kind.INT_EQ, refOf(l.cpVar), l.val); + } + if (v instanceof Literalizer.IntLeLit l) { + return new Arg.Literal(Arg.Literal.Kind.INT_LE, refOf(l.cpVar), l.val); + } + if (v instanceof List list) { + int[] lids = new int[list.size()]; + for (int i = 0; i < lids.length; i++) { + if (!isModelObject(list.get(i))) { + throw new Uncapturable("list of " + (list.get(i) == null ? "null" : list.get(i).getClass().getSimpleName())); + } + lids[i] = refOf(list.get(i)); + } + return new Arg.RefList(lids); + } + if (v != null && v.getClass().isArray()) { + Class ct = v.getClass().getComponentType(); + if (isModelType(ct)) { + return new Arg.RefArray(ct, refsOf((Object[]) v)); + } + if (ct.isArray() && isModelType(ct.getComponentType())) { + Object[][] m = (Object[][]) v; + int[][] mids = new int[m.length][]; + for (int i = 0; i < m.length; i++) { + mids[i] = refsOf(m[i]); + } + return new Arg.RefMatrix(ct.getComponentType(), mids); + } + } + try { + return new Arg.Const(v); + } catch (SpecException e) { + throw new Uncapturable(e.getMessage()); + } + } + + private Arg.Logic logic(LogOp op) throws Uncapturable { + ILogical[] children = op.getChildren(); + Arg[] args = new Arg[children.length]; + for (int i = 0; i < children.length; i++) { + if (children[i] instanceof LogOp sub) { + args[i] = logic(sub); + } else if (children[i] instanceof BoolVar) { + args[i] = new Arg.Ref(refOf(children[i])); + } else { + throw new Uncapturable("logical tree with a " + children[i].getClass().getSimpleName()); + } + } + return new Arg.Logic(op.is(LogOp.Operator.AND), op.isNot(), args); + } + + private int[] refsOf(Object[] objects) throws Uncapturable { + if (objects == null) { + throw new Uncapturable("null array"); + } + int[] r = new int[objects.length]; + for (int i = 0; i < objects.length; i++) { + r[i] = refOf(objects[i]); + } + return r; + } + + /** + * @return the identifier of o; an unknown object is derived, when possible, from known objects + * (cached constant, negation of a known boolean variable) + */ + private int refOf(Object o) throws Uncapturable { + if (o == null) { + throw new Uncapturable("null object"); + } + Integer id = ids.get(o); + if (id != null) { + return id; + } + if (o instanceof Variable v) { + if (v.getModel() != model()) { + throw new Uncapturable("variable " + v.getName() + " belongs to another model"); + } + if (v instanceof IntVar iv && v.isAConstant()) { + int value = iv.getValue(); + if (model().getCachedConstants().get(value) == v) { + return derive(INT_CONSTANT, v, new Arg.Const(value)); + } + } + if (v instanceof BoolVar b && b.hasNot()) { + Integer nid = ids.get(b.not()); + if (nid != null) { + return derive(BOOL_NOT_VIEW, v, new Arg.Ref(nid)); + } + } + throw new Uncapturable("unknown variable " + v.getName() + + " (created outside of the factories, or internally by a factory)"); + } + if (o instanceof Constraint c) { + throw new Uncapturable("unknown constraint " + c.getName() + + " (custom constraint not built with Model.custom(...), or created internally by a factory)"); + } + throw new Uncapturable("unknown " + o.getClass().getSimpleName()); + } + + /** + * Journalize a call which returns the already existing object o (e.g., a cached constant). + */ + private int derive(FactoryMethod method, Object o, Arg arg) { + int id = idFor(o); + steps.add(new Step.Call(new int[]{id}, method, new Arg[]{arg})); + return id; + } + + /** + * @return the identifier of o, a new one if o is unknown + */ + private int idFor(Object o) { + Integer id = ids.get(o); + if (id == null) { + id = capacity(); + ids.put(o, id); + put(id, o); + } + return id; + } + + /** + * @return the identifiers of the model objects returned by a call (flattened for arrays) + */ + private int[] outputs(Object result) { + if (isModelObject(result)) { + return new int[]{idFor(result)}; + } + if (result instanceof Object[] array && isModelType(Specs.elementType(array.getClass()))) { + List flat = new ArrayList<>(); + Specs.flatten(array, flat); + int[] out = new int[flat.size()]; + for (int i = 0; i < out.length; i++) { + out[i] = flat.get(i) == null ? -1 : idFor(flat.get(i)); + } + return out; + } + return Specs.NO_INT; + } +} diff --git a/solver/src/main/java/org/chocosolver/solver/spec/Replayer.java b/solver/src/main/java/org/chocosolver/solver/spec/Replayer.java new file mode 100644 index 0000000000..bd7c66c2ec --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/spec/Replayer.java @@ -0,0 +1,215 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.sat.Literalizer; +import org.chocosolver.solver.Model; +import org.chocosolver.solver.constraints.Constraint; +import org.chocosolver.solver.constraints.nary.cnf.ILogical; +import org.chocosolver.solver.constraints.nary.cnf.LogOp; +import org.chocosolver.solver.variables.Group; +import org.chocosolver.solver.variables.IntVar; +import org.chocosolver.solver.variables.OptionalTask; +import org.chocosolver.solver.variables.Task; +import org.chocosolver.solver.variables.Variable; + +import java.lang.reflect.Array; +import java.util.ArrayList; +import java.util.List; + +/** + * Replays the steps of a {@link ModelSpec} on a new model. + * Not thread-safe: one replayer per instantiation. + * + * @author Charles Prud'homme + */ +final class Replayer extends IdTable { + + Replayer(Header header) { + super(new Model(header.name(), header.settings())); + model().setSeed(header.seed()); + } + + Resolver replay(List steps) { + for (int i = 0; i < steps.size(); i++) { + Step step = steps.get(i); + try { + apply(step); + } catch (VirtualMachineError e) { + // e.g., OutOfMemoryError: not a problem of the spec + throw e; + } catch (Throwable t) { + throw new SpecException("Step #" + i + " (" + step + ") failed: " + t.getMessage(), t); + } + } + return this; + } + + private void apply(Step step) throws Throwable { + Model model = model(); + if (step instanceof Step.Call c) { + Class[] types = c.method().rawParameterTypes(); + Arg[] args = c.rawArgs(); + Object[] values = new Object[args.length]; + for (int k = 0; k < args.length; k++) { + values[k] = materialize(args[k], types[k]); + } + bindOutputs(c.rawOut(), c.method().invoke(model, values)); + } else if (step instanceof Step.Post p) { + model.post(constraints(p.rawCstrs())); + } else if (step instanceof Step.Reify r) { + bind(r.out(), constraint(r.cstr()).reify()); + } else if (step instanceof Step.Link l) { + Constraint c = constraint(l.cstr()); + switch (l.kind()) { + case REIFY_WITH -> c.reifyWith(boolVar(l.bool())); + case IMPLIES -> c.implies(boolVar(l.bool())); + case IMPLIED_BY -> c.impliedBy(boolVar(l.bool())); + } + } else if (step instanceof Step.Unpost u) { + model.unpost(constraints(u.rawCstrs())); + } else if (step instanceof Step.NewTask t) { + IntVar s = intVar(t.start()); + IntVar d = intVar(t.duration()); + IntVar e = intVar(t.end()); + bind(t.out(), t.performed() < 0 ? new Task(s, d, e) : new OptionalTask(s, d, e, boolVar(t.performed()))); + } else if (step instanceof Step.Custom c) { + Constraint cstr = c.factory().apply(this); + if (cstr == null) { + throw new SpecException("Custom constraint " + c.name() + " built nothing"); + } + if (c.out() >= 0) { + bind(c.out(), cstr); + } + } else if (step instanceof Step.Hook h) { + Object value = materialize(h.value(), Object.class); + if (h.name() == null) { + model.removeAllHooks(); + } else if (value == null) { + model.removeHook(h.name()); + } else { + model.addHook(h.name(), value); + } + } else if (step instanceof Step.Seed s) { + model.setSeed(s.seed()); + } else if (step instanceof Step.Objective o) { + if (o.var() < 0) { + model.clearObjective(); + } else { + model.setObjective(o.maximize(), get(o.var(), Variable.class)); + } + } else if (step instanceof Step.Group g) { + model.addGroup(new Group<>(g.name(), (Variable[]) materialize(g.vars(), Variable[].class))); + } else { + throw new SpecException("Unknown step " + step); + } + } + + private Constraint[] constraints(int[] cids) { + Constraint[] cs = new Constraint[cids.length]; + for (int i = 0; i < cids.length; i++) { + cs[i] = constraint(cids[i]); + } + return cs; + } + + private Object materialize(Arg arg, Class type) { + Object value; + if (arg instanceof Arg.Ref r) { + value = get(r.id()); + } else if (arg instanceof Arg.RefArray a) { + value = array(a.componentType(), a.rawIds()); + } else if (arg instanceof Arg.RefMatrix a) { + int[][] rows = a.rawIds(); + Object[] matrix = (Object[]) Array.newInstance(a.componentType().arrayType(), rows.length); + for (int i = 0; i < rows.length; i++) { + matrix[i] = array(a.componentType(), rows[i]); + } + value = matrix; + } else if (arg instanceof Arg.RefList l) { + List list = new ArrayList<>(l.rawIds().length); + for (int id : l.rawIds()) { + list.add(get(id)); + } + value = list; + } else if (arg instanceof Arg.Const c) { + value = c.value(); + } else if (arg instanceof Arg.Logic l) { + value = logic(l); + } else if (arg instanceof Arg.Literal l) { + value = switch (l.kind()) { + case BOOL -> new Literalizer.BoolLit(boolVar(l.var())); + case INT_EQ -> new Literalizer.IntEqLit(intVar(l.var()), l.value()); + case INT_LE -> new Literalizer.IntLeLit(intVar(l.var()), l.value()); + }; + } else { + throw new SpecException("Unknown argument " + arg); + } + if (value == null ? type.isPrimitive() : !Specs.wrap(type).isInstance(value)) { + throw new SpecException("Argument " + arg + " is not a " + type.getSimpleName()); + } + return value; + } + + private Object[] array(Class componentType, int[] aids) { + Object[] array = (Object[]) Array.newInstance(componentType, aids.length); + for (int i = 0; i < aids.length; i++) { + try { + array[i] = get(aids[i]); + } catch (ArrayStoreException e) { + throw new SpecException("Identifier " + aids[i] + " is bound to a " + + get(aids[i]).getClass().getSimpleName() + ", not a " + componentType.getSimpleName()); + } + } + return array; + } + + private LogOp logic(Arg.Logic l) { + Arg[] children = l.rawChildren(); + ILogical[] ops = new ILogical[children.length]; + for (int i = 0; i < children.length; i++) { + ops[i] = children[i] instanceof Arg.Logic sub ? logic(sub) : boolVar(((Arg.Ref) children[i]).id()); + } + if (l.and()) { + return l.negated() ? LogOp.nand(ops) : LogOp.and(ops); + } + return l.negated() ? LogOp.nor(ops) : LogOp.or(ops); + } + + private void bindOutputs(int[] out, Object result) { + if (out.length == 0) { + return; + } + if (result instanceof Object[] array) { + List flat = new ArrayList<>(out.length); + Specs.flatten(array, flat); + if (flat.size() != out.length) { + throw new SpecException("Expected " + out.length + " outputs, got " + flat.size()); + } + for (int i = 0; i < out.length; i++) { + if (out[i] >= 0) { + bind(out[i], flat.get(i)); + } + } + } else { + if (out.length != 1) { + throw new SpecException("Expected " + out.length + " outputs, got 1"); + } + bind(out[0], result); + } + } + + private void bind(int id, Object o) { + if (o == null) { + throw new SpecException("Cannot bind identifier " + id + " to null"); + } + Object prev = put(id, o); + if (prev != null && prev != o) { + throw new SpecException("Divergence: identifier " + id + " is bound to " + prev + ", now to " + o); + } + } +} diff --git a/solver/src/main/java/org/chocosolver/solver/spec/Resolver.java b/solver/src/main/java/org/chocosolver/solver/spec/Resolver.java new file mode 100644 index 0000000000..4d5325bf9d --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/spec/Resolver.java @@ -0,0 +1,89 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.Model; +import org.chocosolver.solver.constraints.Constraint; +import org.chocosolver.solver.variables.BoolVar; +import org.chocosolver.solver.variables.IntVar; +import org.chocosolver.solver.variables.Task; + +/** + * Maps the identifiers of a {@link ModelSpec} to the objects of one instantiated model. + * + * @author Charles Prud'homme + */ +public interface Resolver { + + /** + * @return the model under instantiation (or instantiated) + */ + Model model(); + + /** + * @param id an identifier + * @return the object bound to id + * @throws SpecException if id is not bound + */ + Object get(int id); + + /** + * @param id an identifier + * @param type expected type of the object + * @return the object bound to id + * @throws SpecException if id is not bound or not of the expected type + */ + default T get(int id, Class type) { + Object o = get(id); + if (!type.isInstance(o)) { + throw new SpecException("Identifier " + id + " is bound to a " + o.getClass().getSimpleName() + + ", not a " + type.getSimpleName()); + } + return type.cast(o); + } + + /** + * @return an upper bound (exclusive) of the identifiers + */ + int capacity(); + + /** + * @param id an identifier + * @return true if id is bound to an object + */ + boolean isBound(int id); + + /** + * @param o an object of the model + * @return the (first) identifier bound to o, or -1 if none + */ + int idOf(Object o); + + default IntVar intVar(int id) { + return get(id, IntVar.class); + } + + default IntVar[] intVars(int... ids) { + IntVar[] vars = new IntVar[ids.length]; + for (int i = 0; i < ids.length; i++) { + vars[i] = intVar(ids[i]); + } + return vars; + } + + default BoolVar boolVar(int id) { + return get(id, BoolVar.class); + } + + default Constraint constraint(int id) { + return get(id, Constraint.class); + } + + default Task task(int id) { + return get(id, Task.class); + } +} diff --git a/solver/src/main/java/org/chocosolver/solver/spec/SearchDecl.java b/solver/src/main/java/org/chocosolver/solver/spec/SearchDecl.java new file mode 100644 index 0000000000..551ce179c2 --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/spec/SearchDecl.java @@ -0,0 +1,109 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.Model; +import org.chocosolver.solver.Solver; +import org.chocosolver.solver.search.strategy.Search; +import org.chocosolver.solver.search.strategy.SearchParams; +import org.chocosolver.solver.search.strategy.strategy.AbstractStrategy; +import org.chocosolver.solver.variables.IntVar; + +import java.util.Objects; +import java.util.function.Consumer; + +/** + * The search of a {@link ModelSpec}: configures the solver of each instance, once all the steps are replayed. + *

+ * A search declaration is shared by all the instances, possibly configured concurrently: it must be stateless and + * must only use the objects of the instance, obtained from the {@link Resolver} (never objects of another model, + * which is checked by assertions when the strategy is set). + *

+ * Search strategies cannot be journalized: they are declared, either from the catalog of this interface + * (heuristics and identifiers of variables), or as a function of the model or of the {@link Resolver}. + * + * @author Charles Prud'homme + */ +@FunctionalInterface +public interface SearchDecl { + + /** + * Configure the solver of an instance. + * + * @param resolver maps the identifiers of the spec to the objects of the instance + */ + void configure(Resolver resolver); + + /** + * @return a declaration which applies this one, then next + */ + default SearchDecl andThen(SearchDecl next) { + Objects.requireNonNull(next); + return r -> { + configure(r); + next.configure(r); + }; + } + + /** + * A declaration based on the model only, e.g. {@code SearchDecl.of(Search::defaultSearch)} or + * {@code SearchDecl.of(BlackBoxConfigurator.forCOP()::make)}: the model of each instance holds the same + * variables, groups, hooks and objective as the recorded one. + * + * @param configurer configures a model; must be stateless + */ + static SearchDecl of(Consumer configurer) { + Objects.requireNonNull(configurer); + return r -> configurer.accept(r.model()); + } + + /** + * An integer search strategy over the variables identified by ids. + * + * @param varSel variable selection + * @param valSel value selection + * @param ids identifiers of the decision variables, in order + */ + static SearchDecl intVarSearch(SearchParams.VarSelConf varSel, SearchParams.ValSelConf valSel, int... ids) { + Objects.requireNonNull(varSel); + Objects.requireNonNull(valSel); + int[] vids = ids.clone(); + return r -> { + IntVar[] vars = r.intVars(vids); + r.model().getSolver().setSearch(varSel.make().apply(vars, valSel.make().apply(r.model()))); + }; + } + + /** + * Add a restart policy. + * + * @param conf the restart policy + */ + static SearchDecl restarts(SearchParams.ResConf conf) { + Objects.requireNonNull(conf); + return r -> { + Solver solver = r.model().getSolver(); + solver.addRestarter(conf.make().apply(solver)); + }; + } + + /** + * Wrap the current search strategy with last conflict. + * + * @param k number of conflicting variables to remember + */ + static SearchDecl lastConflict(int k) { + return r -> { + Solver solver = r.model().getSolver(); + AbstractStrategy current = solver.getSearch(); + if (current == null) { + throw new SpecException("lastConflict requires a search strategy to wrap"); + } + solver.setSearch(Search.lastConflict(current, k)); + }; + } +} diff --git a/solver/src/main/java/org/chocosolver/solver/spec/SharedObjects.java b/solver/src/main/java/org/chocosolver/solver/spec/SharedObjects.java new file mode 100644 index 0000000000..33afd410cf --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/spec/SharedObjects.java @@ -0,0 +1,252 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.Settings; +import org.chocosolver.solver.constraints.nary.automata.FA.utils.ICounter; + +import java.lang.invoke.MethodHandle; +import java.lang.ref.Reference; +import java.lang.reflect.Array; +import java.lang.reflect.Field; +import java.lang.reflect.Method; +import java.lang.reflect.Modifier; +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Collection; +import java.util.Collections; +import java.util.Deque; +import java.util.IdentityHashMap; +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.concurrent.ConcurrentHashMap; +import java.util.function.BiConsumer; + +/** + * Diagnostic tool: finds the objects shared by two object graphs (typically, two models instantiated from the same + * {@link ModelSpec}), which must be immutable for the models to be solved concurrently. + *

+ * Objects are compared by identity. The traversal follows instance fields (static fields are ignored), array + * elements, the elements of collections and maps, and referents. Objects of classes which cannot be introspected + * (e.g., of the JDK) are compared but not traversed. + *

+ * Are neither reported nor traversed: immutable objects (classes, methods, the values shared according to the policy + * of {@link Values}), and the data shared by design ({@link Settings}, {@link ICounter}, {@link FactoryMethod}, frozen + * tuples and diagrams). What the latter own is not reported either, even when reached by another path. + * + * @author Charles Prud'homme + */ +public final class SharedObjects { + + private static final Map, Field[]> FIELDS = new ConcurrentHashMap<>(); + + private SharedObjects() { + } + + /** + * A shared object. + * + * @param type type of the object + * @param path a path to the object from the root of the second graph + */ + public record Shared(Class type, String path) { + @Override + public String toString() { + return type.getName() + " at " + path; + } + } + + /** + * @param a root of the first graph + * @param b root of the second graph + * @param allowed types whose instances may be shared (neither reported nor traversed) + * @return the mutable objects reachable from both a and b, one example per type + */ + public static List between(Object a, Object b, Set> allowed) { + return between(a, b, allowed, List.of()); + } + + /** + * @param a root of the first graph + * @param b root of the second graph + * @param allowed types whose instances may be shared (neither reported nor traversed) + * @param byDesign objects which may be shared, e.g. the constants of a {@link ModelSpec} (see + * {@link #constantsOf(ModelSpec)}): neither they nor what they own are reported + * @return the mutable objects reachable from both a and b, one example per type + */ + public static List between(Object a, Object b, Set> allowed, Collection byDesign) { + Set common = common(a, b, allowed, byDesign); + if (common.isEmpty()) { + return List.of(); + } + // a path to one shared object per type + Map, Shared> shared = new LinkedHashMap<>(); + traverse(b, allowed, identitySet(), identitySet(), (o, node) -> { + if (common.contains(o)) { + shared.putIfAbsent(o.getClass(), new Shared(o.getClass(), node.path())); + } + }, true); + return new ArrayList<>(shared.values()); + } + + /** + * @return the mutable objects reachable from both a and b, but those shared by design and what they + * own (see {@link #between(Object, Object, Set, Collection)}) + */ + public static Set common(Object a, Object b, Set> allowed, Collection byDesign) { + Set designed = identitySet(); + designed.addAll(byDesign); + // no path kept, to save memory + Set fromA = identitySet(); + traverse(a, allowed, fromA, designed, null, false); + Set common = identitySet(); + traverse(b, allowed, identitySet(), designed, (o, node) -> { + if (fromA.contains(o)) { + common.add(o); + } + }, false); + fromA.clear(); + // what the data shared by design own may be reached by other paths (e.g., the matrix of frozen tuples + // referenced by a propagator): it is shared by design too + if (!common.isEmpty()) { + Set owned = identitySet(); + for (Object d : designed) { + traverse(d, null, owned, null, null, false); + } + common.removeAll(owned); + } + return common; + } + + /** + * @return the constants of spec, which are shared by design by its instances + */ + public static List constantsOf(ModelSpec spec) { + List constants = new ArrayList<>(); + for (Step s : spec.steps()) { + if (s instanceof Step.Call c) { + for (Arg arg : c.rawArgs()) { + if (arg instanceof Arg.Const k && k.rawValue() != null) { + constants.add(k.rawValue()); + } + } + } + } + return constants; + } + + private static Set identitySet() { + return Collections.newSetFromMap(new IdentityHashMap<>()); + } + + private record Node(Object object, Node parent, String edge) { + String path() { + return parent == null ? edge : parent.path() + edge; + } + } + + /** + * Traverse the graph of root. When allowed is not null, immutable objects are skipped; when + * byDesign is not null, the data shared by design are skipped and collected in it. Paths from the root + * are kept only if paths is set. + */ + private static void traverse(Object root, Set> allowed, Set seen, Set byDesign, + BiConsumer visitor, boolean paths) { + Deque stack = new ArrayDeque<>(); + stack.push(new Node(root, null, root.getClass().getSimpleName())); + while (!stack.isEmpty()) { + Node node = stack.pop(); + Object o = node.object; + if (o == null || !seen.add(o)) { + continue; + } + if (allowed != null && isImmutable(o, allowed)) { + continue; + } + if (byDesign != null && (byDesign.contains(o) || isSharedByDesign(o))) { + byDesign.add(o); + continue; + } + if (visitor != null) { + visitor.accept(o, node); + } + Node parent = paths ? node : null; + Class c = o.getClass(); + if (c.isArray()) { + if (!c.getComponentType().isPrimitive()) { + int n = Array.getLength(o); + for (int i = 0; i < n; i++) { + stack.push(new Node(Array.get(o, i), parent, paths ? "[" + i + "]" : null)); + } + } + } else if (o instanceof Collection col) { + try { + for (Object e : col) { + stack.push(new Node(e, parent, paths ? "{}" : null)); + } + } catch (RuntimeException ignored) { + // concurrent or lazy collection: elements not traversed + } + } else if (o instanceof Reference ref) { + stack.push(new Node(ref.get(), parent, paths ? ".get()" : null)); + } else if (o instanceof Map map) { + try { + for (Map.Entry e : map.entrySet()) { + stack.push(new Node(e.getKey(), parent, paths ? "{key}" : null)); + stack.push(new Node(e.getValue(), parent, paths ? "{" + e.getKey() + "}" : null)); + } + } catch (RuntimeException ignored) { + // elements not traversed + } + } else { + for (Field f : fields(c)) { + try { + stack.push(new Node(f.get(o), parent, paths ? "." + f.getName() : null)); + } catch (IllegalAccessException ignored) { + // not traversed + } + } + } + } + } + + private static boolean isSharedByDesign(Object o) { + return o instanceof Settings || o instanceof ICounter || o instanceof FactoryMethod || Values.isShared(o); + } + + private static boolean isImmutable(Object o, Set> allowed) { + if (o instanceof String || o instanceof Number || o instanceof Boolean || o instanceof Character + || o instanceof Enum || o instanceof Class || o instanceof Method || o instanceof MethodHandle) { + return true; + } + for (Class a : allowed) { + if (a.isInstance(o)) { + return true; + } + } + return !(o instanceof Collection) && !(o instanceof Map) && Specs.isStateless(o.getClass()); + } + + /** + * @return the accessible instance fields of c and its superclasses + */ + private static Field[] fields(Class c) { + return FIELDS.computeIfAbsent(c, k -> { + List list = new ArrayList<>(); + for (Class x = k; x != null; x = x.getSuperclass()) { + for (Field f : x.getDeclaredFields()) { + if (!Modifier.isStatic(f.getModifiers()) && !f.getType().isPrimitive() && f.trySetAccessible()) { + list.add(f); + } + } + } + return list.toArray(new Field[0]); + }); + } +} diff --git a/solver/src/main/java/org/chocosolver/solver/spec/SpecBuilder.java b/solver/src/main/java/org/chocosolver/solver/spec/SpecBuilder.java new file mode 100644 index 0000000000..518d897103 --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/spec/SpecBuilder.java @@ -0,0 +1,322 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.sat.Literalizer; +import org.chocosolver.solver.IModel; +import org.chocosolver.solver.constraints.Constraint; +import org.chocosolver.solver.constraints.nary.cnf.LogOp; +import org.chocosolver.solver.variables.BoolVar; +import org.chocosolver.solver.variables.OptionalTask; +import org.chocosolver.solver.variables.Task; + +import java.lang.reflect.Method; +import java.lang.reflect.Modifier; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.function.Function; +import java.util.stream.Collectors; + +/** + * Helps building a {@link ModelSpec} by hand: allocates identifiers and resolves the overload of factory methods + * from the types of the arguments. + *

+ * Arguments passed to {@code call*} methods are either {@link Arg}s or constants (wrapped in {@link Arg.Const}). + * 

{@code
+ * SpecBuilder b = new SpecBuilder(Header.of("demo"));
+ * int[] x = b.callArray(3, "intVarArray", "x", 3, 1, 3);
+ * b.post(b.call("allDifferent", b.refs(IntVar.class, x)));
+ * ModelSpec spec = b.build();
+ * }
+ * + * @author Charles Prud'homme + */ +public final class SpecBuilder { + + /** + * The (non-static) methods of {@link IModel}, by name. + */ + private static final Map> METHODS = Arrays.stream(IModel.class.getMethods()) + .filter(m -> !Modifier.isStatic(m.getModifiers())) + .collect(Collectors.groupingBy(Method::getName)); + + private final Header header; + private final List steps = new ArrayList<>(); + /** + * Static type of each identifier, to resolve overloads. + */ + private final Map> types = new HashMap<>(); + private int nextId; + private SearchDecl search; + + public SpecBuilder(Header header) { + this.header = header; + } + + /** + * @return a builder which continues spec: its steps, identifiers and search are kept + */ + public static SpecBuilder from(ModelSpec spec) { + SpecBuilder b = new SpecBuilder(spec.header()); + b.search = spec.search(); + for (Step s : spec.steps()) { + b.steps.add(s); + if (s instanceof Step.Call c) { + Class t = Specs.elementType(c.method().returnType()); + for (int o : c.rawOut()) { + if (o >= 0) { + b.types.put(o, t); + } + } + } else if (s instanceof Step.Reify r) { + b.types.put(r.out(), BoolVar.class); + } else if (s instanceof Step.NewTask t) { + b.types.put(t.out(), t.performed() < 0 ? Task.class : OptionalTask.class); + } else if (s instanceof Step.Custom c) { + b.types.put(c.out(), Constraint.class); + } + s.forEachDef(id -> b.nextId = Math.max(b.nextId, id + 1)); + } + return b; + } + + /** + * Set the search of the spec. + */ + public SpecBuilder search(SearchDecl search) { + this.search = search; + return this; + } + + /** + * @return a reference to identifier id + */ + public Arg.Ref ref(int id) { + return new Arg.Ref(id); + } + + /** + * @return a reference to an array of objects of type componentType + */ + public Arg.RefArray refs(Class componentType, int... ids) { + return new Arg.RefArray(componentType, ids); + } + + /** + * @return a reference to a matrix of objects of type componentType + */ + public Arg.RefMatrix refs(Class componentType, int[][] ids) { + return new Arg.RefMatrix(componentType, ids); + } + + /** + * Call a factory method whose result is ignored (or which returns nothing). + */ + public SpecBuilder effect(String name, Object... args) { + return effect(resolve(name, args), args); + } + + public SpecBuilder effect(FactoryMethod m, Object... args) { + steps.add(new Step.Call(Specs.NO_INT, m, toArgs(args))); + return this; + } + + /** + * Call a factory method which returns an object (variable, constraint, task...). + * + * @return the identifier of the object + */ + public int call(String name, Object... args) { + return call(resolve(name, args), args); + } + + public int call(FactoryMethod m, Object... args) { + int id = define(m.returnType()); + steps.add(new Step.Call(new int[]{id}, m, toArgs(args))); + return id; + } + + /** + * Call a factory method which returns an array (or a matrix, flattened row by row) of size objects. + * + * @return the identifiers of the objects + */ + public int[] callArray(int size, String name, Object... args) { + return callArray(size, resolve(name, args), args); + } + + public int[] callArray(int size, FactoryMethod m, Object... args) { + int[] out = new int[size]; + Class component = Specs.elementType(m.returnType()); + for (int i = 0; i < size; i++) { + out[i] = define(component); + } + steps.add(new Step.Call(out, m, toArgs(args))); + return out; + } + + public SpecBuilder post(int... cstrs) { + steps.add(new Step.Post(cstrs)); + return this; + } + + /** + * @return the identifier of the boolean variable reifying cstr + */ + public int reify(int cstr) { + int id = define(BoolVar.class); + steps.add(new Step.Reify(cstr, id)); + return id; + } + + public SpecBuilder reifyWith(int cstr, int bool) { + return link(Step.Link.Kind.REIFY_WITH, cstr, bool); + } + + public SpecBuilder implies(int cstr, int bool) { + return link(Step.Link.Kind.IMPLIES, cstr, bool); + } + + public SpecBuilder impliedBy(int cstr, int bool) { + return link(Step.Link.Kind.IMPLIED_BY, cstr, bool); + } + + private SpecBuilder link(Step.Link.Kind kind, int cstr, int bool) { + steps.add(new Step.Link(kind, cstr, bool)); + return this; + } + + public SpecBuilder unpost(int... cstrs) { + steps.add(new Step.Unpost(cstrs)); + return this; + } + + /** + * @return the identifier of the new task + */ + public int newTask(int start, int duration, int end) { + int id = define(Task.class); + steps.add(new Step.NewTask(id, start, duration, end)); + return id; + } + + /** + * @return the identifier of the new optional task + */ + public int newOptionalTask(int start, int duration, int end, int performed) { + int id = define(OptionalTask.class); + steps.add(new Step.NewTask(id, start, duration, end, performed)); + return id; + } + + /** + * @return the identifier of the custom constraint + */ + public int custom(String name, Function factory) { + int id = define(Constraint.class); + steps.add(new Step.Custom(id, name, factory)); + return id; + } + + public ModelSpec build() { + return new ModelSpec(header, steps, search); + } + + /** + * @return a new identifier, of static type type + */ + private int define(Class type) { + int id = nextId++; + types.put(id, type); + return id; + } + + private static Arg[] toArgs(Object[] args) { + Arg[] res = new Arg[args.length]; + for (int i = 0; i < args.length; i++) { + res[i] = args[i] instanceof Arg a ? a : new Arg.Const(args[i]); + } + return res; + } + + /** + * Resolve the overload of name which accepts args, choosing the most specific one as javac would. + */ + private FactoryMethod resolve(String name, Object[] args) { + List candidates = new ArrayList<>(); + for (Method m : METHODS.getOrDefault(name, List.of())) { + if (m.getParameterCount() == args.length && accepts(m.getParameterTypes(), args)) { + candidates.add(m); + } + } + List mostSpecific = new ArrayList<>(); + for (Method m : candidates) { + if (candidates.stream().allMatch(o -> moreSpecific(m, o))) { + mostSpecific.add(m); + } + } + if (mostSpecific.size() != 1) { + throw new SpecException((candidates.isEmpty() ? "No" : "Ambiguous") + " factory method " + name + + " for arguments " + Arrays.stream(args).map(this::describe).collect(Collectors.joining(", ", "(", ")")) + + (candidates.isEmpty() ? "" : ": " + candidates)); + } + return FactoryMethod.of(mostSpecific.get(0)); + } + + private static boolean moreSpecific(Method m, Method o) { + Class[] pm = m.getParameterTypes(); + Class[] po = o.getParameterTypes(); + for (int i = 0; i < pm.length; i++) { + if (!po[i].isAssignableFrom(pm[i])) return false; + } + return true; + } + + private boolean accepts(Class[] params, Object[] args) { + for (int i = 0; i < params.length; i++) { + Class t = typeOf(args[i]); + if (t == null ? params[i].isPrimitive() : !Specs.wrap(params[i]).isAssignableFrom(t)) { + return false; + } + } + return true; + } + + /** + * @return the static type of an argument, null for a null constant + */ + private Class typeOf(Object arg) { + if (arg instanceof Arg.Ref r) { + Class t = types.get(r.id()); + if (t == null) { + throw new SpecException("Undefined identifier " + r.id()); + } + return t; + } else if (arg instanceof Arg.RefArray a) { + return a.componentType().arrayType(); + } else if (arg instanceof Arg.RefMatrix a) { + return a.componentType().arrayType().arrayType(); + } else if (arg instanceof Arg.RefList) { + return List.class; + } else if (arg instanceof Arg.Logic) { + return LogOp.class; + } else if (arg instanceof Arg.Literal) { + return Literalizer.class; + } else if (arg instanceof Arg.Const c) { + return typeOf(c.rawValue()); + } + return arg == null ? null : arg.getClass(); + } + + private String describe(Object arg) { + Class t = typeOf(arg); + return t == null ? "null" : t.getSimpleName(); + } +} diff --git a/solver/src/main/java/org/chocosolver/solver/spec/SpecException.java b/solver/src/main/java/org/chocosolver/solver/spec/SpecException.java new file mode 100644 index 0000000000..c9a6057f75 --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/spec/SpecException.java @@ -0,0 +1,26 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.exception.SolverException; + +/** + * Thrown when a {@link ModelSpec} is ill-formed or cannot be instantiated. + * + * @author Charles Prud'homme + */ +public class SpecException extends SolverException { + + public SpecException(String message) { + super(message); + } + + public SpecException(String message, Throwable cause) { + super(message); + initCause(cause); + } +} diff --git a/solver/src/main/java/org/chocosolver/solver/spec/SpecSolution.java b/solver/src/main/java/org/chocosolver/solver/spec/SpecSolution.java new file mode 100644 index 0000000000..46b38fd6b2 --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/spec/SpecSolution.java @@ -0,0 +1,102 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.Solution; +import org.chocosolver.solver.variables.IntVar; + +import java.util.Arrays; + +/** + * A solution expressed with the identifiers of a {@link ModelSpec}: found by one instance, it can be read by any + * other instance, or by the recorded model. + *

+ * Only integer (and boolean) variables are stored. Immutable, hence shareable among threads. + * + * @author Charles Prud'homme + */ +public final class SpecSolution { + + /** + * Value of each identifier, meaningful only when stored. + */ + private final int[] values; + private final boolean[] stored; + + private SpecSolution(int[] values, boolean[] stored) { + this.values = values; + this.stored = stored; + } + + /** + * Record the current values of the instantiated integer variables of an instance, typically when a solution + * is found. + * + * @param resolver the resolver of the instance + * @return the solution + */ + public static SpecSolution record(Resolver resolver) { + int n = resolver.capacity(); + int[] values = new int[n]; + boolean[] stored = new boolean[n]; + for (int id = 0; id < n; id++) { + if (resolver.isBound(id) && resolver.get(id) instanceof IntVar v && v.isInstantiated()) { + values[id] = v.getValue(); + stored[id] = true; + } + } + return new SpecSolution(values, stored); + } + + /** + * @param id an identifier + * @return true if this solution holds a value for id + */ + public boolean contains(int id) { + return id >= 0 && id < stored.length && stored[id]; + } + + /** + * @param id identifier of an integer variable + * @return its value in this solution + * @throws SpecException if this solution holds no value for id + */ + public int valueOf(int id) { + if (!contains(id)) { + throw new SpecException("No value for identifier " + id); + } + return values[id]; + } + + /** + * Express this solution in terms of the variables of a model which follows the spec (an instance, or the + * recorded model). + * + * @param resolver identifies the variables of the target model + * @return a solution of the target model + */ + public Solution toSolution(Resolver resolver) { + Solution sol = new Solution(resolver.model()); + for (int id = 0; id < stored.length; id++) { + if (stored[id] && resolver.isBound(id) && resolver.get(id) instanceof IntVar v) { + sol.setIntVal(v, values[id]); + } + } + return sol; + } + + @Override + public boolean equals(Object o) { + return this == o || (o instanceof SpecSolution s + && Arrays.equals(values, s.values) && Arrays.equals(stored, s.stored)); + } + + @Override + public int hashCode() { + return 31 * Arrays.hashCode(values) + Arrays.hashCode(stored); + } +} diff --git a/solver/src/main/java/org/chocosolver/solver/spec/Specs.java b/solver/src/main/java/org/chocosolver/solver/spec/Specs.java new file mode 100644 index 0000000000..ed104d2645 --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/spec/Specs.java @@ -0,0 +1,82 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import java.lang.invoke.MethodType; +import java.lang.reflect.Field; +import java.lang.reflect.Modifier; +import java.util.List; + +/** + * Helpers shared by the classes of this package. + * + * @author Charles Prud'homme + */ +final class Specs { + + static final int[] NO_INT = new int[0]; + + /** + * Whether the instances of a class have no instance field. + */ + private static final ClassValue STATELESS = new ClassValue<>() { + @Override + protected Boolean computeValue(Class c) { + if (c.isArray()) { + return false; + } + for (Class k = c; k != null; k = k.getSuperclass()) { + for (Field f : k.getDeclaredFields()) { + if (!Modifier.isStatic(f.getModifiers())) { + return false; + } + } + } + return true; + } + }; + + private Specs() { + } + + /** + * @return true if the instances of c have no instance field, hence are immutable + */ + static boolean isStateless(Class c) { + return STATELESS.get(c); + } + + /** + * @return the type of the elements of c, whatever the number of dimensions (c if not an array) + */ + static Class elementType(Class c) { + while (c.isArray()) { + c = c.getComponentType(); + } + return c; + } + + /** + * Add the elements of array, row by row whatever the number of dimensions, to flat. + */ + static void flatten(Object[] array, List flat) { + for (Object o : array) { + if (o instanceof Object[] sub) { + flatten(sub, flat); + } else { + flat.add(o); + } + } + } + + /** + * @return the wrapper class of c if primitive, c otherwise + */ + static Class wrap(Class c) { + return c.isPrimitive() ? MethodType.methodType(c).wrap().returnType() : c; + } +} diff --git a/solver/src/main/java/org/chocosolver/solver/spec/Step.java b/solver/src/main/java/org/chocosolver/solver/spec/Step.java new file mode 100644 index 0000000000..48ec7ce8d4 --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/spec/Step.java @@ -0,0 +1,300 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.constraints.Constraint; +import org.chocosolver.solver.variables.OptionalTask; +import org.chocosolver.solver.variables.Task; + +import java.util.Arrays; +import java.util.Objects; +import java.util.function.Function; +import java.util.function.IntConsumer; + +/** + * A step of a {@link ModelSpec}. Steps are replayed in order. + *

+ * A step may define identifiers (its outputs) and use identifiers defined by previous steps. + * An identifier may be defined more than once, provided that the replay binds it to the same object each time + * (e.g., a cached constant). + *

+ * Steps are immutable: public accessors return copies, the package reads the arrays directly. + * + * @author Charles Prud'homme + */ +public sealed interface Step permits Step.Call, Step.Post, Step.Reify, Step.Link, Step.Unpost, Step.NewTask, + Step.Custom, Step.Hook, Step.Seed, Step.Objective, Step.Group { + + /** + * Apply action on each identifier this step uses. + */ + default void forEachUse(IntConsumer action) { + } + + /** + * Apply action on each identifier this step defines. + */ + default void forEachDef(IntConsumer action) { + } + + /** + * A call to a factory method of the model. + * + * @param out identifiers of the outputs: empty if the result is ignored, one identifier for an object, + * one identifier per element for an array (row by row for a matrix), -1 to skip an element + * @param method the factory method + * @param args the arguments, one per parameter of method + */ + record Call(int[] out, FactoryMethod method, Arg[] args) implements Step { + public Call { + Objects.requireNonNull(method); + out = out.clone(); + args = args.clone(); + if (args.length != method.parameterCount()) { + throw new SpecException(method + " expects " + method.parameterCount() + + " arguments, got " + args.length); + } + if (out.length > 0 && method.returnType() == void.class) { + throw new SpecException(method + " returns nothing"); + } + } + + @Override + public int[] out() { + return out.clone(); + } + + @Override + public Arg[] args() { + return args.clone(); + } + + int[] rawOut() { + return out; + } + + Arg[] rawArgs() { + return args; + } + + @Override + public void forEachUse(IntConsumer action) { + for (Arg a : args) a.forEachRef(action); + } + + @Override + public void forEachDef(IntConsumer action) { + for (int o : out) if (o >= 0) action.accept(o); + } + + @Override + public String toString() { + return Arrays.toString(out) + " = " + method.name() + Arrays.toString(args); + } + } + + /** + * Post constraints, as {@link org.chocosolver.solver.Model#post(Constraint...)}. + */ + record Post(int[] cstrs) implements Step { + public Post { + cstrs = cstrs.clone(); + } + + @Override + public int[] cstrs() { + return cstrs.clone(); + } + + int[] rawCstrs() { + return cstrs; + } + + @Override + public void forEachUse(IntConsumer action) { + for (int c : cstrs) action.accept(c); + } + + @Override + public String toString() { + return "post" + Arrays.toString(cstrs); + } + } + + /** + * Reify a constraint, as {@link Constraint#reify()}, and bind the resulting boolean variable to out. + */ + record Reify(int cstr, int out) implements Step { + @Override + public void forEachUse(IntConsumer action) { + action.accept(cstr); + } + + @Override + public void forEachDef(IntConsumer action) { + action.accept(out); + } + } + + /** + * Link a constraint to a boolean variable: {@link Constraint#reifyWith}, {@link Constraint#implies} or + * {@link Constraint#impliedBy}. + */ + record Link(Kind kind, int cstr, int bool) implements Step { + + /** + * The kinds of links between a constraint and a boolean variable. + */ + public enum Kind { + REIFY_WITH, IMPLIES, IMPLIED_BY + } + + public Link { + Objects.requireNonNull(kind); + } + + @Override + public void forEachUse(IntConsumer action) { + action.accept(cstr); + action.accept(bool); + } + } + + /** + * Unpost constraints, as {@link org.chocosolver.solver.Model#unpost(Constraint...)}. + */ + record Unpost(int[] cstrs) implements Step { + public Unpost { + cstrs = cstrs.clone(); + } + + @Override + public int[] cstrs() { + return cstrs.clone(); + } + + int[] rawCstrs() { + return cstrs; + } + + @Override + public void forEachUse(IntConsumer action) { + for (int c : cstrs) action.accept(c); + } + + @Override + public String toString() { + return "unpost" + Arrays.toString(cstrs); + } + } + + /** + * Create a {@link Task} (or an {@link OptionalTask} when performed is not -1) with its canonical + * constructor, from existing variables. + * + * @param out identifier of the task + * @param start identifier of the start variable + * @param duration identifier of the duration variable + * @param end identifier of the end variable + * @param performed identifier of the boolean variable of an optional task, -1 for a mandatory task + */ + record NewTask(int out, int start, int duration, int end, int performed) implements Step { + + public NewTask(int out, int start, int duration, int end) { + this(out, start, duration, end, -1); + } + + @Override + public void forEachUse(IntConsumer action) { + action.accept(start); + action.accept(duration); + action.accept(end); + if (performed >= 0) action.accept(performed); + } + + @Override + public void forEachDef(IntConsumer action) { + action.accept(out); + } + } + + /** + * A custom constraint, built by factory on the model under instantiation, for specs built by hand + * ({@link SpecBuilder#custom}) or extended by a variant ({@link Variant#extend}); a recorded model journalizes + * its custom constraints as calls to {@code IConstraintFactory#custom}. + * The factory must only use objects obtained from the {@link Resolver}. + * The constraint is neither posted nor reified: use subsequent steps. + * + * @param out identifier of the constraint, -1 to ignore it + * @param name name of the custom constraint (for error messages) + * @param factory builds the constraint; must be stateless as it may be called concurrently + */ + record Custom(int out, String name, Function factory) implements Step { + public Custom { + Objects.requireNonNull(name); + Objects.requireNonNull(factory); + } + + @Override + public void forEachDef(IntConsumer action) { + if (out >= 0) action.accept(out); + } + } + + /** + * Add a hook to the model, as {@link org.chocosolver.solver.Model#addHook(String, Object)}, or remove it + * when value is a null constant; remove all the hooks, as + * {@link org.chocosolver.solver.Model#removeAllHooks()}, when name is null. + */ + record Hook(String name, Arg value) implements Step { + public Hook { + Objects.requireNonNull(value); + if (name == null && !(value instanceof Arg.Const c && c.value() == null)) { + throw new IllegalArgumentException("removing all the hooks takes no value"); + } + } + + @Override + public void forEachUse(IntConsumer action) { + value.forEachRef(action); + } + } + + /** + * Set the seed of the model, as {@link org.chocosolver.solver.Model#setSeed(long)}. + */ + record Seed(long seed) implements Step { + } + + /** + * Set the objective of the model, as {@link org.chocosolver.solver.Model#setObjective(boolean, + * org.chocosolver.solver.variables.Variable)}, or clear it when var is -1. + */ + record Objective(boolean maximize, int var) implements Step { + @Override + public void forEachUse(IntConsumer action) { + if (var >= 0) action.accept(var); + } + } + + /** + * Declare a group of variables, as + * {@link org.chocosolver.solver.Model#addGroup(org.chocosolver.solver.variables.Group)}. + * Groups are used by some search strategies to select the decision variables. + */ + record Group(String name, Arg.RefArray vars) implements Step { + public Group { + Objects.requireNonNull(name); + Objects.requireNonNull(vars); + } + + @Override + public void forEachUse(IntConsumer action) { + vars.forEachRef(action); + } + } +} diff --git a/solver/src/main/java/org/chocosolver/solver/spec/Values.java b/solver/src/main/java/org/chocosolver/solver/spec/Values.java new file mode 100644 index 0000000000..2c31f0cf1e --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/spec/Values.java @@ -0,0 +1,168 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.constraints.extension.Tuples; +import org.chocosolver.solver.constraints.extension.hybrid.HybridTuples; +import org.chocosolver.solver.constraints.nary.automata.FA.FiniteAutomaton; +import org.chocosolver.util.objects.graphs.MultivaluedDecisionDiagram; +import org.chocosolver.util.objects.setDataStructures.iterable.IntIterableRangeSet; + +import java.lang.reflect.Array; +import java.lang.reflect.Constructor; +import java.lang.reflect.RecordComponent; +import java.util.function.UnaryOperator; + +/** + * Sharing policy of the constant arguments of a {@link ModelSpec}: the single place which decides what is shared by + * the instances of a spec. + *

    + *
  • immutable values (boxed primitives, strings, enums) are shared;
    • + *
  • heavy read-only data ({@link Tuples}, {@link HybridTuples}, {@link MultivaluedDecisionDiagram}) are frozen on + * capture, then shared;
    • + *
  • objects without instance field (e.g., non-capturing lambdas, stateless singletons such as + * {@code Condition.EXCEPT_0}) cannot capture anything: they are shared;
    • + *
  • arrays (of any dimension, whose elements are supported) and {@link IntIterableRangeSet} are copied on capture + * and on each instantiation;
    • + *
  • automata ({@link FiniteAutomaton} and subclasses) are not thread-safe: copied on capture and on each + * instantiation;
    • + *
  • records whose components are supported: shared if all their components are, otherwise rebuilt with + * their canonical constructor from copied components.
    • + *
+ * Any other type is rejected, in particular capturing lambdas (they may capture objects of the recorded model). + * + * @author Charles Prud'homme + */ +final class Values { + + private Values() { + } + + /** + * Capture a constant when building a spec, detaching it from the caller. + * + * @param value a constant + * @return the value to store in the spec + * @throws SpecException if the type of value is not supported + */ + static Object capture(Object value) { + if (value instanceof Tuples t) { + return t.freeze(); + } + if (value instanceof HybridTuples t) { + return t.freeze(); + } + if (value instanceof MultivaluedDecisionDiagram mdd) { + return mdd.freeze(); + } + return isShared(value) ? value : copy(value, Values::capture); + } + + /** + * @param value a captured constant + * @return the value to pass to a model under instantiation + */ + static Object materialize(Object value) { + return isShared(value) ? value : copy(value, Values::materialize); + } + + /** + * @return true if value can be shared by models solved concurrently + */ + static boolean isShared(Object value) { + return value == null + || value instanceof Number + || value instanceof Boolean + || value instanceof Character + || value instanceof String + || value instanceof Enum + || (value instanceof Tuples t && t.isFrozen()) + || (value instanceof HybridTuples t && t.isFrozen()) + || (value instanceof MultivaluedDecisionDiagram mdd && mdd.isFrozen()) + || Specs.isStateless(value.getClass()) + || (value instanceof Record r && allShared(r)); + } + + private static boolean allShared(Record r) { + try { + for (RecordComponent rc : r.getClass().getRecordComponents()) { + if (!isShared(component(r, rc))) { + return false; + } + } + return true; + } catch (SpecException e) { + // a record which cannot be read is not shared: copying it reports the problem + return false; + } + } + + private static Object component(Record r, RecordComponent rc) { + try { + rc.getAccessor().setAccessible(true); + return rc.getAccessor().invoke(r); + } catch (ReflectiveOperationException | RuntimeException e) { + throw new SpecException("Cannot read the component " + rc.getName() + " of " + r.getClass().getName() + + " (is its package open to org.chocosolver.solver?)", e); + } + } + + /** + * @param elements copies the elements of an array or the components of a record + */ + private static Object copy(Object value, UnaryOperator elements) { + Class c = value.getClass(); + if (c.isArray()) { + int n = Array.getLength(value); + Object dst = Array.newInstance(c.getComponentType(), n); + if (c.getComponentType().isPrimitive()) { + System.arraycopy(value, 0, dst, 0, n); + } else { + Object[] src = (Object[]) value; + Object[] d = (Object[]) dst; + for (int i = 0; i < n; i++) { + d[i] = elements.apply(src[i]); + } + } + return dst; + } + if (value instanceof IntIterableRangeSet set) { + return set.duplicate(); + } + if (value instanceof FiniteAutomaton fa) { + // reading an automaton may lazily modify its internal (dk.brics) state + synchronized (fa) { + try { + return fa.clone(); + } catch (CloneNotSupportedException e) { + throw new SpecException("Cannot copy automaton", e); + } + } + } + if (value instanceof Record r) { + RecordComponent[] rcs = c.getRecordComponents(); + Object[] args = new Object[rcs.length]; + Class[] types = new Class[rcs.length]; + for (int i = 0; i < rcs.length; i++) { + args[i] = elements.apply(component(r, rcs[i])); + types[i] = rcs[i].getType(); + } + try { + Constructor canonical = c.getDeclaredConstructor(types); + canonical.setAccessible(true); + return canonical.newInstance(args); + } catch (ReflectiveOperationException | RuntimeException e) { + throw new SpecException("Cannot copy the record " + c.getName(), e); + } + } + if (c.isSynthetic() || c.isHidden()) { + throw new SpecException("Unsupported capturing lambda " + c.getName() + + ": it may capture objects of the recorded model; use a non-capturing lambda"); + } + throw new SpecException("Unsupported constant of type " + c.getName()); + } +} diff --git a/solver/src/main/java/org/chocosolver/solver/spec/Variant.java b/solver/src/main/java/org/chocosolver/solver/spec/Variant.java new file mode 100644 index 0000000000..d095e159a3 --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/spec/Variant.java @@ -0,0 +1,213 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.Settings; +import org.chocosolver.solver.constraints.extension.Tuples; +import org.chocosolver.solver.variables.IntVar; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.BitSet; +import java.util.List; +import java.util.Objects; +import java.util.function.Consumer; +import java.util.function.Predicate; +import java.util.function.UnaryOperator; + +/** + * A variant of a {@link ModelSpec}: a rewriting of the spec, applied once, whose result is instantiated by as many + * workers as needed (see {@link ModelSpec#with(Variant)}). + *

+ * A variant may change: + *

    + *
  • the header: {@link #seed(long)}, {@link #settings(Settings)};
    • + *
  • the calls to the factories, e.g. the consistency of {@code allDifferent} ({@link #allDifferent(String)}) + * or the algorithm of {@code table} ({@link #tableAlgorithm(String)}), or any call ({@link #mapCalls});
    • + *
  • the constraints: redundant constraints or symmetry breaking ({@link #extend(Consumer)}), removals + * ({@link #unpostIf(Predicate)});
    • + *
  • the search ({@link #search(SearchDecl)}).
    • + *
+ * Variants compose with {@link #andThen(Variant)}. + * + * @author Charles Prud'homme + */ +@FunctionalInterface +public interface Variant { + + /** + * The variant which changes nothing: a carbon copy. + */ + Variant IDENTITY = spec -> spec; + + /** + * @param spec a spec + * @return the rewritten spec + */ + ModelSpec apply(ModelSpec spec); + + /** + * @return a variant which applies this one, then next + */ + default Variant andThen(Variant next) { + Objects.requireNonNull(next); + return spec -> next.apply(apply(spec)); + } + + //*********************************************************************************** + // HEADER AND SEARCH + //*********************************************************************************** + + /** + * Change the seed: propagators drawing random numbers and randomized search strategies behave differently. + * Note that it may also change the encoding of expressions which are sampled ({@code ReExpression#embody}). + * The seeds set during the construction ({@link Step.Seed}) are removed, otherwise they would override this one. + */ + static Variant seed(long seed) { + return spec -> spec.withHeader(spec.header().withSeed(seed)) + .withSteps(spec.steps().stream().filter(s -> !(s instanceof Step.Seed)).toList()); + } + + /** + * Change the settings (e.g., enable views or LCG), which may change the way constraints are built. + */ + static Variant settings(Settings settings) { + Objects.requireNonNull(settings); + return spec -> spec.withHeader(spec.header().withSettings(settings)); + } + + /** + * Change the search. + */ + static Variant search(SearchDecl search) { + return spec -> spec.withSearch(search); + } + + //*********************************************************************************** + // CALLS + //*********************************************************************************** + + /** + * Rewrite each call to a factory method. + * + * @param rewriter returns the call to replay instead (possibly the same), which must define the same + * identifiers + */ + static Variant mapCalls(UnaryOperator rewriter) { + Objects.requireNonNull(rewriter); + return spec -> { + List steps = new ArrayList<>(spec.steps().size()); + for (Step s : spec.steps()) { + steps.add(s instanceof Step.Call c ? rewriter.apply(c) : s); + } + return spec.withSteps(steps); + }; + } + + /** + * Set the consistency of every {@code allDifferent} constraint. + * + * @param consistency among "DEFAULT", "AC", "AC_REGIN", "AC_ZHANG", "BC", "FC", "NEQS" + */ + static Variant allDifferent(String consistency) { + return withOption("allDifferent", consistency, IntVar[].class); + } + + /** + * Set the algorithm of every table constraint of arity greater than 2. + * + * @param algo e.g. "CT+", "STR2+", "GAC3rm", "MDD+", "FC" (see {@code IIntConstraintFactory#table}) + */ + static Variant tableAlgorithm(String algo) { + return withOption("table", algo, IntVar[].class, Tuples.class); + } + + /** + * Set the algorithm of every binary table constraint. + * + * @param algo e.g. "CT+", "STR2+", "AC3rm", "AC2001", "FC" (see {@code IIntConstraintFactory#table}) + */ + static Variant binaryTableAlgorithm(String algo) { + return withOption("table", algo, IntVar.class, IntVar.class, Tuples.class); + } + + /** + * Rewrite the calls to a factory method which exists with and without a trailing {@code String} option (e.g. + * {@code allDifferent(IntVar[])} and {@code allDifferent(IntVar[], String)}) so that they all use + * option. + */ + private static Variant withOption(String name, String option, Class... base) { + Objects.requireNonNull(option); + FactoryMethod without = FactoryMethod.of(name, base); + Class[] withTypes = Arrays.copyOf(base, base.length + 1); + withTypes[base.length] = String.class; + FactoryMethod with = FactoryMethod.of(name, withTypes); + Arg opt = new Arg.Const(option); + return mapCalls(c -> { + boolean hasOption = c.method().equals(with); + if (!hasOption && !c.method().equals(without)) { + return c; + } + Arg[] args = c.rawArgs(); + Arg[] a = Arrays.copyOf(args, hasOption ? args.length : args.length + 1); + a[a.length - 1] = opt; + return new Step.Call(c.rawOut(), with, a); + }); + } + + //*********************************************************************************** + // CONSTRAINTS + //*********************************************************************************** + + /** + * Add steps at the end of the spec, e.g. redundant constraints or symmetry breaking constraints. + * The builder knows the identifiers of the spec (see {@link Recorder#idsOf} to get those of the variables of a + * recorded model). + */ + static Variant extend(Consumer extension) { + Objects.requireNonNull(extension); + return spec -> { + SpecBuilder b = SpecBuilder.from(spec); + extension.accept(b); + return b.build(); + }; + } + + /** + * Do not post the constraints built by the calls which satisfy filter (the calls are still replayed, + * with their side effects, e.g. intermediate variables). + */ + static Variant unpostIf(Predicate filter) { + Objects.requireNonNull(filter); + return spec -> { + BitSet removed = new BitSet(); + for (Step s : spec.steps()) { + if (s instanceof Step.Call c && filter.test(c)) { + s.forEachDef(removed::set); + } + } + List steps = new ArrayList<>(spec.steps().size()); + for (Step s : spec.steps()) { + // a constraint no longer posted cannot be unposted either + if (s instanceof Step.Post p) { + int[] kept = Arrays.stream(p.rawCstrs()).filter(c -> !removed.get(c)).toArray(); + if (kept.length > 0) { + steps.add(new Step.Post(kept)); + } + } else if (s instanceof Step.Unpost u) { + int[] kept = Arrays.stream(u.rawCstrs()).filter(c -> !removed.get(c)).toArray(); + if (kept.length > 0) { + steps.add(new Step.Unpost(kept)); + } + } else { + steps.add(s); + } + } + return spec.withSteps(steps); + }; + } +} diff --git a/solver/src/main/java/org/chocosolver/solver/variables/OptionalTask.java b/solver/src/main/java/org/chocosolver/solver/variables/OptionalTask.java index 78b161f5a7..ac9ee35efb 100644 --- a/solver/src/main/java/org/chocosolver/solver/variables/OptionalTask.java +++ b/solver/src/main/java/org/chocosolver/solver/variables/OptionalTask.java @@ -10,6 +10,7 @@ import org.chocosolver.solver.ICause; import org.chocosolver.solver.Model; import org.chocosolver.solver.exception.ContradictionException; +import org.chocosolver.solver.spec.Recorder; /** * Container representing an optional task: @@ -58,8 +59,11 @@ public OptionalTask(Model model, int est, int lst, int d, int ect, int lct) { * @param performed performed variable */ public OptionalTask(Model model, int est, int lst, int d, int ect, int lct, BoolVar performed) { - super(model, est, lst, d, ect, lct); - this.performed = performed; + this(buildVars(model, est, lst, d, ect, lct), performed); + } + + private OptionalTask(IntVar[] vars, BoolVar performed) { + this(vars[0], vars[1], vars[2], performed); } /** @@ -82,8 +86,7 @@ public OptionalTask(IntVar s, int d) { * @param performed performed variable */ public OptionalTask(IntVar s, int d, BoolVar performed) { - super(s, d); - this.performed = performed; + this(s, s.getModel().intVar(d), s.getModel().offset(s, d), performed); } /** @@ -106,8 +109,7 @@ public OptionalTask(IntVar s, IntVar d) { * @param performed performed variable */ public OptionalTask(IntVar s, IntVar d, BoolVar performed) { - super(s, d); - this.performed = performed; + this(s, d, endOf(s, d), performed); } /** @@ -132,8 +134,7 @@ public OptionalTask(IntVar s, int d, IntVar e) { * @param performed performed variable */ public OptionalTask(IntVar s, int d, IntVar e, BoolVar performed) { - super(s, d, e); - this.performed = performed; + this(s, s.getModel().intVar(d), e, performed); } /** @@ -160,6 +161,13 @@ public OptionalTask(IntVar s, IntVar d, IntVar e) { public OptionalTask(IntVar s, IntVar d, IntVar e, BoolVar performed) { super(s, d, e); this.performed = performed; + // every constructor ends here: journalize the creation of this task, if its model is recorded + if (getClass() == OptionalTask.class) { + Recorder r = s.getModel().getRecorder(); + if (r != null) { + r.newTask(this, s, d, e, performed); + } + } } //*********************************************************************************** diff --git a/solver/src/main/java/org/chocosolver/solver/variables/Task.java b/solver/src/main/java/org/chocosolver/solver/variables/Task.java index 3f85ec41b2..02204fcb57 100644 --- a/solver/src/main/java/org/chocosolver/solver/variables/Task.java +++ b/solver/src/main/java/org/chocosolver/solver/variables/Task.java @@ -14,6 +14,7 @@ import org.chocosolver.solver.constraints.Propagator; import org.chocosolver.solver.constraints.PropagatorPriority; import org.chocosolver.solver.exception.ContradictionException; +import org.chocosolver.solver.spec.Recorder; import org.chocosolver.solver.variables.events.PropagatorEventType; import org.chocosolver.solver.variables.view.integer.IntAffineView; import org.chocosolver.util.ESat; @@ -61,7 +62,7 @@ public Task(Model model, int est, int lst, int d, int ect, int lct) { this(buildVars(model, est, lst, d, ect, lct)); } - private static IntVar[] buildVars(Model model, int est, int lst, int d, int ect, int lct) { + static IntVar[] buildVars(Model model, int est, int lst, int d, int ect, int lct) { IntVar start = model.intVar(Math.max(est, ect - d), Math.min(lst, lct - d)); IntVar duration = model.intVar(d); IntVar end = start.getModel().offset(start, d); @@ -87,12 +88,15 @@ public Task(IntVar s, int d) { * @param d duration value */ public Task(IntVar s, IntVar d) { - this( - s, - d, - d.isInstantiated() ? s.getModel().offset(s, d.getValue()) - : s.getModel().intVar(s.getLB() + d.getLB(), s.getUB() + d.getUB()) - ); + this(s, d, endOf(s, d)); + } + + /** + * @return the end variable of a task of start s and duration d + */ + static IntVar endOf(IntVar s, IntVar d) { + return d.isInstantiated() ? s.getModel().offset(s, d.getValue()) + : s.getModel().intVar(s.getLB() + d.getLB(), s.getUB() + d.getUB()); } /** @@ -124,6 +128,12 @@ public Task(IntVar s, IntVar d, IntVar e) { setActive(); setPassive(); } + if (getClass() == Task.class) { + Recorder r = s.getModel().getRecorder(); + if (r != null) { + r.newTask(this, s, d, e, null); + } + } } public void post() { diff --git a/solver/src/main/java/org/chocosolver/util/objects/graphs/MultivaluedDecisionDiagram.java b/solver/src/main/java/org/chocosolver/util/objects/graphs/MultivaluedDecisionDiagram.java index 36c3c458f5..1843126adb 100644 --- a/solver/src/main/java/org/chocosolver/util/objects/graphs/MultivaluedDecisionDiagram.java +++ b/solver/src/main/java/org/chocosolver/util/objects/graphs/MultivaluedDecisionDiagram.java @@ -9,6 +9,7 @@ import gnu.trove.list.array.TIntArrayList; import gnu.trove.map.hash.TIntIntHashMap; import org.chocosolver.solver.constraints.extension.Tuples; +import org.chocosolver.solver.exception.SolverException; import org.chocosolver.solver.variables.IntVar; import java.util.ArrayList; @@ -80,6 +81,10 @@ public enum Compact { private final Compact compact; private final boolean sortTuples; + /** + * Once frozen, the diagram cannot be modified anymore and can be safely shared among models. + */ + private volatile boolean frozen; // TEMPORARY DATA STRUCTURE, PREFIX WITH "_", CLEARED AFTER USAGE private TIntIntHashMap _nodesToRemove; // store the nodes to remove and the size of each node @@ -208,6 +213,26 @@ private void init(Tuples TUPLES) { } } + /** + * Freeze this diagram: any further modification will throw a {@link SolverException}. + * A frozen diagram can be safely shared among models solved concurrently. + * Freezing is irreversible and idempotent. + * + * @return this + */ + public MultivaluedDecisionDiagram freeze() { + this.frozen = true; + return this; + } + + /** + * @return true if this diagram is frozen + * @see #freeze() + */ + public boolean isFrozen() { + return frozen; + } + /** * Add all tuples within the MDD * @@ -228,6 +253,9 @@ public boolean addTuples(Tuples TUPLES) { * @param TUPLE tuple to add */ public boolean addTuple(int[] TUPLE) { + if (frozen) { + throw new SolverException("Cannot modify a frozen diagram"); + } for (int i = 0; i < nbLayers; i++) { // if the tuple is out of declared domain if (TUPLE[i] < offsets[i] || TUPLE[i] >= offsets[i] + sizes[i]) { diff --git a/solver/src/test/java/org/chocosolver/solver/spec/CustomConstraintTest.java b/solver/src/test/java/org/chocosolver/solver/spec/CustomConstraintTest.java new file mode 100644 index 0000000000..b74a4aad20 --- /dev/null +++ b/solver/src/test/java/org/chocosolver/solver/spec/CustomConstraintTest.java @@ -0,0 +1,119 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.Model; +import org.chocosolver.solver.constraints.Constraint; +import org.chocosolver.solver.constraints.Propagator; +import org.chocosolver.solver.exception.ContradictionException; +import org.chocosolver.solver.variables.IntVar; +import org.chocosolver.util.ESat; +import org.testng.Assert; +import org.testng.annotations.Test; + +import java.util.Arrays; + +/** + * Tests of the custom constraints ({@code Model.custom}) built with parameters. + * + * @author Charles Prud'homme + */ +public class CustomConstraintTest { + + /** + * A custom propagator with parameters: each variable is at most its bound. + */ + static final class PropUpperBounds extends Propagator { + final int[] bounds; + + PropUpperBounds(IntVar[] vars, int[] bounds) { + super(vars); + this.bounds = bounds; + } + + @Override + public void propagate(int evtmask) throws ContradictionException { + for (int i = 0; i < vars.length; i++) { + vars[i].updateUpperBound(bounds[i], this); + } + } + + @Override + public ESat isEntailed() { + boolean all = true; + for (int i = 0; i < vars.length; i++) { + if (vars[i].getLB() > bounds[i]) { + return ESat.FALSE; + } + all &= vars[i].getUB() <= bounds[i]; + } + return all ? ESat.TRUE : ESat.UNDEFINED; + } + } + + /** + * Several parameters, in a record. + */ + record Bounds(int[] ub, int shift) { + } + + /** + * A record which holds a variable: not supported, variables must be passed in {@code vars}. + */ + record WithVar(IntVar var) { + } + + private static PropUpperBounds of(IntVar[] vs, Bounds b) { + return new PropUpperBounds(vs, Arrays.stream(b.ub()).map(u -> u + b.shift()).toArray()); + } + + private static Model build(Model m) { + IntVar[] x = m.intVarArray("x", 3, 0, 9); + m.custom("int", x, 7, (vs, k) -> new PropUpperBounds(vs, new int[]{k, k, k})).post(); + m.custom("array", x, new int[]{6, 5, 8}, PropUpperBounds::new).post(); + m.custom("record", x, new Bounds(new int[]{3, 7, 7}, 1), CustomConstraintTest::of).post(); + // data holding variables: mapped to those of each copy + m.custom("vars", new IntVar[]{x[0]}, new IntVar[]{x[1], x[2]}, + (vs, ws) -> new PropUpperBounds(new IntVar[]{vs[0], ws[0], ws[1]}, new int[]{9, 9, 9})).post(); + m.sum(x, "=", 14).post(); + return m; + } + + private static int[] bounds(Model m, String name) { + Constraint c = Arrays.stream(m.getCstrs()).filter(k -> k.getName().equals(name)).findFirst().orElseThrow(); + return ((PropUpperBounds) c.getPropagator(0)).bounds; + } + + @Test(groups = "1s", timeOut = 60000) + public void testParametersAreReplayed() { + String expected = SpecTestUtils.structure(build(new Model("m"))); + String stats = SpecTestUtils.solve(build(new Model("m")), 100_000); + Model original = build(Model.record("m")); + ModelSpec spec = original.getRecorder().snapshot(); + Model a = spec.instantiate().model(); + Model b = spec.instantiate().model(); + for (Model m : new Model[]{a, b}) { + Assert.assertEquals(SpecTestUtils.structure(m), expected); + Assert.assertEquals(bounds(m, "int"), new int[]{7, 7, 7}); + Assert.assertEquals(bounds(m, "array"), new int[]{6, 5, 8}); + Assert.assertEquals(bounds(m, "record"), new int[]{4, 8, 8}); + } + // mutable data are not shared + Assert.assertNotSame(bounds(a, "array"), bounds(original, "array")); + Assert.assertNotSame(bounds(a, "array"), bounds(b, "array")); + Assert.assertEquals(SpecTestUtils.solve(a, 100_000), stats); + Assert.assertEquals(SpecTestUtils.solve(original, 100_000), stats); + } + + @Test(groups = "1s", timeOut = 60000) + public void testRecordOfVariablesIsReported() { + Model m = Model.record("m"); + IntVar[] x = m.intVarArray("x", 2, 0, 3); + m.custom("withVar", x, new WithVar(x[0]), (vs, w) -> new PropUpperBounds(vs, new int[]{3, 3})).post(); + Assert.assertThrows(SpecException.class, m::duplicate); + } +} diff --git a/solver/src/test/java/org/chocosolver/solver/spec/IntFactoryCoverageTest.java b/solver/src/test/java/org/chocosolver/solver/spec/IntFactoryCoverageTest.java new file mode 100644 index 0000000000..b2ce78bea4 --- /dev/null +++ b/solver/src/test/java/org/chocosolver/solver/spec/IntFactoryCoverageTest.java @@ -0,0 +1,683 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.IModel; +import org.chocosolver.solver.Model; +import org.chocosolver.solver.Settings; +import org.chocosolver.solver.SettingsBuilder; +import org.chocosolver.solver.constraints.Constraint; +import org.chocosolver.solver.constraints.binary.PropGreaterOrEqualX_Y; +import org.chocosolver.solver.constraints.ISchedulingFactory; +import org.chocosolver.solver.constraints.extension.Tuples; +import org.chocosolver.solver.constraints.extension.hybrid.HybridTuples; +import org.chocosolver.solver.constraints.nary.alldifferent.conditions.Condition; +import org.chocosolver.solver.constraints.nary.automata.FA.CostAutomaton; +import org.chocosolver.solver.constraints.nary.automata.FA.FiniteAutomaton; +import org.chocosolver.solver.constraints.nary.circuit.CircuitConf; +import org.chocosolver.solver.constraints.nary.cnf.LogOp; +import org.chocosolver.solver.variables.BoolVar; +import org.chocosolver.solver.variables.IntVar; +import org.chocosolver.solver.variables.Task; +import org.chocosolver.solver.variables.Variable; +import org.chocosolver.util.objects.graphs.MultivaluedDecisionDiagram; +import org.chocosolver.util.objects.setDataStructures.iterable.IntIterableRangeSet; +import org.testng.Assert; +import org.testng.SkipException; +import org.testng.annotations.DataProvider; +import org.testng.annotations.Test; + +import java.lang.reflect.Method; +import java.lang.reflect.Modifier; +import java.lang.reflect.Type; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; +import java.util.Set; +import java.util.TreeSet; +import java.util.function.Consumer; +import java.util.function.Function; +import java.util.stream.Collectors; + +/** + * Exhaustive check that the factory methods of {@link IModel} dealing only with integer and boolean variables + * (variables, views, constraints, reifications, clauses, decompositions, tasks) are supported by + * {@link ModelSpec}: each one is called by a case, and each case built directly, recorded then replayed gives + * the same structure and the same search (all solutions). Constraints are also checked reified. + *

+ * {@link #testEveryIntFactoryMethodIsCovered()} fails if a factory method of the scope is called by no case: add + * a case when adding a factory method. + * + * @author Charles Prud'homme + */ +public class IntFactoryCoverageTest { + + /** + * Factory methods not implemented by the solver (they always throw an exception). + */ + private static final Set NOT_IMPLEMENTED = Set.of("addTable(IntVar[],HybridTuples)"); + + /** + * Types out of the scope (set, real and graph variables and constraints). + */ + private static final List OUT_OF_SCOPE = List.of("SetVar", "RealVar", "GraphVar", "DirectedGraph", + "UndirectedGraph", "ISet", "IGraph", "RealConstraint", "NodeInduced"); + + private record Case(String name, Consumer body) { + @Override + public String toString() { + return name; + } + } + + private static final List CASES = new ArrayList<>(); + + /** + * A case which posts the constraint, and a case which reifies it. + */ + private static void c(String name, Function f) { + CASES.add(new Case(name, m -> f.apply(m).post())); + CASES.add(new Case(name + " [reified]", m -> f.apply(m).reify())); + } + + /** + * A case which runs f. + */ + private static void s(String name, Consumer f) { + CASES.add(new Case(name, f)); + } + + private static IntVar[] x(Model m, int n, int lb, int ub) { + return m.intVarArray("x", n, lb, ub); + } + + private static IntVar v(Model m, String name, int lb, int ub) { + return m.intVar(name, lb, ub); + } + + private static BoolVar[] b(Model m, int n) { + return m.boolVarArray("b", n); + } + + private static int[] ints(int... values) { + return values; + } + + /** + * Post a unary cumulative over the tasks, so that they matter. + */ + private static void cum(Model m, Task... tasks) { + IntVar[] h = new IntVar[tasks.length]; + Arrays.fill(h, m.intVar(1)); + m.cumulative(tasks, h, m.intVar(1)).post(); + } + + private static Tuples tuples(boolean feasible, int[]... ts) { + Tuples t = new Tuples(feasible); + t.add(ts); + return t; + } + + /** + * The numbering of the states of an automaton built from a regular expression is not deterministic (it + * depends on identity hash codes): the direct and the recorded models of a case must share the automaton. + */ + private static final FiniteAutomaton AUTOMATON = new FiniteAutomaton("0*1*2*"); + + private static FiniteAutomaton automaton() { + return AUTOMATON; + } + + private static Task[] tasks(Model m, int n) { + Task[] ts = new Task[n]; + for (int i = 0; i < n; i++) { + ts[i] = m.taskVar(v(m, "s" + i, 0, 3), 1 + (i % 2)); + } + return ts; + } + + static { + // ---------------------------------------------------------------- variables + s("boolVar()", m -> m.boolVar()); + s("boolVar(String)", m -> m.boolVar("b")); + s("boolVar(String,boolean)", m -> m.arithm(m.boolVar("t", true), "=", m.boolVar("b")).post()); + s("boolVar(boolean)", m -> m.arithm(m.boolVar(false), "=", m.boolVar("b")).post()); + s("boolVarArray(String,int)", m -> m.boolVarArray("b", 3)); + s("boolVarArray(int)", m -> m.boolVarArray(3)); + s("boolVarMatrix(String,int,int)", m -> m.boolVarMatrix("b", 2, 2)); + s("boolVarMatrix(int,int)", m -> m.boolVarMatrix(2, 2)); + s("generateName()", m -> { + m.generateName(); + m.boolVar(); + }); + s("generateName(String)", m -> { + m.generateName("X_"); + m.intVar(0, 2); + }); + s("intVar(IntVar)", m -> m.intVar(m.intVar("x", new int[]{1, 3, 5}))); + s("intVar(String,IntVar)", m -> m.intVar("y", v(m, "x", 0, 3))); + s("intVar(String,int)", m -> m.arithm(m.intVar("c", 7), ">", v(m, "x", 5, 9)).post()); + s("intVar(String,int,int)", m -> m.intVar("x", 0, 3)); + s("intVar(String,int,int,boolean)", m -> m.intVar("x", 0, 3, true)); + s("intVar(String,int[])", m -> m.intVar("x", new int[]{1, 4, 6})); + s("intVar(int)", m -> m.arithm(m.intVar(4), ">", v(m, "x", 2, 6)).post()); + s("intVar(int,int)", m -> m.intVar(0, 3)); + s("intVar(int,int,boolean)", m -> m.intVar(0, 3, false)); + s("intVar(int[])", m -> m.intVar(new int[]{2, 5})); + s("intVarArray(String,int,int,int)", m -> m.intVarArray("x", 2, 0, 2)); + s("intVarArray(String,int,int,int,boolean)", m -> m.intVarArray("x", 2, 0, 2, true)); + s("intVarArray(String,int,int[])", m -> m.intVarArray("x", 2, new int[]{1, 3})); + s("intVarArray(int,int,int)", m -> m.intVarArray(2, 0, 2)); + s("intVarArray(int,int,int,boolean)", m -> m.intVarArray(2, 0, 2, false)); + s("intVarArray(int,int[])", m -> m.intVarArray(2, new int[]{1, 3})); + s("intVarMatrix(String,int,int,int,int)", m -> m.intVarMatrix("x", 2, 2, 0, 1)); + s("intVarMatrix(String,int,int,int,int,boolean)", m -> m.intVarMatrix("x", 2, 2, 0, 1, true)); + s("intVarMatrix(String,int,int,int[])", m -> m.intVarMatrix("x", 2, 2, new int[]{0, 2})); + s("intVarMatrix(int,int,int,int)", m -> m.intVarMatrix(2, 2, 0, 1)); + s("intVarMatrix(int,int,int,int,boolean)", m -> m.intVarMatrix(2, 2, 0, 1, false)); + s("intVarMatrix(int,int,int[])", m -> m.intVarMatrix(2, 2, new int[]{0, 2})); + // tasks + s("taskVar(IntVar,IntVar)", m -> cum(m, m.taskVar(v(m, "s", 0, 3), v(m, "d", 1, 2)), m.taskVar(v(m, "t", 0, 3), 1))); + s("taskVar(IntVar,IntVar,BoolVar)", m -> cum(m, m.taskVar(v(m, "s", 0, 3), v(m, "d", 1, 2), m.boolVar("p")), m.taskVar(v(m, "t", 0, 3), 1))); + s("taskVar(IntVar,IntVar,IntVar)", m -> cum(m, m.taskVar(v(m, "s", 0, 3), v(m, "d", 1, 2), v(m, "e", 1, 5)), m.taskVar(v(m, "t", 0, 3), 1))); + s("taskVar(IntVar,IntVar,IntVar,BoolVar)", m -> cum(m, m.taskVar(v(m, "s", 0, 3), v(m, "d", 1, 2), v(m, "e", 1, 5), m.boolVar("p")), m.taskVar(v(m, "t", 0, 3), 1))); + s("taskVar(IntVar,IntVar,IntVar,boolean)", m -> cum(m, m.taskVar(v(m, "s", 0, 3), v(m, "d", 1, 2), v(m, "e", 1, 5), true), m.taskVar(v(m, "t", 0, 3), 1))); + s("taskVar(IntVar,IntVar,boolean)", m -> cum(m, m.taskVar(v(m, "s", 0, 3), v(m, "d", 1, 2), true), m.taskVar(v(m, "t", 0, 3), 1))); + s("taskVar(IntVar,int)", m -> cum(m, m.taskVar(v(m, "s", 0, 3), 2), m.taskVar(v(m, "t", 0, 3), 1))); + s("taskVar(IntVar,int,BoolVar)", m -> cum(m, m.taskVar(v(m, "s", 0, 3), 2, m.boolVar("p")), m.taskVar(v(m, "t", 0, 3), 1))); + s("taskVar(IntVar,int,IntVar)", m -> cum(m, m.taskVar(v(m, "s", 0, 3), 2, v(m, "e", 2, 5)), m.taskVar(v(m, "t", 0, 3), 1))); + s("taskVar(IntVar,int,IntVar,BoolVar)", m -> cum(m, m.taskVar(v(m, "s", 0, 3), 2, v(m, "e", 2, 5), m.boolVar("p")), m.taskVar(v(m, "t", 0, 3), 1))); + s("taskVar(IntVar,int,IntVar,boolean)", m -> cum(m, m.taskVar(v(m, "s", 0, 3), 2, v(m, "e", 2, 5), true), m.taskVar(v(m, "t", 0, 3), 1))); + s("taskVar(IntVar,int,boolean)", m -> cum(m, m.taskVar(v(m, "s", 0, 3), 2, true), m.taskVar(v(m, "t", 0, 3), 1))); + s("taskVar(int,int,int,int,int)", m -> cum(m, m.taskVar(0, 3, 2, 2, 5), m.taskVar(v(m, "t", 0, 3), 1))); + s("taskVar(int,int,int,int,int,BoolVar)", m -> cum(m, m.taskVar(0, 3, 2, 2, 5, m.boolVar("p")), m.taskVar(v(m, "t", 0, 3), 1))); + s("taskVar(int,int,int,int,int,boolean)", m -> cum(m, m.taskVar(0, 3, 2, 2, 5, true), m.taskVar(v(m, "t", 0, 3), 1))); + s("taskVarArray(IntVar[],IntVar[],IntVar[])", m -> cum(m, m.taskVarArray(x(m, 2, 0, 2), m.intVarArray("d", 2, 1, 2), m.intVarArray("e", 2, 1, 4)))); + s("taskVarMatrix(IntVar[][],IntVar[][],IntVar[][])", m -> { + Task[][] t = m.taskVarMatrix(m.intVarMatrix("s", 1, 2, 0, 2), m.intVarMatrix("d", 1, 2, 1, 2), m.intVarMatrix("e", 1, 2, 1, 4)); + cum(m, t[0]); + }); + + // ---------------------------------------------------------------- views + s("abs(IntVar)", m -> m.arithm(m.abs(v(m, "x", -2, 2)), "!=", 1).post()); + s("boolNotView(BoolVar)", m -> { + BoolVar[] bs = b(m, 2); + m.arithm(m.boolNotView(bs[0]), "=", bs[1]).post(); + }); + s("intAbsView(IntVar)", m -> m.arithm(m.intAbsView(v(m, "x", -2, 2)), "!=", 1).post()); + s("intAffineView(int,IntVar,int)", m -> m.arithm(m.intAffineView(2, v(m, "x", 0, 3), 1), "!=", 3).post()); + s("intEqView(IntVar,int)", m -> m.arithm(m.intEqView(v(m, "x", 0, 3), 1), "=", 0).post()); + s("intGeView(IntVar,int)", m -> m.arithm(m.intGeView(v(m, "x", 0, 3), 2), "=", 1).post()); + s("intLeView(IntVar,int)", m -> m.arithm(m.intLeView(v(m, "x", 0, 3), 1), "=", 1).post()); + s("intMinusView(IntVar)", m -> m.arithm(m.intMinusView(v(m, "x", 0, 3)), ">", -2).post()); + s("intNeView(IntVar,int)", m -> m.arithm(m.intNeView(v(m, "x", 0, 3), 1), "=", 1).post()); + s("intOffsetView(IntVar,int)", m -> m.arithm(m.intOffsetView(v(m, "x", 0, 3), 2), "!=", 3).post()); + s("intScaleView(IntVar,int)", m -> m.arithm(m.intScaleView(v(m, "x", 0, 3), 3), "!=", 3).post()); + s("intView(int,IntVar,int)", m -> m.arithm(m.intView(2, v(m, "x", 0, 3), -1), "!=", 1).post()); + s("isEq(IntVar,int)", m -> m.arithm(m.isEq(v(m, "x", 0, 3), 1), "=", 0).post()); + s("isGeq(IntVar,int)", m -> m.arithm(m.isGeq(v(m, "x", 0, 3), 2), "=", 1).post()); + s("isLeq(IntVar,int)", m -> m.arithm(m.isLeq(v(m, "x", 0, 3), 1), "=", 1).post()); + s("isNeq(IntVar,int)", m -> m.arithm(m.isNeq(v(m, "x", 0, 3), 1), "=", 1).post()); + s("mul(IntVar,int)", m -> m.arithm(m.mul(v(m, "x", 0, 3), 2), "!=", 2).post()); + s("neg(IntVar)", m -> m.arithm(m.neg(v(m, "x", 0, 3)), ">", -2).post()); + s("offset(IntVar,int)", m -> m.arithm(m.offset(v(m, "x", 0, 3), 2), "!=", 3).post()); + + // ---------------------------------------------------------------- integer constraints + c("absolute(IntVar,IntVar)", m -> m.absolute(v(m, "y", 0, 2), v(m, "x", -2, 2))); + c("allDiffPrec(IntVar[],boolean[][])", m -> m.allDiffPrec(x(m, 3, 0, 2), new boolean[][]{{false, true, false}, {false, false, false}, {false, false, false}})); + c("allDiffPrec(IntVar[],boolean[][],String)", m -> m.allDiffPrec(x(m, 3, 0, 2), new boolean[][]{{false, true, false}, {false, false, false}, {false, false, false}}, "BESSIERE")); + c("allDiffPrec(IntVar[],int[][],int[][])", m -> m.allDiffPrec(x(m, 3, 0, 2), new int[][]{{}, {0}, {}}, new int[][]{{1}, {}, {}})); + c("allDiffPrec(IntVar[],int[][],int[][],String)", m -> m.allDiffPrec(x(m, 3, 0, 2), new int[][]{{}, {0}, {}}, new int[][]{{1}, {}, {}}, "GREEDY")); + c("allDifferent(IntVar[])", m -> m.allDifferent(x(m, 3, 0, 3))); + c("allDifferent(IntVar[],String)", m -> m.allDifferent(x(m, 3, 0, 3), "AC")); + c("allDifferentExcept0(IntVar[])", m -> m.allDifferentExcept0(x(m, 3, 0, 2))); + c("allDifferentExceptValues(IntVar[],int[])", m -> m.allDifferentExceptValues(x(m, 3, 0, 2), ints(0, 1))); + c("allDifferentUnderCondition(IntVar[],Condition,boolean)", m -> m.allDifferentUnderCondition(x(m, 3, 0, 2), Condition.EXCEPT_0, true)); + c("allDifferentUnderCondition(IntVar[],Condition,boolean,String)", m -> m.allDifferentUnderCondition(x(m, 3, 0, 2), v -> !v.contains(0), false, "AC")); + c("allEqual(IntVar[])", m -> m.allEqual(x(m, 3, 0, 2))); + c("among(IntVar,IntVar[],int[])", m -> m.among(v(m, "n", 0, 3), x(m, 3, 0, 2), ints(1, 2))); + c("and(BoolVar[])", m -> m.and(b(m, 3))); + c("and(Constraint[])", m -> { + IntVar[] x = x(m, 2, 0, 2); + return m.and(m.arithm(x[0], "<", x[1]), m.arithm(x[1], "!=", 1)); + }); + c("argmax(IntVar,int,IntVar[])", m -> m.argmax(v(m, "z", 0, 2), 0, x(m, 3, 0, 2))); + c("argmin(IntVar,int,IntVar[])", m -> m.argmin(v(m, "z", 1, 3), 1, x(m, 3, 0, 2))); + c("arithm(IntVar,String,IntVar)", m -> m.arithm(v(m, "x", 0, 3), "<", v(m, "y", 0, 3))); + c("arithm(IntVar,String,IntVar,String,IntVar)", m -> m.arithm(v(m, "x", 0, 3), "+", v(m, "y", 0, 3), "=", v(m, "z", 0, 3))); + c("arithm(IntVar,String,IntVar,String,int)", m -> m.arithm(v(m, "x", 0, 3), "-", v(m, "y", 0, 3), "<=", 1)); + c("arithm(IntVar,String,int)", m -> m.arithm(v(m, "x", 0, 3), "!=", 2)); + c("atLeastNValues(IntVar[],IntVar,boolean)", m -> m.atLeastNValues(x(m, 3, 0, 2), v(m, "n", 2, 3), true)); + c("atMostNValues(IntVar[],IntVar,boolean)", m -> m.atMostNValues(x(m, 3, 0, 2), v(m, "n", 1, 2), false)); + c("binPacking(IntVar[],int[],IntVar[],int)", m -> m.binPacking(x(m, 3, 0, 1), ints(1, 2, 2), m.intVarArray("l", 2, 0, 4), 0)); + c("bitsIntChanneling(BoolVar[],IntVar)", m -> m.bitsIntChanneling(b(m, 3), v(m, "x", 0, 7))); + c("boolsIntChanneling(BoolVar[],IntVar,int)", m -> m.boolsIntChanneling(b(m, 3), v(m, "x", 0, 2), 0)); + c("circuit(IntVar[])", m -> m.circuit(x(m, 4, 0, 3))); + c("circuit(IntVar[],int)", m -> m.circuit(x(m, 4, 1, 4), 1)); + c("circuit(IntVar[],int,CircuitConf)", m -> m.circuit(x(m, 4, 0, 3), 0, CircuitConf.RD)); + c("clausesIntChanneling(IntVar,BoolVar[],BoolVar[])", m -> m.clausesIntChanneling(v(m, "x", 0, 2), m.boolVarArray("e", 3), m.boolVarArray("l", 3))); + c("costRegular(IntVar[],IntVar,ICostAutomaton)", m -> { + int[][] costs = new int[3][3]; + for (int[] c : costs) Arrays.fill(c, 1); + costs[1][2] = 3; + return m.costRegular(x(m, 3, 0, 2), v(m, "c", 0, 5), CostAutomaton.makeSingleResource(automaton(), costs, 0, 5)); + }); + c("count(IntVar,IntVar[],IntVar)", m -> m.count(v(m, "val", 0, 2), x(m, 3, 0, 2), v(m, "n", 1, 2))); + c("count(int,IntVar[],IntVar)", m -> m.count(1, x(m, 3, 0, 2), v(m, "n", 1, 2))); + c("custom(String,Variable[],Function)", m -> m.custom("geq", x(m, 2, 0, 2), PropGreaterOrEqualX_Y::new)); + c("custom(String,Variable[],Object,BiFunction)", m -> m.custom("geq", x(m, 1, 0, 2), x(m, 1, 0, 2), (u, v) -> new PropGreaterOrEqualX_Y(new IntVar[]{u[0], v[0]}))); + c("decreasing(IntVar[],int)", m -> m.decreasing(x(m, 3, 0, 3), 1)); + c("diffN(IntVar[],IntVar[],IntVar[],IntVar[],boolean)", m -> m.diffN(m.intVarArray("x", 2, 0, 2), m.intVarArray("y", 2, 0, 2), m.intVarArray("w", 2, 1, 2), m.intVarArray("h", 2, 1, 2), true)); + c("diffN(IntVar[][],int[][])", m -> m.diffN(m.intVarMatrix("o", 2, 2, 0, 2), new int[][]{{1, 2}, {2, 1}})); + c("distance(IntVar,IntVar,String,IntVar)", m -> m.distance(v(m, "x", 0, 3), v(m, "y", 0, 3), "<", v(m, "z", 1, 2))); + c("distance(IntVar,IntVar,String,int)", m -> m.distance(v(m, "x", 0, 3), v(m, "y", 0, 3), "=", 1)); + c("div(IntVar,IntVar,IntVar)", m -> m.div(v(m, "x", 0, 6), v(m, "y", 1, 3), v(m, "z", 0, 6))); + c("element(IntVar,IntVar[],IntVar,int)", m -> m.element(v(m, "v", 0, 2), x(m, 3, 0, 2), v(m, "i", 1, 3), 1)); + c("element(IntVar,int[],IntVar)", m -> m.element(v(m, "v", 0, 5), ints(3, 1, 4, 1, 5), v(m, "i", 0, 4))); + c("element(IntVar,int[],IntVar,int)", m -> m.element(v(m, "v", 0, 5), ints(3, 1, 4, 1, 5), v(m, "i", 0, 6), 2)); + c("globalCardinality(IntVar[],int[],IntVar[],boolean)", m -> m.globalCardinality(x(m, 3, 0, 2), ints(0, 1), m.intVarArray("o", 2, 0, 3), false)); + c("globalCardinality(IntVar[],int[],IntVar[],boolean,String)", m -> m.globalCardinality(x(m, 3, 0, 2), ints(0, 1), m.intVarArray("o", 2, 0, 3), true, "AC")); + c("increasing(IntVar[],int)", m -> m.increasing(x(m, 3, 0, 3), 0)); + c("intValuePrecedeChain(IntVar[],int,int)", m -> m.intValuePrecedeChain(x(m, 4, 0, 2), 1, 2)); + c("intValuePrecedeChain(IntVar[],int[])", m -> m.intValuePrecedeChain(x(m, 4, 0, 2), ints(0, 1, 2))); + c("inverseChanneling(IntVar[],IntVar[])", m -> m.inverseChanneling(x(m, 3, 0, 2), m.intVarArray("y", 3, 0, 2))); + c("inverseChanneling(IntVar[],IntVar[],int,int)", m -> m.inverseChanneling(x(m, 3, 1, 3), m.intVarArray("y", 3, 1, 3), 1, 1)); + c("inverseChanneling(IntVar[],IntVar[],int,int,boolean)", m -> m.inverseChanneling(x(m, 3, 1, 3), m.intVarArray("y", 3, 0, 2), 0, 1, true)); + c("keySort(IntVar[][],IntVar[],IntVar[][],int)", m -> m.keySort(m.intVarMatrix("a", 3, 2, 0, 1), m.intVarArray("p", 3, 1, 3), m.intVarMatrix("s", 3, 2, 0, 1), 1)); + c("knapsack(IntVar[],IntVar,IntVar,int[],int[])", m -> m.knapsack(x(m, 3, 0, 2), v(m, "w", 0, 6), v(m, "e", 0, 10), ints(1, 2, 3), ints(2, 3, 4))); + c("lexChainLess(IntVar[][])", m -> m.lexChainLess(m.intVarMatrix("a", 3, 2, 0, 1))); + c("lexChainLessEq(IntVar[][])", m -> m.lexChainLessEq(m.intVarMatrix("a", 3, 2, 0, 1))); + c("lexLess(IntVar[],IntVar[])", m -> m.lexLess(x(m, 2, 0, 2), m.intVarArray("y", 2, 0, 2))); + c("lexLessEq(IntVar[],IntVar[])", m -> m.lexLessEq(x(m, 2, 0, 2), m.intVarArray("y", 2, 0, 2))); + c("max(BoolVar,BoolVar[])", m -> m.max(m.boolVar("m"), b(m, 3))); + c("max(IntVar,IntVar,IntVar)", m -> m.max(v(m, "m", 0, 3), v(m, "x", 0, 3), v(m, "y", 0, 3))); + c("max(IntVar,IntVar[])", m -> m.max(v(m, "m", 0, 3), x(m, 3, 0, 3))); + c("mddc(IntVar[],MultivaluedDecisionDiagram)", m -> { + IntVar[] x = x(m, 3, 0, 2); + return m.mddc(x, new MultivaluedDecisionDiagram(x, tuples(true, ints(0, 1, 2), ints(1, 1, 1), ints(2, 0, 1)))); + }); + c("member(IntVar,IntIterableRangeSet)", m -> m.member(v(m, "x", 0, 5), new IntIterableRangeSet(ints(1, 3, 4)))); + c("member(IntVar,int,int)", m -> m.member(v(m, "x", 0, 5), 2, 4)); + c("member(IntVar,int[])", m -> m.member(v(m, "x", 0, 5), ints(1, 5))); + c("min(BoolVar,BoolVar[])", m -> m.min(m.boolVar("m"), b(m, 3))); + c("min(IntVar,IntVar,IntVar)", m -> m.min(v(m, "m", 0, 3), v(m, "x", 0, 3), v(m, "y", 0, 3))); + c("min(IntVar,IntVar[])", m -> m.min(v(m, "m", 0, 3), x(m, 3, 0, 3))); + c("mod(IntVar,IntVar,IntVar)", m -> m.mod(v(m, "x", 0, 6), v(m, "y", 1, 3), v(m, "z", 0, 2))); + c("mod(IntVar,int,IntVar)", m -> m.mod(v(m, "x", 0, 6), 3, v(m, "z", 0, 2))); + c("mod(IntVar,int,int)", m -> m.mod(v(m, "x", 0, 6), 3, 1)); + c("multiCostRegular(IntVar[],IntVar[],ICostAutomaton)", m -> { + int[][][] costs = new int[3][3][2]; + for (int[][] l : costs) for (int[] c : l) Arrays.fill(c, 1); + return m.multiCostRegular(x(m, 3, 0, 2), m.intVarArray("c", 2, 0, 3), CostAutomaton.makeMultiResources(automaton(), costs, ints(0, 0), ints(3, 3))); + }); + c("multiCostRegular(IntVar[],IntVar[],ICostAutomaton,double)", m -> { + int[][][] costs = new int[3][3][2]; + for (int[][] l : costs) for (int[] c : l) Arrays.fill(c, 1); + return m.multiCostRegular(x(m, 3, 0, 2), m.intVarArray("c", 2, 0, 3), CostAutomaton.makeMultiResources(automaton(), costs, ints(0, 0), ints(3, 3)), 1e-4); + }); + c("nValues(IntVar[],IntVar)", m -> m.nValues(x(m, 3, 0, 2), v(m, "n", 1, 2))); + c("not(Constraint)", m -> m.not(m.arithm(v(m, "x", 0, 3), "=", 1))); + c("notAllEqual(IntVar[])", m -> m.notAllEqual(x(m, 3, 0, 1))); + c("notMember(IntVar,IntIterableRangeSet)", m -> m.notMember(v(m, "x", 0, 5), new IntIterableRangeSet(ints(1, 3, 4)))); + c("notMember(IntVar,int,int)", m -> m.notMember(v(m, "x", 0, 5), 2, 4)); + c("notMember(IntVar,int[])", m -> m.notMember(v(m, "x", 0, 5), ints(1, 5))); + c("or(BoolVar[])", m -> m.or(b(m, 3))); + c("or(Constraint[])", m -> { + IntVar[] x = x(m, 2, 0, 2); + return m.or(m.arithm(x[0], "<", x[1]), m.arithm(x[1], "=", 0)); + }); + c("path(IntVar[],IntVar,IntVar)", m -> m.path(x(m, 4, 0, 4), v(m, "s", 0, 3), v(m, "e", 0, 3))); + c("path(IntVar[],IntVar,IntVar,int)", m -> m.path(x(m, 4, 1, 5), v(m, "s", 1, 4), v(m, "e", 1, 4), 1)); + c("pow(IntVar,IntVar,IntVar)", m -> m.pow(v(m, "b", 0, 2), v(m, "e", 0, 2), v(m, "r", 0, 4))); + c("pow(IntVar,int,IntVar)", m -> m.pow(v(m, "b", -2, 2), 2, v(m, "r", 0, 4))); + c("regular(IntVar[],IAutomaton)", m -> m.regular(x(m, 3, 0, 2), automaton())); + c("scalar(IntVar[],int[],String,IntVar)", m -> m.scalar(x(m, 3, 0, 2), ints(1, 2, 3), "<=", v(m, "s", 0, 6))); + c("scalar(IntVar[],int[],String,IntVar,int)", m -> m.scalar(x(m, 3, 0, 2), ints(1, 2, 3), "=", v(m, "s", 0, 6), 2)); + c("scalar(IntVar[],int[],String,int)", m -> m.scalar(x(m, 3, 0, 2), ints(1, 2, 3), "=", 4)); + c("scalar(IntVar[],int[],String,int,int)", m -> m.scalar(x(m, 3, 0, 2), ints(1, -2, 3), ">=", 2, 2)); + c("sort(IntVar[],IntVar[])", m -> m.sort(x(m, 3, 0, 2), m.intVarArray("y", 3, 0, 2))); + c("square(IntVar,IntVar)", m -> m.square(v(m, "y", 0, 9), v(m, "x", -3, 3))); + c("subCircuit(IntVar[],int,IntVar)", m -> m.subCircuit(x(m, 4, 0, 3), 0, v(m, "l", 0, 4))); + c("subPath(IntVar[],IntVar,IntVar,int,IntVar)", m -> m.subPath(x(m, 4, 0, 4), v(m, "s", 0, 3), v(m, "e", 0, 3), 0, v(m, "l", 1, 4))); + c("sum(BoolVar[],String,IntVar)", m -> m.sum(b(m, 3), "=", v(m, "s", 0, 2))); + c("sum(BoolVar[],String,IntVar,int)", m -> m.sum(b(m, 3), "<=", v(m, "s", 0, 2), 2)); + c("sum(BoolVar[],String,int)", m -> m.sum(b(m, 3), "=", 2)); + c("sum(IntVar[],String,IntVar)", m -> m.sum(x(m, 3, 0, 2), "=", v(m, "s", 0, 6))); + c("sum(IntVar[],String,IntVar,int)", m -> m.sum(x(m, 3, 0, 2), "<", v(m, "s", 0, 6), 2)); + c("sum(IntVar[],String,IntVar[])", m -> m.sum(x(m, 2, 0, 2), "=", m.intVarArray("y", 2, 0, 2))); + c("sum(IntVar[],String,int)", m -> m.sum(x(m, 3, 0, 2), "=", 3)); + c("sum(IntVar[],String,int,int)", m -> m.sum(x(m, 3, 0, 2), "!=", 3, 2)); + c("table(IntVar,IntVar,Tuples)", m -> m.table(v(m, "x", 0, 2), v(m, "y", 0, 2), tuples(true, ints(0, 1), ints(1, 2), ints(2, 2)))); + c("table(IntVar,IntVar,Tuples,String)", m -> m.table(v(m, "x", 0, 2), v(m, "y", 0, 2), tuples(false, ints(0, 1), ints(1, 2)), "AC3")); + c("table(IntVar[],HybridTuples)", m -> { + HybridTuples h = new HybridTuples(); + h.add(HybridTuples.eq(1), HybridTuples.any(), HybridTuples.ge(1)); + h.add(HybridTuples.ne(1), HybridTuples.col(0), HybridTuples.lt(2)); + return m.table(x(m, 3, 0, 2), h); + }); + c("table(IntVar[],Tuples)", m -> m.table(x(m, 3, 0, 2), tuples(true, ints(0, 1, 2), ints(1, 1, 1), ints(2, 0, 1)))); + c("table(IntVar[],Tuples,String)", m -> m.table(x(m, 3, 0, 2), tuples(true, ints(0, 1, 2), ints(1, 1, 1), ints(2, 0, 1)), "STR2+")); + c("times(IntVar,IntVar,IntVar)", m -> m.times(v(m, "x", -2, 2), v(m, "y", 0, 2), v(m, "z", -4, 4))); + c("times(IntVar,IntVar,int)", m -> m.times(v(m, "x", 0, 3), v(m, "y", 0, 3), 2)); + c("times(IntVar,int,IntVar)", m -> m.times(v(m, "x", 0, 3), 2, v(m, "z", 0, 6))); + c("tree(IntVar[],IntVar)", m -> m.tree(x(m, 4, 0, 3), v(m, "n", 1, 2))); + c("tree(IntVar[],IntVar,int)", m -> m.tree(x(m, 4, 1, 4), v(m, "n", 1, 2), 1)); + s("conditional(Variable[],Function,Supplier) [unsupported by design]", m -> { + IntVar[] x = x(m, 2, 0, 2); + m.conditional(x, vs -> vs[0].isInstantiated(), () -> new Constraint[]{m.arithm(x[0], "!=", x[1])}); + }); + + // ---------------------------------------------------------------- decompositions + s("allDifferentExceptDec(IntVar[],int[])", m -> m.allDifferentExceptDec(x(m, 3, 0, 2), ints(0))); + s("allDifferentExceptDecWithGCC(IntVar[],int[])", m -> m.allDifferentExceptDecWithGCC(x(m, 3, 0, 2), ints(0))); + s("amongDec(IntVar,IntVar[],IntVar[])", m -> m.amongDec(v(m, "n", 0, 3), x(m, 3, 0, 2), new IntVar[]{m.intVar(1), m.intVar(2)})); + s("argmaxDec(IntVar,int,IntVar[])", m -> m.argmaxDec(v(m, "z", 0, 2), 0, x(m, 3, 0, 2))); + s("argminDec(IntVar,int,IntVar[])", m -> m.argminDec(v(m, "z", 0, 2), 0, x(m, 3, 0, 2))); + s("binPackingDec(IntVar[],int[],IntVar[],int)", m -> m.binPackingDec(x(m, 3, 0, 1), ints(1, 2, 2), m.intVarArray("l", 2, 0, 4), 0)); + s("circuitDec(IntVar[],int)", m -> m.circuitDec(x(m, 4, 0, 3), 0)); + s("costFlow(int[],int[],int[],int[],IntVar[],IntVar,int)", m -> m.costFlow(ints(0, 1, 0), ints(1, 2, 2), ints(1, 0, -1), ints(1, 1, 3), m.intVarArray("f", 3, 0, 1), v(m, "c", 0, 5), 0)); + s("cumulativeDec(IntVar[],IntVar[],IntVar[],IntVar)", m -> m.cumulativeDec(x(m, 2, 0, 2), m.intVarArray("d", 2, 1, 2), m.intVarArray("h", 2, 1, 1), v(m, "c", 1, 1))); + s("cumulativeDec(Task[],IntVar[],IntVar)", m -> m.cumulativeDec(tasks(m, 2), m.intVarArray("h", 2, 1, 1), v(m, "c", 1, 1))); + s("cumulativeTimeDec(IntVar[],int[],int[],int)", m -> m.cumulativeTimeDec(x(m, 2, 0, 2), ints(1, 2), ints(1, 1), 1)); + s("disjunctiveDec(Task[],boolean)", m -> m.disjunctiveDec(tasks(m, 2), true)); + s("element(IntVar,IntVar[][],IntVar,int,IntVar,int)", m -> m.element(v(m, "v", 0, 2), m.intVarMatrix("t", 2, 2, 0, 2), v(m, "r", 0, 1), 0, v(m, "c", 1, 2), 1)); + s("element(IntVar,int[][],IntVar,int,IntVar,int)", m -> m.element(v(m, "v", 0, 5), new int[][]{{1, 2}, {3, 4}}, v(m, "r", 0, 1), 0, v(m, "c", 0, 1), 0)); + s("globalCardinalityDec(IntVar[],IntVar[],IntVar[],boolean)", m -> m.globalCardinalityDec(x(m, 3, 0, 2), new IntVar[]{m.intVar(0), m.intVar(1)}, m.intVarArray("o", 2, 0, 3), false)); + s("ifThenElseDec(BoolVar[],IntVar[],IntVar)", m -> m.ifThenElseDec(b(m, 2), x(m, 2, 0, 2), v(m, "y", 0, 2))); + s("ifThenElseDec(BoolVar[],int[],IntVar)", m -> m.ifThenElseDec(b(m, 2), ints(1, 2), v(m, "y", 0, 2))); + s("intValuePrecedeChainDec(IntVar[],int,int)", m -> m.intValuePrecedeChainDec(x(m, 4, 0, 2), 1, 2)); + s("intValuePrecedeChainDec(IntVar[],int[])", m -> m.intValuePrecedeChainDec(x(m, 4, 0, 2), ints(0, 1, 2))); + s("product(BoolVar[][],BoolVar[][],BoolVar[][])", m -> m.product(m.boolVarMatrix("a", 2, 2), m.boolVarMatrix("b", 2, 2), m.boolVarMatrix("c", 2, 2))); + s("product(IntVar[][],IntVar[][],IntVar[][])", m -> m.product(m.intVarMatrix("a", 2, 2, 0, 1), m.intVarMatrix("b", 2, 2, 0, 1), m.intVarMatrix("c", 2, 2, 0, 2))); + s("regularDec(IntVar[],IAutomaton)", m -> m.regularDec(x(m, 3, 0, 2), automaton())); + + // ---------------------------------------------------------------- reifications + s("ifOnlyIf(Constraint,Constraint)", m -> { + IntVar[] x = x(m, 2, 0, 2); + m.ifOnlyIf(m.arithm(x[0], "=", 1), m.arithm(x[1], ">", 0)); + }); + s("ifThen(BoolVar,Constraint)", m -> m.ifThen(m.boolVar("b"), m.arithm(v(m, "x", 0, 2), "=", 1))); + s("ifThen(Constraint,Constraint)", m -> { + IntVar[] x = x(m, 2, 0, 2); + m.ifThen(m.arithm(x[0], "=", 1), m.arithm(x[1], ">", 0)); + }); + s("ifThenElse(BoolVar,Constraint,Constraint)", m -> { + IntVar x = v(m, "x", 0, 2); + m.ifThenElse(m.boolVar("b"), m.arithm(x, "=", 1), m.arithm(x, "=", 2)); + }); + s("ifThenElse(Constraint,Constraint,Constraint)", m -> { + IntVar[] x = x(m, 2, 0, 2); + m.ifThenElse(m.arithm(x[0], "=", 1), m.arithm(x[1], ">", 0), m.arithm(x[1], "=", 0)); + }); + s("impXrelC(IntVar,String,int,BoolVar)", m -> m.impXrelC(v(m, "x", 0, 3), "<", 2, m.boolVar("b"))); + s("impXrelYC(IntVar,String,IntVar,int,BoolVar)", m -> m.impXrelYC(v(m, "x", 0, 3), "<=", v(m, "y", 0, 3), 1, m.boolVar("b"))); + s("reifXrelC(IntVar,String,int,BoolVar)", m -> m.reifXrelC(v(m, "x", 0, 3), ">=", 1, m.boolVar("b"))); + s("reifXrelYC(IntVar,String,IntVar,int,BoolVar)", m -> m.reifXrelYC(v(m, "x", 0, 3), "=", v(m, "y", 0, 3), 1, m.boolVar("b"))); + s("reification(BoolVar,Constraint)", m -> m.reification(m.boolVar("b"), m.arithm(v(m, "x", 0, 3), "=", 1))); + s("reifyXeqC(IntVar,int,BoolVar)", m -> m.reifyXeqC(v(m, "x", 0, 3), 1, m.boolVar("b"))); + s("reifyXeqY(IntVar,IntVar,BoolVar)", m -> m.reifyXeqY(v(m, "x", 0, 3), v(m, "y", 0, 3), m.boolVar("b"))); + s("reifyXeqYC(IntVar,IntVar,int,BoolVar)", m -> m.reifyXeqYC(v(m, "x", 0, 3), v(m, "y", 0, 3), 1, m.boolVar("b"))); + s("reifyXgeY(IntVar,IntVar,BoolVar)", m -> m.reifyXgeY(v(m, "x", 0, 3), v(m, "y", 0, 3), m.boolVar("b"))); + s("reifyXgtC(IntVar,int,BoolVar)", m -> m.reifyXgtC(v(m, "x", 0, 3), 1, m.boolVar("b"))); + s("reifyXgtY(IntVar,IntVar,BoolVar)", m -> m.reifyXgtY(v(m, "x", 0, 3), v(m, "y", 0, 3), m.boolVar("b"))); + s("reifyXgtYC(IntVar,IntVar,int,BoolVar)", m -> m.reifyXgtYC(v(m, "x", 0, 3), v(m, "y", 0, 3), 1, m.boolVar("b"))); + s("reifyXinS(IntVar,IntIterableRangeSet,BoolVar)", m -> m.reifyXinS(v(m, "x", 0, 5), new IntIterableRangeSet(ints(1, 4)), m.boolVar("b"))); + s("reifyXleY(IntVar,IntVar,BoolVar)", m -> m.reifyXleY(v(m, "x", 0, 3), v(m, "y", 0, 3), m.boolVar("b"))); + s("reifyXltC(IntVar,int,BoolVar)", m -> m.reifyXltC(v(m, "x", 0, 3), 2, m.boolVar("b"))); + s("reifyXltY(IntVar,IntVar,BoolVar)", m -> m.reifyXltY(v(m, "x", 0, 3), v(m, "y", 0, 3), m.boolVar("b"))); + s("reifyXltYC(IntVar,IntVar,int,BoolVar)", m -> m.reifyXltYC(v(m, "x", 0, 3), v(m, "y", 0, 3), 1, m.boolVar("b"))); + s("reifyXneC(IntVar,int,BoolVar)", m -> m.reifyXneC(v(m, "x", 0, 3), 1, m.boolVar("b"))); + s("reifyXneY(IntVar,IntVar,BoolVar)", m -> m.reifyXneY(v(m, "x", 0, 3), v(m, "y", 0, 3), m.boolVar("b"))); + s("reifyXneYC(IntVar,IntVar,int,BoolVar)", m -> m.reifyXneYC(v(m, "x", 0, 3), v(m, "y", 0, 3), 1, m.boolVar("b"))); + s("reifyXnotinS(IntVar,IntIterableRangeSet,BoolVar)", m -> m.reifyXnotinS(v(m, "x", 0, 5), new IntIterableRangeSet(ints(1, 4)), m.boolVar("b"))); + + // ---------------------------------------------------------------- result variables + s("argmax(String,IntVar[])", m -> m.arithm(m.argmax("a", x(m, 3, 0, 2)), "!=", 1).post()); + s("argmin(String,IntVar[])", m -> m.arithm(m.argmin("a", x(m, 3, 0, 2)), "!=", 1).post()); + s("count(String,IntVar,IntVar[])", m -> m.arithm(m.count("c", v(m, "v", 0, 2), x(m, 3, 0, 2)), ">", 1).post()); + s("count(String,int,IntVar[])", m -> m.arithm(m.count("c", 1, x(m, 3, 0, 2)), ">", 1).post()); + s("element(String,IntVar[],IntVar,int)", m -> m.arithm(m.element("e", x(m, 3, 0, 2), v(m, "i", 1, 3), 1), "!=", 1).post()); + s("element(String,int[],IntVar)", m -> m.arithm(m.element("e", ints(3, 1, 4), v(m, "i", 0, 2)), "!=", 1).post()); + s("element(String,int[],IntVar,int)", m -> m.arithm(m.element("e", ints(3, 1, 4), v(m, "i", 1, 3), 1), "!=", 1).post()); + s("max(String,IntVar[])", m -> m.arithm(m.max("m", x(m, 3, 0, 2)), "!=", 1).post()); + s("min(String,IntVar[])", m -> m.arithm(m.min("m", x(m, 3, 0, 2)), "!=", 1).post()); + s("mod(String,IntVar,IntVar)", m -> m.arithm(m.mod("r", v(m, "x", 0, 6), v(m, "y", 1, 3)), "!=", 1).post()); + s("mod(String,IntVar,int)", m -> m.arithm(m.mod("r", v(m, "x", 0, 6), 3), "!=", 1).post()); + s("sum(String,IntVar[])", m -> m.arithm(m.sum("s", x(m, 3, 0, 2)), "=", 3).post()); + + // ---------------------------------------------------------------- clauses + s("addClause(int[]), lit(int), neg(int), satVar(Variable,Literalizer)", m -> { + BoolVar[] b = b(m, 3); + m.addClause(m.lit(b[0].satVar()), m.neg(b[1].satVar())); + m.addClause(m.lit(b[2].satVar()), m.lit(b[1].satVar())); + }); + s("sat()", m -> { + b(m, 2); + m.sat(); + }); + s("addClauseFalse(BoolVar)", m -> m.addClauseFalse(b(m, 2)[0])); + s("addClauseTrue(BoolVar)", m -> m.addClauseTrue(b(m, 2)[0])); + s("addClauses(BoolVar[],BoolVar[])", m -> { + BoolVar[] b = b(m, 3); + m.addClauses(new BoolVar[]{b[0], b[1]}, new BoolVar[]{b[2]}); + }); + s("addClauses(LogOp)", m -> { + BoolVar[] b = b(m, 3); + m.addClauses(LogOp.or(b[0], LogOp.and(b[1], LogOp.nor(b[2])))); + }); + s("addClausesAtMostNMinusOne(BoolVar[])", m -> m.addClausesAtMostNMinusOne(b(m, 3))); + s("addClausesAtMostOne(BoolVar[])", m -> m.addClausesAtMostOne(b(m, 3))); + s("addClausesBoolAndArrayEqVar(BoolVar[],BoolVar)", m -> m.addClausesBoolAndArrayEqVar(b(m, 2), m.boolVar("r"))); + s("addClausesBoolAndArrayEqualFalse(BoolVar[])", m -> m.addClausesBoolAndArrayEqualFalse(b(m, 3))); + s("addClausesBoolAndEqVar(BoolVar,BoolVar,BoolVar)", m -> { + BoolVar[] b = b(m, 3); + m.addClausesBoolAndEqVar(b[0], b[1], b[2]); + }); + s("addClausesBoolEq(BoolVar,BoolVar)", m -> { + BoolVar[] b = b(m, 2); + m.addClausesBoolEq(b[0], b[1]); + }); + s("addClausesBoolIsEqVar(BoolVar,BoolVar,BoolVar)", m -> { + BoolVar[] b = b(m, 3); + m.addClausesBoolIsEqVar(b[0], b[1], b[2]); + }); + s("addClausesBoolIsLeVar(BoolVar,BoolVar,BoolVar)", m -> { + BoolVar[] b = b(m, 3); + m.addClausesBoolIsLeVar(b[0], b[1], b[2]); + }); + s("addClausesBoolIsLtVar(BoolVar,BoolVar,BoolVar)", m -> { + BoolVar[] b = b(m, 3); + m.addClausesBoolIsLtVar(b[0], b[1], b[2]); + }); + s("addClausesBoolIsNeqVar(BoolVar,BoolVar,BoolVar)", m -> { + BoolVar[] b = b(m, 3); + m.addClausesBoolIsNeqVar(b[0], b[1], b[2]); + }); + s("addClausesBoolLe(BoolVar,BoolVar)", m -> { + BoolVar[] b = b(m, 2); + m.addClausesBoolLe(b[0], b[1]); + }); + s("addClausesBoolLt(BoolVar,BoolVar)", m -> { + BoolVar[] b = b(m, 2); + m.addClausesBoolLt(b[0], b[1]); + }); + s("addClausesBoolNot(BoolVar,BoolVar)", m -> { + BoolVar[] b = b(m, 2); + m.addClausesBoolNot(b[0], b[1]); + }); + s("addClausesBoolOrArrayEqVar(BoolVar[],BoolVar)", m -> m.addClausesBoolOrArrayEqVar(b(m, 2), m.boolVar("r"))); + s("addClausesBoolOrArrayEqualTrue(BoolVar[])", m -> m.addClausesBoolOrArrayEqualTrue(b(m, 3))); + s("addClausesBoolOrEqVar(BoolVar,BoolVar,BoolVar)", m -> { + BoolVar[] b = b(m, 3); + m.addClausesBoolOrEqVar(b[0], b[1], b[2]); + }); + s("addClausesBoolXorEqVar(BoolVar,BoolVar,BoolVar)", m -> { + BoolVar[] b = b(m, 3); + m.addClausesBoolXorEqVar(b[0], b[1], b[2]); + }); + s("addClausesMaxBoolArrayLessEqVar(BoolVar[],BoolVar)", m -> m.addClausesMaxBoolArrayLessEqVar(b(m, 2), m.boolVar("r"))); + s("addClausesSumBoolArrayGreaterEqVar(BoolVar[],BoolVar)", m -> m.addClausesSumBoolArrayGreaterEqVar(b(m, 2), m.boolVar("r"))); + s("addClausesSumBoolArrayLessEqKVar(BoolVar[],BoolVar)", m -> m.addClausesSumBoolArrayLessEqKVar(b(m, 3), m.boolVar("r"))); + s("addConstructiveDisjunction(Constraint[])", m -> { + IntVar[] x = x(m, 2, 0, 3); + m.addConstructiveDisjunction(m.arithm(x[0], "<", x[1]), m.arithm(x[0], "=", 3)); + }); + s("addElement(IntVar,int[],IntVar,int)", m -> m.addElement(v(m, "v", 0, 5), ints(3, 1, 4), v(m, "i", 0, 2), 0)); + s("addTable(IntVar[],HybridTuples)", m -> { + HybridTuples h = new HybridTuples(); + h.add(HybridTuples.eq(1), HybridTuples.any()); + h.add(HybridTuples.ne(1), HybridTuples.col(0)); + m.addTable(x(m, 2, 0, 2), h); + }); + s("addTable(IntVar[],Tuples)", m -> m.addTable(x(m, 2, 0, 2), tuples(true, ints(0, 1), ints(2, 2)))); + + // ---------------------------------------------------------------- scheduling + s("cumulative(IntVar[],int[],int[],int)", m -> m.cumulative(x(m, 3, 0, 3), ints(1, 2, 1), ints(1, 1, 2), 2).post()); + s("cumulative(List,List,IntVar)", m -> m.cumulative(Arrays.asList(tasks(m, 2)), Arrays.asList(m.intVar(1), m.intVar(1)), v(m, "c", 1, 2)).post()); + s("cumulative(Task[],IntVar[],IntVar)", m -> m.cumulative(tasks(m, 3), m.intVarArray("h", 3, 1, 2), v(m, "c", 2, 3)).post()); + s("cumulative(Task[],IntVar[],IntVar,boolean,boolean)", m -> m.cumulative(tasks(m, 3), m.intVarArray("h", 3, 1, 2), v(m, "c", 2, 3), true, false).post()); + s("setTimes(Task[])", m -> { + Task[] t = tasks(m, 2); + cum(m, t); + m.setTimes(t); + }); + s("smallest(Task[]), smallest(Task[],ArbitrationRule), before(Task,Task,ArbitrationRule)", m -> { + Task[] t = tasks(m, 2); + cum(m, t); + m.smallest(t); + m.smallest(t, ISchedulingFactory.ArbitrationRule.MIN_ECT); + m.before(t[0], t[1], ISchedulingFactory.ArbitrationRule.MIN_EST); + }); + } + + //*********************************************************************************** + // CHECKS + //*********************************************************************************** + + /** + * The modes in which the cases are checked: some factories build different constraints (or variables) with + * the SAT solver or with LCG. + */ + private enum Mode { + DEFAULT, SAT, LCG; + + Settings settings() { + switch (this) { + case SAT: + return SettingsBuilder.init().setEnableSAT(true).build(); + case LCG: + return SettingsBuilder.init().setLCG(true).build(); + default: + return SettingsBuilder.init().build(); + } + } + } + + @DataProvider + public Object[][] cases() { + List res = new ArrayList<>(); + for (Mode mode : Mode.values()) { + for (Case c : CASES) { + res.add(new Object[]{mode, c}); + } + } + return res.toArray(new Object[0][]); + } + + @Test(groups = "1s", timeOut = 60000, dataProvider = "cases") + public void testCase(Mode mode, Case c) { + Settings settings = mode.settings(); + // what the solver itself does not support (in this mode) is out of the scope of the duplication + Model direct = new Model("m", settings); + String stats; + try { + c.body().accept(direct); + stats = SpecTestUtils.solve(direct, 50_000); + } catch (Throwable e) { + throw new SkipException("not supported by the solver in mode " + mode + ": " + e); + } + direct = new Model("m", settings); + c.body().accept(direct); + RecordingModel recorded = new RecordingModel("m", settings); + c.body().accept(recorded); + if (c.name().contains("[unsupported by design]")) { + SpecException e = Assert.expectThrows(SpecException.class, recorded::snapshot); + Assert.assertTrue(e.getMessage().contains("lambda"), e.getMessage()); + return; + } + ModelSpec spec = recorded.snapshot(); + Model replayed = spec.instantiate().model(); + String expected = SpecTestUtils.structure(direct); + Assert.assertEquals(SpecTestUtils.structure(recorded), expected, "recording changes the model"); + Assert.assertEquals(SpecTestUtils.structure(replayed), expected, "the replayed model differs"); + Assert.assertEquals(SpecTestUtils.solve(recorded, 50_000), stats, "the recorded model searches differently"); + Assert.assertEquals(SpecTestUtils.solve(replayed, 50_000), stats, "the replayed model searches differently"); + } + + /** + * @return the factory methods dealing only with integer and boolean variables + */ + private static Set scope() { + Set scope = new TreeSet<>(); + for (Method m : IModel.class.getMethods()) { + if (!m.isDefault() || Modifier.isStatic(m.getModifiers()) || m.isSynthetic() || RecordingModel.EXCLUDED.contains(m.getName())) { + continue; + } + String types = Arrays.stream(m.getGenericParameterTypes()).map(Type::getTypeName) + .collect(Collectors.joining(" ")) + " " + m.getGenericReturnType().getTypeName(); + boolean real = Arrays.stream(m.getParameterTypes()).anyMatch(p -> p == double.class || p == double[].class) + && !m.getName().equals("multiCostRegular"); + String sig = signature(m.getName(), m.getParameterTypes()); + if (OUT_OF_SCOPE.stream().noneMatch(types::contains) && !real && !NOT_IMPLEMENTED.contains(sig)) { + scope.add(sig); + } + } + return scope; + } + + private static String signature(String name, Class[] params) { + return name + Arrays.stream(params).map(Class::getSimpleName).collect(Collectors.joining(",", "(", ")")); + } + + @Test(groups = "1s", timeOut = 60000) + public void testEveryIntFactoryMethodIsCovered() { + Set called = new TreeSet<>(); + for (Mode mode : Mode.values()) { + for (Case c : CASES) { + record(mode, c, called); + } + } + List missing = scope().stream().filter(s -> !called.contains(s)).collect(Collectors.toList()); + Assert.assertTrue(missing.isEmpty(), missing.size() + " factory methods are not covered: " + missing); + } + + /** + * Run a case on a recording model and collect the factory methods called at top level. + */ + private static void record(Mode mode, Case c, Set called) { + { + RecordingModel m = new RecordingModel("m", mode.settings()); + try { + c.body().accept(m); + } catch (Throwable ignored) { + // not supported by the solver in this mode + return; + } + // the calls are recorded, whether journalizable or not + m.getRecorder().unsupported().forEach(u -> called.add(u.operation().replace(" ", ""))); + try { + for (Step s : m.snapshot().steps()) { + if (s instanceof Step.Call) { + called.add(((Step.Call) s).method().toString().replace(" ", "")); + } + } + } catch (SpecException ignored) { + // unsupported by design + } + } + } +} diff --git a/solver/src/test/java/org/chocosolver/solver/spec/ModelSpecTest.java b/solver/src/test/java/org/chocosolver/solver/spec/ModelSpecTest.java new file mode 100644 index 0000000000..01634f1a15 --- /dev/null +++ b/solver/src/test/java/org/chocosolver/solver/spec/ModelSpecTest.java @@ -0,0 +1,399 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.Model; +import org.chocosolver.solver.Solver; +import org.chocosolver.solver.constraints.Constraint; +import org.chocosolver.solver.constraints.extension.Tuples; +import org.chocosolver.solver.constraints.nary.automata.FA.FiniteAutomaton; +import org.chocosolver.solver.constraints.nary.cnf.LogOp; +import org.chocosolver.solver.exception.SolverException; +import org.chocosolver.solver.search.strategy.Search; +import org.chocosolver.solver.variables.BoolVar; +import org.chocosolver.solver.variables.IntVar; +import org.chocosolver.solver.variables.Task; +import org.testng.Assert; +import org.testng.annotations.Test; + +import java.lang.reflect.Field; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashSet; +import java.util.List; +import java.util.Set; +import java.util.concurrent.ExecutorService; +import java.util.concurrent.Executors; +import java.util.concurrent.Future; + +/** + * Tests of {@link ModelSpec} built by hand, without recorder. + * + * @author Charles Prud'homme + */ +public class ModelSpecTest { + + /** + * Enumerate all solutions with a deterministic search. + * + * @return solutions, nodes and fails + */ + private static String solveAll(Model model, IntVar... decisions) { + Solver s = model.getSolver(); + s.setSearch(Search.inputOrderLBSearch(decisions)); + while (s.solve()) ; + return s.getSolutionCount() + " sols, " + s.getNodeCount() + " nodes, " + s.getFailCount() + " fails"; + } + + private record Queens(ModelSpec spec, int[] q) { + } + + private static Queens queensSpec(int n) { + SpecBuilder b = new SpecBuilder(Header.of("queens")); + int[] q = b.callArray(n, "intVarArray", "q", n, 1, n); + for (int i = 0; i < n - 1; i++) { + for (int j = i + 1; j < n; j++) { + b.post(b.call("arithm", b.ref(q[i]), "!=", b.ref(q[j]))); + b.post(b.call("arithm", b.ref(q[i]), "!=", b.ref(q[j]), "+", j - i)); + b.post(b.call("arithm", b.ref(q[i]), "!=", b.ref(q[j]), "-", j - i)); + } + } + return new Queens(b.build(), q); + } + + private static String queensDirect(int n) { + Model m = new Model("queens"); + IntVar[] q = m.intVarArray("q", n, 1, n); + for (int i = 0; i < n - 1; i++) { + for (int j = i + 1; j < n; j++) { + m.arithm(q[i], "!=", q[j]).post(); + m.arithm(q[i], "!=", q[j], "+", j - i).post(); + m.arithm(q[i], "!=", q[j], "-", j - i).post(); + } + } + return solveAll(m, q); + } + + @Test(groups = "1s", timeOut = 60000) + public void testQueensSameSearchAsDirectModel() { + Queens qs = queensSpec(8); + Resolver i1 = qs.spec().instantiate(); + Resolver i2 = qs.spec().instantiate(); + Assert.assertNotSame(i1.model(), i2.model()); + Assert.assertEquals(i1.model().getNbVars(), 8); + Assert.assertEquals(i1.model().getNbCstrs(), 3 * 28); + String direct = queensDirect(8); + Assert.assertEquals(solveAll(i1.model(), i1.intVars(qs.q())), direct); + Assert.assertEquals(solveAll(i2.model(), i2.intVars(qs.q())), direct); + Assert.assertTrue(direct.startsWith("92 sols")); + } + + @Test(groups = "1s", timeOut = 60000) + public void testInstancesAreIndependent() { + Queens qs = queensSpec(4); + Resolver i1 = qs.spec().instantiate(); + Resolver i2 = qs.spec().instantiate(); + for (int id : qs.q()) { + IntVar v1 = i1.intVar(id); + IntVar v2 = i2.intVar(id); + Assert.assertNotSame(v1, v2); + Assert.assertSame(v1.getModel(), i1.model()); + Assert.assertSame(v2.getModel(), i2.model()); + Assert.assertEquals(i1.idOf(v1), id); + Assert.assertEquals(i1.idOf(v2), -1); + } + } + + @Test(groups = "10s", timeOut = 120000) + public void testConcurrentInstantiations() throws Exception { + Queens qs = queensSpec(8); + String direct = queensDirect(8); + ExecutorService pool = Executors.newFixedThreadPool(8); + try { + List> futures = new ArrayList<>(); + for (int k = 0; k < 16; k++) { + futures.add(pool.submit(() -> { + Resolver inst = qs.spec().instantiate(); + return solveAll(inst.model(), inst.intVars(qs.q())); + })); + } + for (Future f : futures) { + Assert.assertEquals(f.get(), direct); + } + } finally { + pool.shutdownNow(); + } + } + + @Test(groups = "1s", timeOut = 60000) + public void testHeader() { + Header h = Header.of("h").withSeed(42); + Model m = new ModelSpec(h, List.of()).instantiate().model(); + Assert.assertEquals(m.getName(), "h"); + Assert.assertEquals(m.getSeed(), 42L); + Assert.assertSame(m.getSettings(), h.settings()); + } + + @Test(groups = "1s", timeOut = 60000) + public void testVarargsAndAllDifferent() { + SpecBuilder b = new SpecBuilder(Header.of("ad")); + int[] x = b.callArray(3, "intVarArray", "x", 3, 1, 3); + b.post(b.call("allDifferent", b.refs(IntVar.class, x))); + Resolver inst = b.build().instantiate(); + Assert.assertEquals(solveAll(inst.model(), inst.intVars(x)).split(",")[0], "6 sols"); + } + + @Test(groups = "1s", timeOut = 60000) + public void testReificationSteps() { + // direct + Model m = new Model(); + IntVar x = m.intVar("x", 0, 5); + Constraint c1 = m.arithm(x, ">", 2); + BoolVar b1 = c1.reify(); + BoolVar b2 = m.boolVar("b2"); + m.arithm(x, "<", 4).reifyWith(b2); + BoolVar b3 = m.boolVar("b3"); + m.arithm(x, "=", 0).implies(b3); + BoolVar b4 = m.boolVar("b4"); + m.arithm(x, "=", 5).impliedBy(b4); + m.sum(new BoolVar[]{b1, b2}, "=", 1).post(); + String direct = solveAll(m, x, b1, b2, b3, b4); + // spec + SpecBuilder b = new SpecBuilder(Header.of("reif")); + int ix = b.call("intVar", "x", 0, 5); + int ib1 = b.reify(b.call("arithm", b.ref(ix), ">", 2)); + int ib2 = b.call("boolVar", "b2"); + b.reifyWith(b.call("arithm", b.ref(ix), "<", 4), ib2); + int ib3 = b.call("boolVar", "b3"); + b.implies(b.call("arithm", b.ref(ix), "=", 0), ib3); + int ib4 = b.call("boolVar", "b4"); + b.impliedBy(b.call("arithm", b.ref(ix), "=", 5), ib4); + b.post(b.call("sum", b.refs(BoolVar.class, ib1, ib2), "=", 1)); + Resolver inst = b.build().instantiate(); + Assert.assertEquals(inst.model().getNbCstrs(), m.getNbCstrs()); + Assert.assertEquals(solveAll(inst.model(), inst.intVars(ix, ib1, ib2, ib3, ib4)), direct); + } + + @Test(groups = "1s", timeOut = 60000) + public void testUnpost() { + SpecBuilder b = new SpecBuilder(Header.of("unpost")); + int x = b.call("intVar", "x", 0, 3); + int c = b.call("arithm", b.ref(x), ">", 1); + b.post(c).unpost(c); + Resolver inst = b.build().instantiate(); + Assert.assertEquals(inst.model().getNbCstrs(), 0); + Assert.assertEquals(solveAll(inst.model(), inst.intVar(x)).split(",")[0], "4 sols"); + } + + @Test(groups = "1s", timeOut = 60000) + public void testTableSharesFrozenTuples() { + Tuples tuples = new Tuples(true); + tuples.add(1, 2); + tuples.add(2, 1); + tuples.add(3, 3); + SpecBuilder b = new SpecBuilder(Header.of("table")); + int[] x = b.callArray(2, "intVarArray", "x", 2, 1, 3); + b.post(b.call("table", b.refs(IntVar.class, x), tuples)); + ModelSpec spec = b.build(); + Assert.assertTrue(tuples.isFrozen()); + Assert.assertThrows(SolverException.class, () -> tuples.add(1, 1)); + Assert.assertThrows(SolverException.class, tuples::sort); + for (int k = 0; k < 2; k++) { + Resolver inst = spec.instantiate(); + Assert.assertEquals(solveAll(inst.model(), inst.intVars(x)).split(",")[0], "3 sols"); + } + } + + @Test(groups = "1s", timeOut = 60000) + public void testArraysAreCopied() { + int[] coeffs = {1, 2, 3}; + SpecBuilder b = new SpecBuilder(Header.of("scalar")); + int[] x = b.callArray(3, "intVarArray", "x", 3, 0, 3); + b.post(b.call("scalar", b.refs(IntVar.class, x), coeffs, "=", 6)); + ModelSpec spec = b.build(); + coeffs[0] = 100; + Model m = new Model(); + IntVar[] y = m.intVarArray("x", 3, 0, 3); + m.scalar(y, new int[]{1, 2, 3}, "=", 6).post(); + Resolver inst = spec.instantiate(); + Assert.assertEquals(solveAll(inst.model(), inst.intVars(x)), solveAll(m, y)); + } + + @Test(groups = "1s", timeOut = 60000) + public void testAutomatonIsCopied() { + FiniteAutomaton fa = new FiniteAutomaton("(1|2)3*1"); + SpecBuilder b = new SpecBuilder(Header.of("regular")); + int[] x = b.callArray(4, "intVarArray", "x", 4, 0, 3); + b.post(b.call("regular", b.refs(IntVar.class, x), fa)); + ModelSpec spec = b.build(); + Step.Call call = (Step.Call) spec.steps().get(1); + Object captured = ((Arg.Const) call.args()[1]).value(); + Assert.assertNotSame(captured, fa); + Assert.assertNotSame(((Arg.Const) call.args()[1]).value(), captured); + Model m = new Model(); + IntVar[] y = m.intVarArray("x", 4, 0, 3); + m.regular(y, fa).post(); + String direct = solveAll(m, y); + Assert.assertTrue(direct.startsWith("2 sols")); + Resolver inst = spec.instantiate(); + Assert.assertEquals(solveAll(inst.model(), inst.intVars(x)), direct); + } + + @Test(groups = "1s", timeOut = 60000) + public void testAutomatonCloneDoesNotShareBuffer() throws Exception { + FiniteAutomaton fa = new FiniteAutomaton("(1|2)3*1"); + FiniteAutomaton copy = fa.clone(); + Field nexts = FiniteAutomaton.class.getDeclaredField("nexts"); + nexts.setAccessible(true); + Assert.assertNotSame(nexts.get(copy), nexts.get(fa)); + Assert.assertEquals(copy.isDeterministic(), fa.isDeterministic()); + Assert.assertEquals(copy.getTransitions().size(), fa.getTransitions().size()); + } + + @Test(groups = "1s", timeOut = 60000) + public void testMatrixArgumentAndOutput() { + Model m = new Model(); + IntVar[][] y = m.intVarMatrix("m", 2, 3, 0, 2); + m.lexChainLess(y).post(); + String direct = solveAll(m, Arrays.stream(y).flatMap(Arrays::stream).toArray(IntVar[]::new)); + SpecBuilder b = new SpecBuilder(Header.of("lex")); + int[] ids = b.callArray(6, "intVarMatrix", "m", 2, 3, 0, 2); + int[][] rows = {Arrays.copyOfRange(ids, 0, 3), Arrays.copyOfRange(ids, 3, 6)}; + b.post(b.call("lexChainLess", b.refs(IntVar.class, rows))); + Resolver inst = b.build().instantiate(); + Assert.assertEquals(solveAll(inst.model(), inst.intVars(ids)), direct); + } + + @Test(groups = "1s", timeOut = 60000) + public void testTasksAndCumulative() { + int[] durations = {2, 3, 1}; + int[] heights = {1, 2, 2}; + Model m = new Model(); + IntVar[] s = new IntVar[3]; + Task[] tasks = new Task[3]; + IntVar[] h = new IntVar[3]; + for (int i = 0; i < 3; i++) { + s[i] = m.intVar("s" + i, 0, 4); + IntVar e = m.intVar("e" + i, 0, 6); + tasks[i] = new Task(s[i], m.intVar(durations[i]), e); + h[i] = m.intVar(heights[i]); + } + m.cumulative(tasks, h, m.intVar(3)).post(); + String direct = solveAll(m, s); + + SpecBuilder b = new SpecBuilder(Header.of("cumulative")); + int[] is = new int[3]; + int[] it = new int[3]; + int[] ih = new int[3]; + for (int i = 0; i < 3; i++) { + is[i] = b.call("intVar", "s" + i, 0, 4); + int ie = b.call("intVar", "e" + i, 0, 6); + it[i] = b.newTask(is[i], b.call("intVar", durations[i]), ie); + ih[i] = b.call("intVar", heights[i]); + } + b.post(b.call("cumulative", b.refs(Task.class, it), b.refs(IntVar.class, ih), b.ref(b.call("intVar", 3)))); + Resolver inst = b.build().instantiate(); + Assert.assertEquals(inst.model().getNbVars(), m.getNbVars()); + Assert.assertEquals(solveAll(inst.model(), inst.intVars(is)), direct); + } + + @Test(groups = "1s", timeOut = 60000) + public void testClauses() { + Model m = new Model(); + BoolVar[] x = m.boolVarArray("b", 3); + m.addClauses(LogOp.or(LogOp.and(x[0], x[1]), LogOp.nor(x[2]))); + String direct = solveAll(m, x); + SpecBuilder b = new SpecBuilder(Header.of("clauses")); + int[] ix = b.callArray(3, "boolVarArray", "b", 3); + b.effect("addClauses", Arg.or(Arg.and(b.ref(ix[0]), b.ref(ix[1])), new Arg.Logic(false, true, new Arg[]{b.ref(ix[2])}))); + Resolver inst = b.build().instantiate(); + Assert.assertEquals(solveAll(inst.model(), inst.intVars(ix)), direct); + } + + @Test(groups = "1s", timeOut = 60000) + public void testCustom() { + SpecBuilder b = new SpecBuilder(Header.of("custom")); + int x = b.call("intVar", "x", 0, 3); + b.post(b.custom("gt1", r -> r.model().arithm(r.intVar(x), ">", 1))); + Resolver inst = b.build().instantiate(); + Assert.assertEquals(solveAll(inst.model(), inst.intVar(x)).split(",")[0], "2 sols"); + } + + @Test(groups = "1s", timeOut = 60000) + public void testMostSpecificOverload() { + SpecBuilder b = new SpecBuilder(Header.of("overload")); + int[] x = b.callArray(3, "boolVarArray", "b", 3); + // sum(IntVar[], ...) and sum(BoolVar[], ...) both apply: the latter is chosen + b.post(b.call("sum", b.refs(BoolVar.class, x), "=", 2)); + ModelSpec spec = b.build(); + Step.Call call = (Step.Call) spec.steps().get(1); + Assert.assertEquals(call.method().parameterTypes()[0], BoolVar[].class); + Resolver inst = spec.instantiate(); + Assert.assertEquals(solveAll(inst.model(), inst.intVars(x)).split(",")[0], "3 sols"); + } + + @Test(groups = "1s", timeOut = 60000) + public void testCachedConstantsAreAliased() { + SpecBuilder b = new SpecBuilder(Header.of("alias")); + int c1 = b.call("intVar", 5); + int c2 = b.call("intVar", 5); + Resolver inst = b.build().instantiate(); + Assert.assertSame(inst.get(c1), inst.get(c2)); + Assert.assertEquals(inst.idOf(inst.get(c2)), c1); + } + + @Test(groups = "1s", timeOut = 60000) + public void testDivergenceIsDetected() { + FactoryMethod intVar = FactoryMethod.of("intVar", String.class, int.class, int.class); + Arg[] args = {new Arg.Const("x"), new Arg.Const(0), new Arg.Const(1)}; + ModelSpec spec = new ModelSpec(Header.of("div"), List.of( + new Step.Call(new int[]{0}, intVar, args), + new Step.Call(new int[]{0}, intVar, args))); + SpecException e = Assert.expectThrows(SpecException.class, spec::instantiate); + Assert.assertTrue(e.getMessage().contains("Divergence"), e.getMessage()); + Assert.assertTrue(e.getMessage().startsWith("Step #1"), e.getMessage()); + } + + @Test(groups = "1s", timeOut = 60000) + public void testIllFormedSpecs() { + // undefined identifier + Assert.assertThrows(SpecException.class, () -> new ModelSpec(Header.of("e"), List.of(new Step.Post(new int[]{3})))); + // wrong number of arguments + FactoryMethod intVar = FactoryMethod.of("intVar", String.class, int.class, int.class); + Assert.assertThrows(SpecException.class, () -> new Step.Call(new int[]{0}, intVar, new Arg[]{new Arg.Const("x")})); + // not a factory method + Assert.assertThrows(SpecException.class, () -> FactoryMethod.of("getSolver")); + // unsupported (mutable) constant; an object without field is immutable, hence supported + Assert.assertThrows(SpecException.class, () -> new Arg.Const(new StringBuilder())); + new Arg.Const(new Object()); + // a variable where a constraint is expected + SpecBuilder b = new SpecBuilder(Header.of("e")); + int x = b.call("intVar", "x", 0, 1); + ModelSpec spec = b.post(x).build(); + Assert.assertThrows(SpecException.class, spec::instantiate); + // a constraint where a variable is expected + FactoryMethod arithm = FactoryMethod.of("arithm", org.chocosolver.solver.variables.IntVar.class, String.class, int.class); + SpecBuilder b2 = new SpecBuilder(Header.of("e")); + int y = b2.call("intVar", "y", 0, 1); + int c = b2.call("arithm", b2.ref(y), ">", 0); + b2.call(arithm, b2.ref(c), ">", 0); + Assert.assertThrows(SpecException.class, () -> b2.build().instantiate()); + } + + @Test(groups = "1s", timeOut = 60000) + public void testNoSharedMutableObject() { + Queens qs = queensSpec(5); + Resolver i1 = qs.spec().instantiate(); + Resolver i2 = qs.spec().instantiate(); + Set seen = java.util.Collections.newSetFromMap(new java.util.IdentityHashMap<>()); + seen.addAll(Arrays.asList(i1.model().getVars())); + seen.addAll(Arrays.asList(i1.model().getCstrs())); + for (Object o : i2.model().getVars()) Assert.assertFalse(seen.contains(o)); + for (Object o : i2.model().getCstrs()) Assert.assertFalse(seen.contains(o)); + Assert.assertEquals(new HashSet<>(Arrays.asList(i1.model().getVars())).size(), 5); + } +} diff --git a/solver/src/test/java/org/chocosolver/solver/spec/RecordedModelTest.java b/solver/src/test/java/org/chocosolver/solver/spec/RecordedModelTest.java new file mode 100644 index 0000000000..3d46874c6c --- /dev/null +++ b/solver/src/test/java/org/chocosolver/solver/spec/RecordedModelTest.java @@ -0,0 +1,128 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.Model; +import org.chocosolver.solver.ParallelPortfolio; +import org.chocosolver.solver.Solution; +import org.chocosolver.solver.exception.SolverException; +import org.chocosolver.solver.search.strategy.Search; +import org.chocosolver.solver.search.strategy.strategy.AbstractStrategy; +import org.chocosolver.solver.variables.IntVar; +import org.testng.Assert; +import org.testng.annotations.Test; + +import java.util.List; + +/** + * The simple usage: {@link Model#record(String)}, {@link Model#duplicate()} and + * {@link ParallelPortfolio#of(Model, int)}, without knowing anything about specs. + * + * @author Charles Prud'homme + */ +public class RecordedModelTest { + + private static IntVar[] queens(Model model, int n) { + IntVar[] q = model.intVarArray("q", n, 1, n); + for (int i = 0; i < n - 1; i++) { + for (int j = i + 1; j < n; j++) { + model.arithm(q[i], "!=", q[j]).post(); + model.arithm(q[i], "!=", q[j], "+", j - i).post(); + model.arithm(q[i], "!=", q[j], "-", j - i).post(); + } + } + return q; + } + + private static void assertQueens(Solution s, IntVar[] q) { + for (int i = 0; i < q.length - 1; i++) { + for (int j = i + 1; j < q.length; j++) { + int a = s.getIntVal(q[i]); + int b = s.getIntVal(q[j]); + Assert.assertTrue(a != b && a != b + j - i && a != b - j + i); + } + } + } + + @Test(groups = "1s", timeOut = 60000) + public void testDuplicate() { + Model model = Model.record("queens"); + queens(model, 8); + + Model copy = model.duplicate(); + Assert.assertNotSame(copy, model); + Assert.assertEquals(copy.getNbVars(), model.getNbVars()); + Assert.assertEquals(copy.getNbCstrs(), model.getNbCstrs()); + Assert.assertEquals(copy.getSolver().findAllSolutions().size(), 92); + // the original is untouched, and can be duplicated again + Assert.assertEquals(model.duplicate().getSolver().findAllSolutions().size(), 92); + Assert.assertEquals(model.getSolver().findAllSolutions().size(), 92); + } + + @Test(groups = "1s", timeOut = 60000) + public void testPortfolio() { + Model model = Model.record("queens"); + IntVar[] q = queens(model, 10); + + ParallelPortfolio portfolio = ParallelPortfolio.of(model, 4); + Assert.assertEquals(portfolio.getModels().size(), 4); + Assert.assertSame(portfolio.getModels().get(0), model, "the original model is the first worker"); + Assert.assertTrue(portfolio.solve()); + // the solution is expressed with the variables of the original model + assertQueens(portfolio.getBestSolution(), q); + } + + @Test(groups = "1s", timeOut = 60000) + public void testOptimizationPortfolio() { + Model model = Model.record("knapsack"); + IntVar[] occ = model.intVarArray("o", 3, 0, 5); + IntVar value = model.intVar("v", 0, 100); + model.knapsack(occ, model.intVar("w", 0, 10), value, new int[]{2, 3, 4}, new int[]{3, 5, 7}).post(); + model.setObjective(Model.MAXIMIZE, value); + + ParallelPortfolio portfolio = ParallelPortfolio.of(model, List.of(Variant.IDENTITY, Variant.seed(3))); + Assert.assertEquals(portfolio.getModels().size(), 3, "the original model and one copy per variant"); + int best = -1; + while (portfolio.solve()) { + Solution s = portfolio.getBestSolution(); + best = s.getIntVal(value); + Assert.assertEquals(best, 3 * s.getIntVal(occ[0]) + 5 * s.getIntVal(occ[1]) + 7 * s.getIntVal(occ[2])); + } + Assert.assertEquals(best, 17); + } + + @Test(groups = "1s", timeOut = 60000) + public void testOriginalSearchIsKept() { + Model model = Model.record("queens"); + IntVar[] q = queens(model, 8); + AbstractStrategy search = Search.inputOrderUBSearch(q); + model.getSolver().setSearch(search); + ParallelPortfolio portfolio = ParallelPortfolio.of(model, 2); + Assert.assertTrue(portfolio.solve()); + Assert.assertSame(model.getSolver().getSearch(), search, "the search declared on the original model is kept"); + assertQueens(portfolio.getBestSolution(), q); + } + + @Test(groups = "1s", timeOut = 60000) + public void testSolvedModelCannotBeDuplicated() { + Model model = Model.record("queens"); + queens(model, 4); + Assert.assertNotNull(model.duplicate()); + Assert.assertTrue(model.getSolver().solve()); + // once its resolution has started, the model cannot be duplicated anymore + Assert.assertThrows(SolverException.class, model::duplicate); + } + + @Test(groups = "1s", timeOut = 60000) + public void testPlainModelCannotBeDuplicated() { + Model model = Model.create("plain"); + queens(model, 4); + SolverException e = Assert.expectThrows(SolverException.class, model::duplicate); + Assert.assertTrue(e.getMessage().contains("Model.record"), e.getMessage()); + Assert.assertThrows(SolverException.class, () -> ParallelPortfolio.of(model, 2)); + } +} diff --git a/solver/src/test/java/org/chocosolver/solver/spec/RecorderTest.java b/solver/src/test/java/org/chocosolver/solver/spec/RecorderTest.java new file mode 100644 index 0000000000..385835d0e0 --- /dev/null +++ b/solver/src/test/java/org/chocosolver/solver/spec/RecorderTest.java @@ -0,0 +1,358 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.Model; +import org.chocosolver.solver.constraints.Constraint; +import org.chocosolver.solver.constraints.binary.PropGreaterOrEqualX_Y; +import org.chocosolver.solver.constraints.extension.Tuples; +import org.chocosolver.solver.constraints.nary.automata.FA.CostAutomaton; +import org.chocosolver.solver.constraints.nary.automata.FA.FiniteAutomaton; +import org.chocosolver.solver.constraints.nary.cnf.LogOp; +import org.chocosolver.solver.exception.SolverException; +import org.chocosolver.solver.variables.BoolVar; +import org.chocosolver.solver.variables.IntVar; +import org.chocosolver.solver.variables.OptionalTask; +import org.chocosolver.solver.variables.Task; +import org.testng.Assert; +import org.testng.annotations.DataProvider; +import org.testng.annotations.Test; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; +import java.util.concurrent.ExecutorService; +import java.util.concurrent.Executors; +import java.util.concurrent.Future; +import java.util.function.Consumer; + +/** + * Tests of {@link RecordingModel} and {@link Recorder}: a model built directly and the same model recorded, + * snapshot and instantiated must be identical. + * + * @author Charles Prud'homme + */ +public class RecorderTest { + + /** + * Build the model directly and through a snapshot, check they are identical and return the spec. + */ + private static ModelSpec roundTrip(Consumer builder) { + Model direct = new Model("m"); + builder.accept(direct); + RecordingModel recorded = new RecordingModel("m"); + builder.accept(recorded); + ModelSpec spec = recorded.snapshot(); + Model replayed = spec.instantiate().model(); + String expected = SpecTestUtils.structure(direct); + Assert.assertEquals(SpecTestUtils.structure(recorded), expected, "recording must not change the model"); + Assert.assertEquals(SpecTestUtils.structure(replayed), expected, "replay differs"); + Assert.assertEquals(replayed.getSeed(), direct.getSeed()); + String stats = SpecTestUtils.solve(direct, 100_000); + Assert.assertEquals(SpecTestUtils.solve(recorded, 100_000), stats); + Assert.assertEquals(SpecTestUtils.solve(replayed, 100_000), stats); + return spec; + } + + //*********************************************************************************** + // SCENARIOS + //*********************************************************************************** + + private static void queens(Model m) { + int n = 6; + IntVar[] q = m.intVarArray("q", n, 1, n); + IntVar[] d1 = new IntVar[n]; + IntVar[] d2 = new IntVar[n]; + for (int i = 0; i < n; i++) { + d1[i] = m.offset(q[i], i); + d2[i] = m.offset(q[i], -i); + } + m.allDifferent(q, "AC").post(); + m.allDifferent(d1, "BC").post(); + m.allDifferent(d2).post(); + } + + private static void sideEffects(Model m) { + IntVar[] x = m.intVarArray("x", 5, 0, 4); + IntVar v = m.intVar("v", 0, 10); + IntVar i = m.intVar("i", 0, 6); + m.element(v, new int[]{3, 1, 4, 1, 5}, i, 2).post(); + m.among(m.intVar("n", 0, 5), x, new int[]{1, 3}).post(); + m.globalCardinality(x, new int[]{0, 1}, m.intVarArray("o", 2, 0, 2), false).post(); + m.nValues(x, m.intVar("nv", 2, 3)).post(); + m.sum(x, "<=", m.intVar("s", 0, 12)).post(); + m.increasing(Arrays.copyOf(x, 3), 0).post(); + m.count(2, x, m.intVar("c", 1, 2)).post(); + m.mod(x[3], 3, x[4]).post(); + m.scalar(x, new int[]{1, 2, 3, 4, 5}, ">=", 10).post(); + } + + private static void reification(Model m) { + IntVar x = m.intVar("x", 0, 5); + IntVar y = m.intVar("y", 0, 5); + BoolVar b1 = m.arithm(x, ">", y).reify(); + BoolVar b2 = m.boolVar("b2"); + m.arithm(x, "=", 2).reifyWith(b2); + BoolVar b3 = m.boolVar("b3"); + m.arithm(y, "=", 0).implies(b3); + BoolVar b4 = m.boolVar("b4"); + m.arithm(y, "=", 5).impliedBy(b4); + m.or(m.arithm(x, "=", y), m.arithm(x, "=", 0)).post(); + m.and(b1.not(), b3).post(); + m.ifThen(m.arithm(x, "=", 1), m.arithm(y, "=", 1)); + m.not(m.arithm(x, "=", 4)).post(); + Constraint c = m.arithm(x, "<", 5); + BoolVar again1 = c.reify(); + BoolVar again2 = c.reify(); + Assert.assertSame(again1, again2); + m.sum(new BoolVar[]{b1, b2, b4, again1}, ">=", 1).post(); + } + + private static void expressions(Model m) { + IntVar x = m.intVar("x", 0, 5); + IntVar y = m.intVar("y", 0, 5); + IntVar z = m.intVar("z", 0, 12); + x.add(y).mul(2).eq(z).post(); + x.gt(y).or(z.lt(3)).post(); + x.sub(y).abs().ge(2).extension().post(); + IntVar xy = x.add(y).intVar(); + m.arithm(xy, "<=", 8).post(); + x.mul(y).ne(4).decompose().post(); + } + + private static void views(Model m) { + IntVar x = m.intVar("x", -3, 3); + BoolVar b = m.boolVar("b"); + m.arithm(m.intMinusView(x), "<=", 2).post(); + m.arithm(m.intScaleView(x, 2), "!=", 2).post(); + m.arithm(m.intAbsView(x), ">", 0).post(); + BoolVar eq = m.isEq(x, 1); + m.arithm(eq, "!=", b).post(); + m.arithm(b.not(), "=", m.isLeq(x, 0)).post(); + m.arithm(m.intVar(5), ">", x).post(); + m.arithm(m.intVar(5), "!=", m.intVar("w", 4, 6)).post(); + } + + private static void scheduling(Model m) { + IntVar[] s = m.intVarArray("s", 3, 0, 5); + Task t0 = new Task(s[0], 2); + Task t1 = m.taskVar(s[1], 3); + Task t2 = new Task(s[2], m.intVar("d2", 1, 2), m.intVar("e2", 0, 8)); + OptionalTask t3 = new OptionalTask(m.intVar("s3", 0, 5), 2); + m.cumulative(new Task[]{t0, t1, t2, t3}, m.intVarArray("h", 4, 1, 1), m.intVar(2)).post(); + m.cumulative(s, new int[]{1, 1, 2}, new int[]{1, 1, 1}, 2).post(); + } + + private static void sat(Model m) { + BoolVar[] b = m.boolVarArray("b", 4); + m.addClauses(LogOp.or(LogOp.and(b[0], b[1]), LogOp.nor(b[2]))); + m.addClauseTrue(b[3]); + m.addClausesBoolOrArrayEqVar(new BoolVar[]{b[0], b[2]}, b[1]); + m.addClauses(new BoolVar[]{b[0]}, new BoolVar[]{b[2]}); + } + + private static void data(Model m) { + IntVar[] x = m.intVarArray("x", 3, 0, 3); + Tuples t = new Tuples(true); + t.add(0, 1, 2); + t.add(1, 2, 3); + t.add(3, 3, 3); + m.table(x, t, "CT+").post(); + m.table(new IntVar[]{x[0], x[1]}, new Tuples(new int[][]{{0, 1}, {1, 2}, {3, 3}}, false, java.util.OptionalInt.empty())).post(); + IntVar[] y = m.intVarArray("y", 4, 0, 3); + m.regular(y, new FiniteAutomaton("(1|2)3*1")).post(); + FiniteAutomaton fa = new FiniteAutomaton("(0|1)*"); + int[][] costs = new int[4][4]; + for (int[] c : costs) Arrays.fill(c, 1); + costs[1][1] = 0; + m.costRegular(m.intVarArray("z", 4, 0, 1), m.intVar("cost", 0, 3), + CostAutomaton.makeSingleResource(fa, costs, 0, 3)).post(); + m.lexChainLess(m.intVarMatrix("mat", 2, 2, 0, 1)).post(); + } + + private static void objectiveHooksSeed(Model m) { + m.addHook("CUMULATIVE", "GLB"); + IntVar[] x = m.intVarArray("x", 4, 0, 5); + m.setSeed(42); + m.allDifferent(x).post(); + IntVar obj = m.intVar("obj", 0, 20); + m.sum(x, "=", obj).post(); + m.setObjective(Model.MINIMIZE, obj); + Constraint tmp = m.arithm(x[0], ">", 3); + tmp.post(); + m.unpost(tmp); + } + + private static void custom(Model m) { + IntVar[] x = m.intVarArray("x", 2, 0, 3); + BoolVar[] b = m.boolVarArray("b", 2); + m.custom("geq", x, PropGreaterOrEqualX_Y::new).post(); + // the propagator is built from an array of the recorded type + m.custom("geqBool", b, PropGreaterOrEqualX_Y::new).post(); + m.custom("geqLambda", new IntVar[]{x[1], b[0]}, vs -> new PropGreaterOrEqualX_Y(vs)).post(); + } + + private static void nameAndHooks(Model m) { + m.setName("renamed"); + m.addHook("CUMULATIVE", "GLB"); + m.removeAllHooks(); + m.addHook("other", 1); + m.allDifferent(m.intVarArray("x", 3, 0, 2)).post(); + } + + private static void groups(Model m) { + IntVar[] x = m.intVarArray("x", 4, 0, 3); + IntVar[] y = m.intVarArray("y", 3, 0, 3); + m.addAsGroup("x", x); + m.addAsGroup("y", y); + m.allDifferent(x).post(); + m.sum(y, "=", x[0]).post(); + } + + @DataProvider + public Object[][] scenarios() { + return new Object[][]{ + {"queens", (Consumer) RecorderTest::queens}, + {"sideEffects", (Consumer) RecorderTest::sideEffects}, + {"reification", (Consumer) RecorderTest::reification}, + {"expressions", (Consumer) RecorderTest::expressions}, + {"views", (Consumer) RecorderTest::views}, + {"scheduling", (Consumer) RecorderTest::scheduling}, + {"sat", (Consumer) RecorderTest::sat}, + {"data", (Consumer) RecorderTest::data}, + {"objectiveHooksSeed", (Consumer) RecorderTest::objectiveHooksSeed}, + {"groups", (Consumer) RecorderTest::groups}, + {"custom", (Consumer) RecorderTest::custom}, + {"nameAndHooks", (Consumer) RecorderTest::nameAndHooks}, + }; + } + + @Test(groups = "1s", timeOut = 60000, dataProvider = "scenarios") + public void testRoundTrip(String name, Consumer builder) { + roundTrip(builder); + } + + @Test(groups = "1s", timeOut = 60000) + public void testHooksSeedAndObjectiveAreReplayed() { + ModelSpec spec = roundTrip(RecorderTest::objectiveHooksSeed); + Model m = spec.instantiate().model(); + Assert.assertEquals(m.getHook("CUMULATIVE"), "GLB"); + Assert.assertEquals(m.getSeed(), 42L); + Assert.assertNotNull(m.getObjective()); + Assert.assertEquals(m.getObjective().getName(), "obj"); + } + + @Test(groups = "1s", timeOut = 60000) + public void testNameAndHooksAreReplayed() { + ModelSpec spec = roundTrip(RecorderTest::nameAndHooks); + Assert.assertEquals(spec.header().name(), "renamed"); + Model m = spec.instantiate().model(); + Assert.assertEquals(m.getName(), "renamed"); + Assert.assertNull(m.getHook("CUMULATIVE")); + Assert.assertEquals(m.getHook("other"), 1); + } + + @Test(groups = "1s", timeOut = 60000) + public void testCapturingCustomConstraintIsReported() { + RecordingModel m = new RecordingModel("m"); + IntVar[] x = m.intVarArray("x", 2, 0, 3); + m.custom("captures", x, vs -> new PropGreaterOrEqualX_Y(x)).post(); + SpecException e = Assert.expectThrows(SpecException.class, m::snapshot); + Assert.assertTrue(e.getMessage().contains("capturing lambda"), e.getMessage()); + } + + @Test(groups = "1s", timeOut = 60000) + public void testOnlyTopLevelCallsAreRecorded() { + RecordingModel m = new RecordingModel("m"); + IntVar[] x = m.intVarArray("x", 50, 0, 5); // 1 call + m.sum(x, "=", 30, 5).post(); // 1 call + 1 post, despite the decomposition + m.globalCardinality(x, new int[]{0, 1}, m.intVarArray("o", 2, 0, 50), true).post(); // 2 calls + 1 post + List steps = m.snapshot().steps(); + Assert.assertEquals(steps.size(), 6, steps.toString()); + Assert.assertTrue(m.getNbVars() > 52, "decomposition should create intermediate variables"); + Assert.assertTrue(steps.get(0) instanceof Step.Call); + Assert.assertEquals(((Step.Call) steps.get(0)).out().length, 50); + Assert.assertTrue(steps.get(2) instanceof Step.Post); + } + + @Test(groups = "1s", timeOut = 60000) + public void testCustomConstraintIsReported() { + RecordingModel m = new RecordingModel("m"); + IntVar[] x = m.intVarArray("x", 2, 0, 3); + new Constraint("MyCustom", new PropGreaterOrEqualX_Y(x)).post(); + Assert.assertEquals(m.getRecorder().unsupported().size(), 1); + SpecException e = Assert.expectThrows(SpecException.class, m::snapshot); + Assert.assertTrue(e.getMessage().contains("MyCustom"), e.getMessage()); + Assert.assertTrue(e.getMessage().contains("Model.custom"), e.getMessage()); + } + + @Test(groups = "1s", timeOut = 60000) + public void testUnsupportedArgumentsAreReported() { + RecordingModel m = new RecordingModel("m"); + IntVar[] x = m.intVarArray("x", 3, 0, 3); + // a capturing lambda cannot be journalized (it may capture objects of the recorded model) + int threshold = x.length - 2; + m.allDifferentUnderCondition(x, v -> v.getUB() > threshold, true).post(); + // a variable of another model + Model other = new Model(); + try { + m.arithm(x[0], "=", other.intVar("o", 0, 1)).post(); + } catch (SolverException | AssertionError ignored) { + // the model itself rejects it (assertion of Model.post) + } + List u = m.getRecorder().unsupported(); + Assert.assertTrue(u.size() >= 2, u.toString()); + Assert.assertTrue(u.get(0).operation().startsWith("allDifferentUnderCondition"), u.toString()); + Assert.assertThrows(SpecException.class, m::snapshot); + } + + @Test(groups = "1s", timeOut = 60000) + public void testSnapshotAfterSolveFails() { + RecordingModel m = new RecordingModel("m"); + m.arithm(m.intVar("x", 0, 3), ">", 1).post(); + m.getSolver().solve(); + Assert.assertThrows(SpecException.class, m::snapshot); + } + + @Test(groups = "1s", timeOut = 60000) + public void testTuplesAreFrozenByRecording() { + RecordingModel m = new RecordingModel("m"); + Tuples t = new Tuples(true); + t.add(0, 1); + m.table(m.intVarArray("x", 2, 0, 1), t).post(); + Assert.assertTrue(t.isFrozen()); + } + + @Test(groups = "1s", timeOut = 60000) + public void testSnapshotIsReusableConcurrently() throws Exception { + RecordingModel master = new RecordingModel("m"); + sideEffects(master); + reification(master); + ModelSpec spec = master.snapshot(); + String expected = SpecTestUtils.solve(spec.instantiate().model(), 100_000); + ExecutorService pool = Executors.newFixedThreadPool(4); + try { + List> futures = new ArrayList<>(); + for (int k = 0; k < 8; k++) { + futures.add(pool.submit(() -> SpecTestUtils.solve(spec.instantiate().model(), 100_000))); + } + for (Future f : futures) { + Assert.assertEquals(f.get(), expected); + } + } finally { + pool.shutdownNow(); + } + } + + @Test(groups = "1s", timeOut = 60000) + public void testPlainModelHasNoRecorder() { + Model m = new Model(); + Assert.assertNull(m.getRecorder()); + BoolVar b = m.arithm(m.intVar("x", 0, 3), ">", 1).reify(); + Assert.assertNotNull(b); + } +} diff --git a/solver/src/test/java/org/chocosolver/solver/spec/SearchDeclTest.java b/solver/src/test/java/org/chocosolver/solver/spec/SearchDeclTest.java new file mode 100644 index 0000000000..fcfacd5b1c --- /dev/null +++ b/solver/src/test/java/org/chocosolver/solver/spec/SearchDeclTest.java @@ -0,0 +1,188 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.Model; +import org.chocosolver.solver.Solution; +import org.chocosolver.solver.Solver; +import org.chocosolver.solver.search.strategy.BlackBoxConfigurator; +import org.chocosolver.solver.search.strategy.Search; +import org.chocosolver.solver.search.strategy.SearchParams; +import org.chocosolver.solver.variables.IntVar; +import org.testng.Assert; +import org.testng.annotations.Test; + +import java.util.ArrayList; +import java.util.List; +import java.util.concurrent.ExecutorService; +import java.util.concurrent.Executors; +import java.util.concurrent.Future; +import java.util.function.Consumer; + +/** + * Tests of the search, objective and solutions of a {@link ModelSpec}. + * + * @author Charles Prud'homme + */ +public class SearchDeclTest { + + private static final SearchParams.VarSelConf DOMWDEG = + new SearchParams.VarSelConf(SearchParams.VariableSelection.DOMWDEG, Integer.MAX_VALUE); + private static final SearchParams.ValSelConf MIN = + new SearchParams.ValSelConf(SearchParams.ValueSelection.MIN, false, 1, false); + private static final SearchParams.ResConf LUBY = + new SearchParams.ResConf(SearchParams.Restart.LUBY, 50, 0, true); + + /** + * A small optimization problem: returns its decision variables. + */ + private static IntVar[] build(Model m) { + int n = 7; + IntVar[] x = m.intVarArray("x", n, 0, n - 1); + m.allDifferent(x).post(); + for (int i = 0; i < n - 1; i++) { + m.arithm(x[i], "!=", x[i + 1], "+", 1).post(); + } + IntVar obj = m.intVar("obj", 0, 100); + m.scalar(x, new int[]{1, 2, 3, 4, 5, 6, 7}, "=", obj).post(); + m.setObjective(Model.MINIMIZE, obj); + return x; + } + + /** + * @return solutions, nodes, fails and best objective + */ + private static String solve(Model m) { + Solver s = m.getSolver(); + s.limitNode(20_000); + while (s.solve()) ; + return s.getSolutionCount() + " sols, " + s.getNodeCount() + " nodes, " + s.getFailCount() + " fails, best=" + + s.getBestSolutionValue(); + } + + /** + * Configure the direct model with direct, and the instances with decl: they must search alike. + */ + private static void assertSameSearch(Consumer direct, SearchDecl decl) throws Exception { + Model d = new Model("m"); + IntVar[] x = build(d); + direct.accept(x); + String expected = solve(d); + + RecordingModel r = new RecordingModel("m"); + build(r); + ModelSpec spec = r.snapshot().withSearch(decl); + ExecutorService pool = Executors.newFixedThreadPool(4); + try { + List> futures = new ArrayList<>(); + for (int k = 0; k < 4; k++) { + futures.add(pool.submit(() -> solve(spec.instantiate().model()))); + } + for (Future f : futures) { + Assert.assertEquals(f.get(), expected); + } + } finally { + pool.shutdownNow(); + } + } + + @Test(groups = "1s", timeOut = 60000) + public void testModelBasedSearch() throws Exception { + assertSameSearch(x -> Search.defaultSearch(x[0].getModel()), SearchDecl.of(Search::defaultSearch)); + } + + @Test(groups = "1s", timeOut = 60000) + public void testBlackBoxWithNogoods() throws Exception { + // nogoods on restarts create the SAT constraint on each instance + assertSameSearch(x -> BlackBoxConfigurator.forCOP().make(x[0].getModel()), + SearchDecl.of(m -> BlackBoxConfigurator.forCOP().make(m))); + } + + @Test(groups = "1s", timeOut = 60000) + public void testCatalogSearch() throws Exception { + RecordingModel r = new RecordingModel("m"); + IntVar[] x = build(r); + int[] ids = r.getRecorder().idsOf(x); + assertSameSearch(v -> { + Solver s = v[0].getModel().getSolver(); + s.setSearch(DOMWDEG.make().apply(v, MIN.make().apply(v[0].getModel()))); + s.addRestarter(LUBY.make().apply(s)); + s.setSearch(Search.lastConflict(s.getSearch(), 2)); + }, + SearchDecl.intVarSearch(DOMWDEG, MIN, ids) + .andThen(SearchDecl.restarts(LUBY)) + .andThen(SearchDecl.lastConflict(2))); + } + + @Test(groups = "1s", timeOut = 60000) + public void testSolutionsAreSharedByIdentifiers() throws Exception { + RecordingModel master = new RecordingModel("m"); + IntVar[] mx = build(master); + int[] ids = master.getRecorder().idsOf(mx); + ModelSpec spec = master.snapshot().withSearch(SearchDecl.intVarSearch(DOMWDEG, MIN, ids)); + + // a worker finds the optimum + Resolver worker = spec.instantiate(); + SpecSolution best = null; + while (worker.model().getSolver().solve()) { + best = SpecSolution.record(worker); + } + Assert.assertNotNull(best); + int objId = master.getRecorder().idOf(master.getObjective()); + int optimum = best.valueOf(objId); + Assert.assertEquals(optimum, worker.model().getSolver().getBestSolutionValue().intValue()); + + // read by the master + Solution inMaster = best.toSolution(master.getRecorder()); + for (int i = 0; i < mx.length; i++) { + Assert.assertEquals(inMaster.getIntVal(mx[i]), best.valueOf(ids[i])); + } + Assert.assertEquals(inMaster.getIntVal((IntVar) master.getObjective()), optimum); + + // and it is a solution of another instance + Resolver other = spec.instantiate(); + for (int id : ids) { + other.model().arithm(other.intVar(id), "=", best.valueOf(id)).post(); + } + Assert.assertTrue(other.model().getSolver().solve()); + Assert.assertEquals(SpecSolution.record(other).valueOf(objId), optimum); + } + + @Test(groups = "1s", timeOut = 60000) + public void testCustomConstraintCapturingAnotherModelIsDetected() { + Model master = new Model(); + IntVar foreign = master.intVar("x", 0, 3); + SpecBuilder b = new SpecBuilder(Header.of("guard")); + b.call("intVar", "y", 0, 3); + b.post(b.custom("bad", r -> r.model().arithm(foreign, ">", 1))); + ModelSpec spec = b.build(); + SpecException e = Assert.expectThrows(SpecException.class, spec::instantiate); + Assert.assertTrue(e.getCause() instanceof AssertionError, String.valueOf(e.getCause())); + } + + @Test(groups = "1s", timeOut = 60000) + public void testSearchCapturingAnotherModelIsDetected() { + Model master = new Model(); + IntVar foreign = master.intVar("x", 0, 3); + SpecBuilder b = new SpecBuilder(Header.of("guard")); + b.call("intVar", "y", 0, 3); + ModelSpec spec = b.build().withSearch(r -> r.model().getSolver().setSearch(Search.inputOrderLBSearch(foreign))); + Assert.expectThrows(AssertionError.class, spec::instantiate); + } + + @Test(groups = "1s", timeOut = 60000) + public void testMasterIsAResolver() { + RecordingModel master = new RecordingModel("m"); + IntVar[] x = build(master); + Recorder r = master.getRecorder(); + Assert.assertSame(r.model(), master); + for (IntVar v : x) { + Assert.assertSame(r.get(r.idOf(v)), v); + } + Assert.assertThrows(SpecException.class, () -> r.idsOf(new Model().intVar("z", 0, 1))); + } +} diff --git a/solver/src/test/java/org/chocosolver/solver/spec/SpecPortfolioTest.java b/solver/src/test/java/org/chocosolver/solver/spec/SpecPortfolioTest.java new file mode 100644 index 0000000000..e0a109f825 --- /dev/null +++ b/solver/src/test/java/org/chocosolver/solver/spec/SpecPortfolioTest.java @@ -0,0 +1,136 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.Model; +import org.chocosolver.solver.ParallelPortfolio; +import org.chocosolver.solver.Solution; +import org.chocosolver.solver.SettingsBuilder; +import org.chocosolver.solver.exception.SolverException; +import org.chocosolver.solver.search.strategy.SearchParams; +import org.chocosolver.solver.variables.IntVar; +import org.testng.Assert; +import org.testng.annotations.Test; + +import java.util.HashSet; +import java.util.List; +import java.util.Set; + +/** + * Tests of {@link ParallelPortfolio#of(ModelSpec, List)}. + * + * @author Charles Prud'homme + */ +public class SpecPortfolioTest { + + private static final int[] WEIGHTS = {3, 4, 5, 8, 9, 11, 13}; + private static final int[] VALUES = {4, 5, 7, 10, 11, 15, 17}; + private static final int CAPACITY = 30; + + /** + * A small knapsack, to maximize. + * + * @return the occurrences + */ + private static IntVar[] knapsack(Model m) { + IntVar[] occ = m.intVarArray("o", WEIGHTS.length, 0, 3); + IntVar weight = m.intVar("w", 0, CAPACITY); + IntVar value = m.intVar("v", 0, 200); + m.knapsack(occ, weight, value, WEIGHTS, VALUES).post(); + m.setObjective(Model.MAXIMIZE, value); + return occ; + } + + /** + * @return the optimum, computed sequentially + */ + private static int optimum() { + Model m = new Model(); + knapsack(m); + Solution best = m.getSolver().findOptimalSolution((IntVar) m.getObjective(), Model.MAXIMIZE); + return best.getIntVal((IntVar) m.getObjective()); + } + + private static void assertOptimal(ParallelPortfolio portfolio, RecordingModel master, IntVar[] occ) { + int best = -1; + while (portfolio.solve()) { + best = portfolio.getBestModel().getSolver().getBestSolutionValue().intValue(); + // each solution can be read from the master + SpecSolution sol = portfolio.getBestSpecSolution(); + Solution inMaster = sol.toSolution(master.getRecorder()); + int weight = 0; + int value = 0; + for (int i = 0; i < occ.length; i++) { + weight += WEIGHTS[i] * inMaster.getIntVal(occ[i]); + value += VALUES[i] * inMaster.getIntVal(occ[i]); + } + Assert.assertTrue(weight <= CAPACITY); + Assert.assertEquals(value, best); + Assert.assertEquals(inMaster.getIntVal((IntVar) master.getObjective()), best); + } + Assert.assertEquals(best, optimum()); + } + + @Test(groups = "1s", timeOut = 60000) + public void testCarbonCopies() { + RecordingModel master = new RecordingModel("knapsack"); + IntVar[] occ = knapsack(master); + ParallelPortfolio portfolio = ParallelPortfolio.of(master.snapshot(), 4); + List models = portfolio.getModels(); + Assert.assertEquals(models.size(), 4); + Set names = new HashSet<>(); + for (Model m : models) { + Assert.assertNotSame(m, master); + Assert.assertNotNull(portfolio.resolverOf(m)); + names.add(m.getName()); + } + Assert.assertEquals(names.size(), 4, "the models are named after their rank"); + assertOptimal(portfolio, master, occ); + } + + @Test(groups = "1s", timeOut = 60000) + public void testVariants() { + RecordingModel master = new RecordingModel("knapsack"); + IntVar[] occ = knapsack(master); + int[] ids = master.getRecorder().idsOf(occ); + SearchDecl search = SearchDecl.intVarSearch( + new SearchParams.VarSelConf(SearchParams.VariableSelection.DOM, Integer.MAX_VALUE), + new SearchParams.ValSelConf(SearchParams.ValueSelection.MAX, false, 1, false), ids); + ParallelPortfolio portfolio = ParallelPortfolio.of(master.snapshot(), List.of( + Variant.IDENTITY, + Variant.seed(17), + Variant.search(search), + Variant.settings(SettingsBuilder.init().setEnableSAT(true).build()))); + Assert.assertEquals(portfolio.getModels().size(), 4); + Assert.assertEquals(portfolio.getModels().get(1).getSeed(), 17L); + assertOptimal(portfolio, master, occ); + } + + @Test(groups = "1s", timeOut = 60000) + public void testManualPortfolioHasNoResolver() { + ParallelPortfolio portfolio = new ParallelPortfolio(); + Model m = new Model(); + knapsack(m); + portfolio.addModel(m); + Assert.assertNull(portfolio.resolverOf(m)); + Assert.assertTrue(portfolio.solve()); + Assert.assertThrows(SolverException.class, portfolio::getBestSpecSolution); + Assert.assertNotNull(portfolio.getBestSolution()); + } + + @Test(groups = "1s", timeOut = 60000) + public void testInvalidVariantIsReported() { + RecordingModel master = new RecordingModel("knapsack"); + knapsack(master); + ModelSpec spec = master.snapshot(); + // a variant which breaks the replay: the error of the instantiation is reported + Variant broken = Variant.mapCalls(c -> c.method().name().equals("knapsack") + ? new Step.Call(c.out(), FactoryMethod.of("allDifferent", IntVar[].class, String.class), + new Arg[]{c.args()[0], new Arg.Const("UNKNOWN")}) : c); + Assert.assertThrows(SolverException.class, () -> ParallelPortfolio.of(spec, List.of(Variant.IDENTITY, broken))); + } +} diff --git a/solver/src/test/java/org/chocosolver/solver/spec/SpecTestUtils.java b/solver/src/test/java/org/chocosolver/solver/spec/SpecTestUtils.java new file mode 100644 index 0000000000..9bba375a23 --- /dev/null +++ b/solver/src/test/java/org/chocosolver/solver/spec/SpecTestUtils.java @@ -0,0 +1,73 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.Model; +import org.chocosolver.solver.Solver; +import org.chocosolver.solver.constraints.Constraint; +import org.chocosolver.solver.search.strategy.Search; +import org.chocosolver.solver.variables.IntVar; +import org.chocosolver.solver.variables.Variable; + +import java.util.Arrays; +import java.util.stream.Collectors; + +/** + * What the tests of this package compare between models built directly, recorded and replayed. + * + * @author Charles Prud'homme + */ +final class SpecTestUtils { + + private SpecTestUtils() { + } + + /** + * @return a description of the structure of the model: variables (with their domains), groups and constraints + * (with their propagators), in order + */ + static String structure(Model m) { + StringBuilder sb = new StringBuilder(); + for (Variable v : m.getVars()) { + sb.append(v.getClass().getSimpleName()).append(' ').append(v.getName()); + if (v instanceof IntVar iv) { + sb.append(' ').append(iv.getLB()).append("..").append(iv.getUB()).append(" #").append(iv.getDomainSize()); + } + sb.append('\n'); + } + m.getGroups().forEach(g -> sb.append("group ").append(g.getName()).append(Arrays.stream(g.getVariables()) + .map(Variable::getName).collect(Collectors.joining(",", "[", "]"))).append('\n')); + for (Constraint c : m.getCstrs()) { + sb.append(c.getName()).append(Arrays.stream(c.getPropagators()) + .map(p -> p.getClass().getSimpleName() + "/" + p.getNbVars()) + .collect(Collectors.joining(",", "[", "]"))).append('\n'); + } + return sb.toString(); + } + + /** + * Solve with a deterministic search over all integer variables, limited in nodes. + * + * @return solutions, nodes, fails and best objective + */ + static String solve(Model m, long nodes) { + Solver s = m.getSolver(); + IntVar[] vars = m.retrieveIntVars(true); + if (vars.length > 0) { + s.setSearch(Search.inputOrderLBSearch(vars)); + } + s.limitNode(nodes); + Number best = null; + while (s.solve()) { + if (m.getObjective() != null) { + best = s.getBestSolutionValue(); + } + } + return s.getSolutionCount() + " sols, " + s.getNodeCount() + " nodes, " + s.getFailCount() + + " fails" + (best == null ? "" : ", best=" + best); + } +} diff --git a/solver/src/test/java/org/chocosolver/solver/spec/VariantTest.java b/solver/src/test/java/org/chocosolver/solver/spec/VariantTest.java new file mode 100644 index 0000000000..8405f497f0 --- /dev/null +++ b/solver/src/test/java/org/chocosolver/solver/spec/VariantTest.java @@ -0,0 +1,210 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.spec; + +import org.chocosolver.solver.Model; +import org.chocosolver.solver.Solver; +import org.chocosolver.solver.constraints.Constraint; +import org.chocosolver.solver.constraints.extension.Tuples; +import org.chocosolver.solver.search.strategy.Search; +import org.chocosolver.solver.search.strategy.SearchParams; +import org.chocosolver.solver.variables.IntVar; +import org.testng.Assert; +import org.testng.annotations.Test; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; +import java.util.concurrent.ExecutorService; +import java.util.concurrent.Executors; +import java.util.concurrent.Future; +import java.util.stream.Collectors; + +/** + * Tests of {@link Variant}. + * + * @author Charles Prud'homme + */ +public class VariantTest { + + private static final int N = 7; + + /** + * Queens with three allDifferent, and a table on the first two queens. + */ + private static IntVar[] queens(Model m) { + IntVar[] q = m.intVarArray("q", N, 1, N); + IntVar[] d1 = new IntVar[N]; + IntVar[] d2 = new IntVar[N]; + for (int i = 0; i < N; i++) { + d1[i] = m.offset(q[i], i); + d2[i] = m.offset(q[i], -i); + } + m.allDifferent(q).post(); + m.allDifferent(d1, "AC").post(); + m.allDifferent(d2).post(); + Tuples t = new Tuples(false); + t.add(1, 3); + t.add(3, 1); + m.table(new IntVar[]{q[0], q[1], q[2]}, tuples3()).post(); + m.table(q[0], q[1], t).post(); + return q; + } + + private static Tuples tuples3() { + Tuples t = new Tuples(true); + for (int a = 1; a <= N; a++) { + for (int b = 1; b <= N; b++) { + for (int c = 1; c <= N; c++) { + if (a != 2 || b != 4) { + t.add(a, b, c); + } + } + } + } + return t; + } + + private static ModelSpec spec() { + return ModelSpec.record("queens", org.chocosolver.solver.SettingsBuilder.init().build(), VariantTest::queens); + } + + private static List propagators(Model m, String constraintName) { + return Arrays.stream(m.getCstrs()).filter(c -> c.getName().equals(constraintName)) + .flatMap(c -> Arrays.stream(c.getPropagators())).map(p -> p.getClass().getSimpleName()) + .collect(Collectors.toList()); + } + + private static long solutions(Model m) { + Solver s = m.getSolver(); + s.setSearch(Search.inputOrderLBSearch(m.retrieveIntVars(true))); + return s.findAllSolutions().size(); + } + + @Test(groups = "1s", timeOut = 60000) + public void testIdentity() { + ModelSpec spec = spec(); + Assert.assertSame(spec.with(Variant.IDENTITY), spec); + Assert.assertEquals(solutions(spec.instantiate(Variant.IDENTITY).model()), solutions(spec.instantiate().model())); + } + + @Test(groups = "1s", timeOut = 60000) + public void testAllDifferentConsistency() { + ModelSpec spec = spec(); + long expected = solutions(spec.instantiate().model()); + Model bc = spec.instantiate(Variant.allDifferent("BC")).model(); + List props = propagators(bc, "ALLDIFFERENT"); + Assert.assertEquals(props.stream().filter(p -> p.contains("BC")).count(), 3, props.toString()); + Assert.assertTrue(props.stream().noneMatch(p -> p.contains("AC")), props.toString()); + Assert.assertEquals(solutions(bc), expected); + Model neqs = spec.instantiate(Variant.allDifferent("NEQS")).model(); + Assert.assertTrue(propagators(neqs, "ALLDIFFERENT").isEmpty() || !propagators(neqs, "ALLDIFFERENT").contains("PropAllDiffBC")); + Assert.assertEquals(solutions(neqs), expected); + } + + @Test(groups = "1s", timeOut = 60000) + public void testTableAlgorithms() { + ModelSpec spec = spec(); + long expected = solutions(spec.instantiate().model()); + Model str2 = spec.instantiate(Variant.tableAlgorithm("STR2+")).model(); + Assert.assertTrue(propagators(str2, "TABLE").contains("PropTableStr2"), propagators(str2, "TABLE").toString()); + Assert.assertEquals(solutions(str2), expected); + Model ac3 = spec.instantiate(Variant.binaryTableAlgorithm("AC3rm")).model(); + Assert.assertTrue(propagators(ac3, "TABLE").stream().anyMatch(p -> p.contains("AC3rm")), propagators(ac3, "TABLE").toString()); + Assert.assertEquals(solutions(ac3), expected); + } + + @Test(groups = "1s", timeOut = 60000) + public void testSeedOverridesRecordedSeeds() { + Model recorded = Model.record("seeded"); + recorded.setSeed(42); + recorded.allDifferent(recorded.intVarArray("x", 3, 0, 2)).post(); + ModelSpec spec = recorded.getRecorder().snapshot(); + Assert.assertEquals(spec.instantiate().model().getSeed(), 42L); + Assert.assertEquals(spec.instantiate(Variant.seed(7)).model().getSeed(), 7L); + } + + @Test(groups = "1s", timeOut = 60000) + public void testSeedAndSearch() { + ModelSpec spec = spec(); + long expected = solutions(spec.instantiate().model()); + Model m = spec.instantiate(Variant.seed(123)).model(); + Assert.assertEquals(m.getSeed(), 123L); + Assert.assertEquals(solutions(m), expected); + SearchParams.VarSelConf dom = new SearchParams.VarSelConf(SearchParams.VariableSelection.DOM, Integer.MAX_VALUE); + SearchParams.ValSelConf max = new SearchParams.ValSelConf(SearchParams.ValueSelection.MAX, false, 1, false); + int[] q = new int[N]; + for (int i = 0; i < N; i++) { + q[i] = i; // intVarArray is the first call: its outputs are 0..N-1 + } + Model searched = spec.instantiate(Variant.search(SearchDecl.intVarSearch(dom, max, q))).model(); + Assert.assertTrue(searched.getSolver().solve()); + Assert.assertEquals(searched.getSolver().getSearch().getClass().getSimpleName(), "IntStrategy"); + } + + @Test(groups = "1s", timeOut = 60000) + public void testExtendAndUnpost() { + RecordingModel master = new RecordingModel("queens"); + IntVar[] q = queens(master); + int[] ids = master.getRecorder().idsOf(q); + ModelSpec spec = master.snapshot(); + long expected = solutions(spec.instantiate().model()); + int nbCstrs = spec.instantiate().model().getNbCstrs(); + + // redundant constraint: the sum of the queens + Variant redundant = Variant.extend(b -> b.post(b.call("sum", b.refs(IntVar.class, ids), "=", N * (N + 1) / 2))); + Model r = spec.instantiate(redundant).model(); + Assert.assertEquals(r.getNbCstrs(), nbCstrs + 1); + Assert.assertEquals(solutions(r), expected); + + // symmetry breaking: q[0] < q[N-1] + Variant symmetry = Variant.extend(b -> b.post(b.call("arithm", b.ref(ids[0]), "<", b.ref(ids[N - 1])))); + Assert.assertTrue(solutions(spec.instantiate(symmetry).model()) < expected); + + // removal of the tables + Model relaxed = spec.instantiate(Variant.unpostIf(c -> c.method().name().equals("table"))).model(); + Assert.assertEquals(relaxed.getNbCstrs(), nbCstrs - 2); + Assert.assertTrue(solutions(relaxed) > expected); + } + + @Test(groups = "1s", timeOut = 60000) + public void testComposedVariantsInParallel() throws Exception { + ModelSpec spec = spec(); + long expected = solutions(spec.instantiate().model()); + List variants = List.of( + Variant.IDENTITY, + Variant.allDifferent("BC"), + Variant.allDifferent("AC").andThen(Variant.tableAlgorithm("STR2+")).andThen(Variant.seed(7)), + Variant.binaryTableAlgorithm("FC").andThen(Variant.search(SearchDecl.of(Search::defaultSearch)))); + List specs = variants.stream().map(spec::with).collect(Collectors.toList()); + ExecutorService pool = Executors.newFixedThreadPool(4); + try { + List> futures = new ArrayList<>(); + for (ModelSpec s : specs) { + futures.add(pool.submit(() -> solutions(s.instantiate().model()))); + } + for (Future f : futures) { + Assert.assertEquals(f.get().longValue(), expected); + } + } finally { + pool.shutdownNow(); + } + } + + @Test(groups = "1s", timeOut = 60000) + public void testVariantKeepsIdentifiers() { + ModelSpec spec = spec(); + ModelSpec v = spec.with(Variant.allDifferent("BC")); + Assert.assertEquals(v.steps().size(), spec.steps().size()); + Resolver i = v.instantiate(); + for (int id = 0; id < N; id++) { + Assert.assertEquals(i.intVar(id).getName(), "q[" + id + "]"); + } + Constraint[] cs = i.model().getCstrs(); + Assert.assertEquals(cs.length, spec.instantiate().model().getNbCstrs()); + } +}