From bd75fd54bb28666235cd812014c85ec53358bb1e Mon Sep 17 00:00:00 2001 From: Jason N Date: Fri, 9 Oct 2026 10:02:59 +1100 Subject: [PATCH 1/3] Remove GCLock This is no longer needed as expressions are reference counted now and FindMUS doesn't own anything. --- lib/FznSubProblem.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/lib/FznSubProblem.cpp b/lib/FznSubProblem.cpp index e3e200d..fdc7792 100644 --- a/lib/FznSubProblem.cpp +++ b/lib/FznSubProblem.cpp @@ -140,7 +140,6 @@ void FznSubProblem::init_oracle_model(const string &oraclepath, int ncons, } void FznSubProblem::init_fzn_model(const string &fznpath) { - MiniZinc::GCLock lock; vector includes; includes.push_back(mopts.mzn_stdlib_dir + "/std/"); From 3ba1aabffb896d33388c4bd9d532e435fc4a940e Mon Sep 17 00:00:00 2001 From: Jason N Date: Fri, 9 Oct 2026 10:15:17 +1100 Subject: [PATCH 2/3] Add CI job to run tests --- .github/workflows/ci.yml | 25 ++++++++++++++++++++++++- CMakeLists.txt | 1 + scripts/ci_test.sh | 24 ++++++++++++++++++++++++ tests/tests.cpp | 4 ++-- 4 files changed, 51 insertions(+), 3 deletions(-) create mode 100644 scripts/ci_test.sh diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5ae3984..39ae513 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -200,9 +200,32 @@ jobs: name: findMUS-${{ matrix.platform }} path: findMUS-${{ matrix.triple }}.tar.gz + # The tests exercise the MUS enumeration algorithms only, which do not depend + # on the platform, so one platform is enough. Same container as the linux build. + test: + name: test + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@v7 + + - name: Fetch libminizinc + Gecode + shell: bash + run: bash scripts/fetch_minizinc.sh x86_64-linux-gnu + + - name: Build & run tests + shell: bash + run: | + set -eux + docker run --rm -v "$PWD:/work" -w /work \ + -e ROOT=/work \ + -e CMAKE_GENERATOR="Unix Makefiles" \ + -e CMAKEDIR="lib64/cmake" \ + "quay.io/pypa/manylinux_2_28_x86_64" \ + bash scripts/ci_test.sh + publish: name: publish release - needs: [build, check-version] + needs: [build, test, check-version] if: github.event_name != 'pull_request' && (github.ref == 'refs/heads/develop' || startsWith(github.ref, 'refs/tags/')) runs-on: ubuntu-24.04 permissions: diff --git a/CMakeLists.txt b/CMakeLists.txt index 1750f04..da774fd 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -6,6 +6,7 @@ if(POLICY CMP0074) endif(POLICY CMP0074) option(BUILD_FINDMUS_EXAMPLES "Build set of cpp example SubProblems" OFF) +option(BUILD_FINDMUS_TESTS "Build the MUS enumeration tests" OFF) option(MZN_SUPPORTS_SHRINK "Indicate that minizinc supports native shrink" OFF) message("-- Configuring: C++ options") diff --git a/scripts/ci_test.sh b/scripts/ci_test.sh new file mode 100644 index 0000000..3ce8fa7 --- /dev/null +++ b/scripts/ci_test.sh @@ -0,0 +1,24 @@ +#!/usr/bin/env bash +# Configure and build the findMUS tests against the libminizinc SDK and Gecode +# already in $ROOT (see fetch_minizinc.sh), then run them. +# +# Env: ROOT, CMAKE_GENERATOR, CMAKEDIR (as for ci_build.sh) +set -eux + +: "${ROOT:?ROOT must be set}" +: "${CMAKEDIR:?CMAKEDIR must be set}" + +# Debug, so the enumerators' assertions are checked too. +cmake -S "$ROOT" -B "$ROOT/build" -G "${CMAKE_GENERATOR:-Ninja}" \ + -DCMAKE_BUILD_TYPE=Debug \ + -DBUILD_FINDMUS_TESTS=ON \ + -DUSE_SYSTEM_LIBMINIZINC=1 \ + -Dlibminizinc_DIR="$ROOT/minizinc/${CMAKEDIR}/libminizinc" \ + -DGecode_ROOT="$ROOT/vendor/gecode" \ + -DOsiCBC_ROOT="$ROOT/vendor/cbc" +cmake --build "$ROOT/build" --target tests + +# The tests find their specs relative to the build directory, and option +# parsing needs a standard library even though the tests never use it. +cd "$ROOT/build" +MZN_STDLIB_DIR="$ROOT/minizinc/share/minizinc" ./tests diff --git a/tests/tests.cpp b/tests/tests.cpp index 2828d76..e73ff56 100644 --- a/tests/tests.cpp +++ b/tests/tests.cpp @@ -64,7 +64,7 @@ bool run_test(size_t id, const vector &args, string path) { return result == "PASS"; } -int run_tests(vector ids) { +bool run_tests(vector ids) { vector> test_args = { {"-t", "1000", "--paramset", "fzn", "--no-binarize", "--structure", "flat", "--shrink-alg", "map_lin"}, {"-t", "1000", "--paramset", "fzn", "--structure", "flat", "--shrink-alg", "map_lin"}, @@ -140,5 +140,5 @@ int main(int argc, char **argv) { i++; } - return HierMUS::run_tests(ids); + return HierMUS::run_tests(ids) ? EXIT_SUCCESS : EXIT_FAILURE; } From 61ea1ca8bf688a13626cfcc65c9fb8eab871fd58 Mon Sep 17 00:00:00 2001 From: Jason N Date: Fri, 9 Oct 2026 10:24:56 +1100 Subject: [PATCH 3/3] Fix ReMUS marking non-critical constraints as critical ReMUS used Selection::size() to check whether a SAT seed left out exactly one constraint, so it could wrongly mark a constraint as critical, which led to non-minimal MUSes. Fixes test 35. --- lib/ReMUS.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/lib/ReMUS.cpp b/lib/ReMUS.cpp index 25ad606..251314a 100644 --- a/lib/ReMUS.cpp +++ b/lib/ReMUS.cpp @@ -95,9 +95,12 @@ bool ReMUS::search() { } else { subsetMap->blockSubsets(s_max); Selection s_mcs = state.S.get_diff(s_max); + // Count the included nodes, not the selected ones: when state.S selects a + // parent (e.g. the root), the difference still selects only that parent. + const NodeSet& s_mcs_included = s_mcs.const_included().get_nodes(); - if (s_mcs.size() == 1) { - state.criticals.insert((*s_mcs.const_included().begin()).child); + if (s_mcs_included.size() == 1) { + state.criticals.insert(*s_mcs_included.begin()); std::stringstream ss; ss << indent << "ReMUS: updated crits: {" << state.criticals << " }"; @@ -105,7 +108,6 @@ bool ReMUS::search() { } else { // We are aboute to modify remus_stack so we need a copy of criticals NodeSet criticals_copy = state.criticals; - const NodeSet& s_mcs_included = s_mcs.const_included().get_nodes(); vector::const_reverse_iterator rit; for (rit = s_mcs_included.rbegin(); rit != s_mcs_included.rend(); ++rit) { const MapNode *n = *rit;