From e244987b8823eb7be65ab2f9d813e97b47b68624 Mon Sep 17 00:00:00 2001 From: radevgit Date: Wed, 15 Oct 2025 09:24:46 +0300 Subject: [PATCH] Change in parsing globals, arrays --- AGPRICE_MISSING_CONSTRAINTS.md | 251 ------- Cargo.lock | 2 +- Cargo.toml | 2 +- FLATZINC_MIGRATION.md | 69 -- README.md | 2 +- ZELEN_BUG_REPORT_MISSING_ARRAYS.md | 145 ---- docs/EXPORT_TO_SELEN.md | 1 + share/minizinc/solvers/zelen.msc | 2 +- share/minizinc/zelen/fzn_at_least_int.mzn | 7 + share/minizinc/zelen/fzn_at_most_int.mzn | 7 + share/minizinc/zelen/fzn_exactly_int.mzn | 7 + share/minizinc/zelen/fzn_int_element.mzn | 8 + share/minizinc/zelen/redefinitions.mzn | 68 ++ src/exporter.rs | 710 ++++++++++++++++++- src/mapper.rs | 40 +- src/mapper/constraints/cardinality.rs | 69 ++ src/mapper/constraints/counting.rs | 3 +- src/mapper/constraints/element.rs | 46 +- src/mapper/constraints/global_cardinality.rs | 24 +- src/mapper/constraints/mod.rs | 1 + test_problems.sh | 69 -- 21 files changed, 924 insertions(+), 609 deletions(-) delete mode 100644 AGPRICE_MISSING_CONSTRAINTS.md delete mode 100644 FLATZINC_MIGRATION.md delete mode 100644 ZELEN_BUG_REPORT_MISSING_ARRAYS.md create mode 100644 docs/EXPORT_TO_SELEN.md create mode 100644 share/minizinc/zelen/fzn_at_least_int.mzn create mode 100644 share/minizinc/zelen/fzn_at_most_int.mzn create mode 100644 share/minizinc/zelen/fzn_exactly_int.mzn create mode 100644 share/minizinc/zelen/fzn_int_element.mzn create mode 100644 src/mapper/constraints/cardinality.rs delete mode 100755 test_problems.sh diff --git a/AGPRICE_MISSING_CONSTRAINTS.md b/AGPRICE_MISSING_CONSTRAINTS.md deleted file mode 100644 index 83e0b33..0000000 --- a/AGPRICE_MISSING_CONSTRAINTS.md +++ /dev/null @@ -1,251 +0,0 @@ -# Analysis: Missing Constraints in agprice_full.rs - -## Executive Summary - -The generated `agprice_full.rs` file is **missing critical upper bound constraints** from the original MiniZinc model. This causes the optimization problem to be **mathematically unbounded**, leading to astronomical solution values (e.g., 8.2e51). - -**The issue is NOT with Selen's optimizer - it's with the MiniZinc-to-Rust conversion process.** - -## Problem Manifestation - -When running the generated file: -``` -OBJECTIVE = -8245408037230409000000000000000000000000000000000000 (-8.2e51) -xm = 128512896896560200000000000000000000 (1.3e35) -xb = 257154306690016960000000000000000000000 (2.6e38) -qsq = 8245408037230409000000000000000000000000000000000000 (8.2e51) -``` - -All main decision variables (milk, butt, cha, etc.) = 0, while auxiliary variables explode to astronomical values. - -## Root Cause: Missing Constraints - -### Original MiniZinc Model -Source: https://www.hakank.org/minizinc/agprice.mzn - -The original model contains **THREE CRITICAL GROUPS** of constraints that bound the problem: - -### 1. Resource Limit Constraints (MISSING) - -These constraints limit the production resources: - -```minizinc -0.04*xm+0.8*xb+0.35*xca+0.25*xcb<=0.600 /\ -0.09*xm+0.02*xb+0.3*xca+0.4*xcb<=0.750 /\ -4.82*milk+0.32*butt+0.21*cha+0.07*chb <= 1.939 /\ -``` - -**Status**: ❌ **COMPLETELY MISSING** from generated file -**Impact**: Without these, xm, xb, xca, xcb can grow unbounded - -### 2. Piecewise Linear Variable Sum Constraints (MISSING) - -These constraints ensure the piecewise linear approximation variables sum to at most 1.0: - -```minizinc -sum (i in point) (lmilk[i])<=1.0 /\ -sum (i in point) (lbutt[i])<=1.0 /\ -sum (i in point) (lcha[i])<=1.0 /\ -sum (i in point) (lchb[i])<=1.0 /\ -sum (i in point) (mq[i]+lq[i])<=1.0 -``` - -**Status**: ❌ **COMPLETELY MISSING** from generated file -**Impact**: Without these, the lmilk, lbutt, lcha, lchb arrays can grow unbounded - -### 3. Basic Non-negativity Constraints (PRESENT) - -```minizinc -milk >= 0.0 /\ -milksq >= 0.0 /\ -butt >= 0.0 /\ -buttsq >= 0.0 /\ -cha >= 0.0 /\ -chasq >= 0.0 /\ -chb >= 0.0 /\ -chbsq >= 0.0 /\ -xm >= 0.0 /\ -xb >= 0.0 /\ -xca >= 0.0 /\ -xcb >= 0.0 /\ -qsq >= 0.0 /\ -forall(i in point) (lmilk[i] >= 0.0) /\ -forall(i in point) (lbutt[i] >= 0.0) /\ -forall(i in point) (lcha[i] >= 0.0) /\ -forall(i in point) (lchb[i] >= 0.0) /\ -forall(i in point) (lq[i] >= 0.0) /\ -forall(i in point) (mq[i] >= 0.0) -``` - -**Status**: ✅ **PRESENT** in generated file (lines 296-313) -**Note**: These are correctly translated - -## Why This Causes Unbounded Solutions - -The revenue equation is: -``` -revenue = 420*cha + 1185*butt + 6748*milk - qsq - 8*chbsq - 194*chasq - 1200*buttsq - 6492*milksq + 70*chb -``` - -Without the resource limit constraints: -1. All variables have only **lower bounds** (>= 0) but **no upper bounds** -2. Variables with **positive coefficients** in revenue (milk, butt, cha, chb) should increase to maximize revenue -3. But without upper bound constraints, they can increase to **infinity** -4. The solver is correctly maximizing within the given constraints - the problem is that the constraints are incomplete! - -## Mathematical Proof of Unboundedness - -Given only the constraints in the generated file: -- Let milk = M, butt = B, cha = C, chb = K, all >= 0 -- Let all squared terms = 0 (for simplicity) -- revenue = 6748*M + 1185*B + 420*C + 70*K - -Without upper bounds on M, B, C, K: -- For any revenue value R, we can set M = R/6748 to achieve it -- As M → ∞, revenue → ∞ -- **Therefore: The problem is mathematically unbounded** - -The resource constraints like `4.82*milk + 0.32*butt + 0.21*cha + 0.07*chb <= 1.939` are essential to bound the feasible region. - -## Verification - -### Check 1: Search for resource limits -```bash -grep -E "0.600|0.750|1.939" /home/ross/devpublic/selen/debug/agprice_full.rs -``` -**Result**: No matches found ❌ - -### Check 2: Count constraint statements -```bash -grep -E "(float_lin_le|float_lin_eq)" /home/ross/devpublic/selen/debug/agprice_full.rs | wc -l -``` -**Result**: Only 16 constraint statements found - -**Expected**: Should have: -- 13+ basic >= 0 constraints ✅ -- 3 resource limit constraints ❌ -- 5 piecewise sum <= 1.0 constraints ❌ -- Multiple equality constraints for piecewise definitions ❌ -- Total should be 100+ constraint statements - -## What Selen's Optimizer Is Doing (Correctly) - -Selen's optimizer is working correctly: -1. It detects that revenue can be maximized -2. It respects all the constraints that ARE present (>= 0 bounds) -3. Since there are no upper bounds, it tries to maximize revenue as much as possible -4. The astronomical values are the solver's attempt to maximize within an unbounded feasible region - -**This is mathematically correct behavior for an unbounded optimization problem.** - -## Expected Behavior - -With the complete constraint set from the MiniZinc model, the optimal solution should be: -- **cha ≈ 10.0** (cheese 1 price around $10,000) -- All other variables at reasonable finite values -- Revenue at a finite optimal value - -The original MiniZinc model with all constraints is **bounded** and has a **finite optimal solution**. - -## Recommendations for Zelen (MiniZinc Converter) - -The MiniZinc-to-Rust converter needs to properly translate: - -1. **Linear inequality constraints** with floating-point coefficients: - - `0.04*xm+0.8*xb+0.35*xca+0.25*xcb<=0.600` - - Should generate: `model.float_lin_le(&vec![0.04, 0.8, 0.35, 0.25], &vec![xm, xb, xca, xcb], 0.600)` - -2. **Sum constraints over arrays**: - - `sum(i in point) (lmilk[i])<=1.0` - - Should generate: `model.float_lin_le(&vec![1.0; 35], &lmilk, 1.0)` (all coefficients are 1.0) - -3. **Combined array sums**: - - `sum(i in point) (mq[i]+lq[i])<=1.0` - - Should generate: `model.float_lin_le(&vec![1.0; 70], &[mq, lq].concat(), 1.0)` - -## Test Case for Zelen - -To verify the fix, the generated file should: -1. Include all resource limit constraints -2. Include all sum <= 1.0 constraints for piecewise variables -3. When run, produce output with cha ≈ 10.0 (not 0) -4. All variables should be finite (not astronomical) -5. Revenue should be finite and positive - -## Files for Reference - -- **Generated file**: `/tmp/agprice_full.rs` (incomplete) -- **Original MiniZinc**: https://www.hakank.org/minizinc/agprice.mzn (complete) -- **Expected output**: cha ≈ 10.0, finite revenue - -## Conclusion - -This is **NOT a bug in Selen's constraint solver or optimizer**. Selen is correctly solving the optimization problem as specified in the generated file. The problem is that the generated file is **missing critical constraints** that bound the feasible region. - -The fix needs to be in the MiniZinc-to-Rust converter (Zelen) to ensure all constraints are properly translated. - ---- - -## UPDATE: New Export Issue Found (agprice_test.rs) - -After the constraint export was fixed, a new issue was discovered in `/tmp/agprice_test.rs`: - -### Problem: Missing Parameter Array Definitions - -The file contains comments indicating parameter arrays that should be defined: -```rust -// Array parameter: X_INTRODUCED_212_ (initialization skipped in export) -// Array parameter: X_INTRODUCED_214_ (initialization skipped in export) -// ... etc -``` - -But these arrays are **never actually defined** in the code. Later, the constraints try to use them: -```rust -model.float_lin_eq(&x_introduced_212_, &vec![xm, milk], 1.4); // ❌ ERROR: x_introduced_212_ not defined -model.float_lin_eq(&x_introduced_214_, &vec![xb, butt], 3.7); // ❌ ERROR: x_introduced_214_ not defined -``` - -### What Should Be Generated - -Based on the MiniZinc constraints like: -```minizinc -(1.0/4.82)*xm+(0.4/0.297)*milk = 1.4 -``` - -The exporter should generate: -```rust -let x_introduced_212_ = vec![1.0/4.82, 0.4/0.297]; -model.float_lin_eq(&x_introduced_212_, &vec![xm, milk], 1.4); -``` - -### Missing Arrays - -From the comments, these parameter arrays need to be defined: -- `x_introduced_212_` - coefficients for equation with xm, milk -- `x_introduced_214_` - coefficients for equation with xb, butt -- `x_introduced_216_` - coefficients for equation with cha, xca, chb -- `x_introduced_218_` - coefficients for equation with chb, xcb, cha -- `x_introduced_220_` - coefficients for constraint with xca, xb, xm, xcb (≤ 0.6) -- `x_introduced_222_` - coefficients for constraint with xca, xb, xm, xcb (≤ 0.75) -- `x_introduced_224_` - coefficients for constraint with cha, butt, milk, chb (≤ 1.939) -- `x_introduced_226_` - coefficients for equation with chb, cha, q -- And several more for sum constraints - -### Current Status - -✅ Constraint structure is correct (the calls to float_lin_eq/float_lin_le are proper) -✅ Variables are declared correctly -❌ **Coefficient arrays are missing** - marked as "initialization skipped in export" -❌ **File does not compile** - 284 compilation errors due to undefined variables - -### Next Steps for Zelen - -1. Generate the coefficient array definitions for all `X_INTRODUCED_NNN_` parameter arrays -2. Each should be a `vec![...]` of floating-point coefficients -3. Extract the coefficients from the original FlatZinc constraints - ---- - -**Date**: October 7, 2025 -**Selen Version**: v0.9.4 -**Analyzer**: GitHub Copilot diff --git a/Cargo.lock b/Cargo.lock index 111b709..d619301 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -251,7 +251,7 @@ checksum = "d6bbff5f0aada427a1e5a6da5f1f98158182f26556f345ac9e04d36d0ebed650" [[package]] name = "zelen" -version = "0.2.0" +version = "0.3.0" dependencies = [ "clap", "selen", diff --git a/Cargo.toml b/Cargo.toml index 1551ae5..5592140 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "zelen" -version = "0.2.0" +version = "0.3.0" edition = "2024" description = "Selen CSP solver parser for FlatZinc" rust-version = "1.88" diff --git a/FLATZINC_MIGRATION.md b/FLATZINC_MIGRATION.md deleted file mode 100644 index 9419f30..0000000 --- a/FLATZINC_MIGRATION.md +++ /dev/null @@ -1,69 +0,0 @@ -# Migrating FlatZinc-Exported Files to New Selen API - -## Overview - -If you have auto-generated Selen programs from FlatZinc (like `agprice_full.rs`), they use the **old type-specific API** that has been removed. This guide shows how to update these files to work with the **new generic API**. - -## Problem Identification - -Old FlatZinc exports use methods like: -```rust -model.float_lin_eq(&coeffs, &vars, rhs); -model.float_lin_le(&coeffs, &vars, rhs); -model.int_lin_eq(&coeffs, &vars, rhs); -model.int_lin_le(&coeffs, &vars, rhs); -``` - -These methods **no longer exist** in Selen. They have been replaced with generic methods that work for both int and float. - -## Quick Fix Guide - -### 1. Replace Old Linear Constraint Methods - -**Find and Replace:** - -| Old Method | New Method | -|------------|-----------| -| `model.float_lin_eq(` | `model.lin_eq(` | -| `model.float_lin_le(` | `model.lin_le(` | -| `model.float_lin_ne(` | `model.lin_ne(` | -| `model.int_lin_eq(` | `model.lin_eq(` | -| `model.int_lin_le(` | `model.lin_le(` | -| `model.int_lin_ne(` | `model.lin_ne(` | - -**Example:** -```rust -// OLD (won't compile): -model.float_lin_eq(&vec![420.0, 1185.0, 6748.0, -1.0], - &vec![cha, butt, milk, revenue], - 0.0); - -// NEW (works): -model.lin_eq(&vec![420.0, 1185.0, 6748.0, -1.0], - &vec![cha, butt, milk, revenue], - 0.0); -``` - -### 2. Replace Reified Constraint Methods - -If your FlatZinc export uses reified constraints: - -| Old Method | New Method | -|------------|-----------| -| `model.int_eq_reif(` | `model.eq_reif(` | -| `model.float_eq_reif(` | `model.eq_reif(` | -| `model.int_ne_reif(` | `model.ne_reif(` | -| `model.float_ne_reif(` | `model.ne_reif(` | -| `model.int_le_reif(` | `model.le_reif(` | -| `model.float_le_reif(` | `model.le_reif(` | -| `model.int_lt_reif(` | `model.lt_reif(` | -| `model.float_lt_reif(` | `model.lt_reif(` | - -**Example:** -```rust -// OLD: -model.int_eq_reif(x, 5, bool_var); - -// NEW: -model.eq_reif(x, 5, bool_var); -``` diff --git a/README.md b/README.md index 38d2a24..353f52b 100644 --- a/README.md +++ b/README.md @@ -27,7 +27,7 @@ Add this to your `Cargo.toml`: ```toml [dependencies] -zelen = "0.2" +zelen = "0.3" ``` ### As a Command-Line Solver diff --git a/ZELEN_BUG_REPORT_MISSING_ARRAYS.md b/ZELEN_BUG_REPORT_MISSING_ARRAYS.md deleted file mode 100644 index 310e9bb..0000000 --- a/ZELEN_BUG_REPORT_MISSING_ARRAYS.md +++ /dev/null @@ -1,145 +0,0 @@ -# Zelen Export Bug Report: Missing Coefficient Arrays - -## Status: agprice_test.rs DOES NOT COMPILE ❌ - -**File**: `/tmp/agprice_test.rs` -**Errors**: 284 compilation errors -**Root Cause**: Parameter arrays (coefficient vectors) are not being generated - ---- - -## The Problem - -The exporter correctly identifies that parameter arrays are needed: - -```rust -// Array parameter: X_INTRODUCED_212_ (initialization skipped in export) -// Array parameter: X_INTRODUCED_214_ (initialization skipped in export) -// Array parameter: X_INTRODUCED_216_ (initialization skipped in export) -// ... 11 more arrays -``` - -But then **never actually creates these arrays**. Later in the code, constraints try to use them: - -```rust -model.float_lin_eq(&x_introduced_212_, &vec![xm, milk], 1.4); - ^^^^^^^^^^^^^^^^^^ - ERROR: cannot find value `x_introduced_212_` in this scope -``` - ---- - -## What Needs to Be Fixed - -### Example from MiniZinc -```minizinc -constraint (1.0/4.82)*xm + (0.4/0.297)*milk = 1.4 -``` - -### What's Currently Generated (BROKEN) -```rust -// Array parameter: X_INTRODUCED_212_ (initialization skipped in export) -// ... later in file ... -model.float_lin_eq(&x_introduced_212_, &vec![xm, milk], 1.4); // ❌ UNDEFINED! -``` - -### What Should Be Generated (CORRECT) -```rust -let x_introduced_212_ = vec![1.0/4.82, 0.4/0.297]; // ✅ DEFINE THE ARRAY! -// ... later in file ... -model.float_lin_eq(&x_introduced_212_, &vec![xm, milk], 1.4); -``` - ---- - -## Complete List of Missing Arrays - -Based on the compilation errors, these 14 parameter arrays need to be defined: - -1. **x_introduced_212_** - Used in: `model.float_lin_eq(&x_introduced_212_, &vec![xm, milk], 1.4)` -2. **x_introduced_214_** - Used in: `model.float_lin_eq(&x_introduced_214_, &vec![xb, butt], 3.7)` -3. **x_introduced_216_** - Used in: `model.float_lin_eq(&x_introduced_216_, &vec![cha, xca, chb], 2)` -4. **x_introduced_218_** - Used in: `model.float_lin_eq(&x_introduced_218_, &vec![chb, xcb, cha], 1)` -5. **x_introduced_220_** - Used in: `model.float_lin_le(&x_introduced_220_, &vec![xca, xb, xm, xcb], 0.6)` -6. **x_introduced_222_** - Used in: `model.float_lin_le(&x_introduced_222_, &vec![xca, xb, xm, xcb], 0.75)` -7. **x_introduced_224_** - Used in: `model.float_lin_le(&x_introduced_224_, &vec![cha, butt, milk, chb], 1.939)` -8. **x_introduced_226_** - Used in: `model.float_lin_eq(&x_introduced_226_, &vec![chb, cha, q], -0)` -9. **x_introduced_301_** - Used in: `model.float_lin_eq(&x_introduced_301_, &x_introduced_300_, -0)` -10. **x_introduced_491_** - Used in: `model.float_lin_eq(&x_introduced_491_, &x_introduced_490_, -0)` -11. **x_introduced_563_** - Used in: `model.float_lin_eq(&x_introduced_563_, &x_introduced_562_, -0)` -12. **x_introduced_753_** - Used in: `model.float_lin_eq(&x_introduced_753_, &x_introduced_752_, -0)` -13. **x_introduced_755_** - Used in: `model.float_lin_le(&x_introduced_755_, &lmilk, 1)` -14. **x_introduced_798_** - Used in: `model.float_lin_le(&x_introduced_798_, &x_introduced_797_, 1.0)` - ---- - -## Where to Place the Definitions - -The coefficient arrays should be defined **after the imports but before any model.float() calls**, typically right after `let mut model = Model::default();` - -### Recommended Structure: -```rust -use selen::prelude::*; -use selen::variables::Val; - -fn main() { - let mut model = Model::default(); - - // ===== PARAMETER ARRAYS (COEFFICIENT VECTORS) ===== - let x_introduced_212_ = vec![1.0/4.82, 0.4/0.297]; - let x_introduced_214_ = vec![1.0/0.32, 2.7/0.720]; - let x_introduced_216_ = vec![1.0/0.21, 1.1/1.05, -0.1/0.815]; - // ... etc for all 14 arrays - - // ===== VARIABLES ===== - let milk = model.float(f64::NEG_INFINITY, f64::INFINITY); - // ... rest of the code -``` - ---- - -## How to Extract Coefficients from FlatZinc - -Look for the FlatZinc constraint declarations. For example: - -``` -constraint float_lin_eq([0.20746887966804978, 1.3468013468013468], [xm, milk], 1.4); -``` - -Should generate: -```rust -let x_introduced_212_ = vec![0.20746887966804978, 1.3468013468013468]; -model.float_lin_eq(&x_introduced_212_, &vec![xm, milk], 1.4); -``` - -The coefficient array `[0.20746887966804978, 1.3468013468013468]` corresponds to `[1.0/4.82, 0.4/0.297]` from the MiniZinc source. - ---- - -## Verification Steps - -After fixing the exporter: - -1. ✅ File should compile without errors -2. ✅ Run the compiled binary and check output -3. ✅ Verify `cha` value is around 10.0 (not 0 or astronomical) -4. ✅ All variables should have finite, reasonable values -5. ✅ Revenue should be finite and positive - ---- - -## Current Export Progress - -✅ **FIXED**: Constraint structure (float_lin_eq, float_lin_le calls are correct) -✅ **FIXED**: Variable declarations (all model.float() calls present) -✅ **FIXED**: Array variable groupings (x_introduced_300_, etc.) -❌ **BROKEN**: Coefficient array definitions (all marked as "initialization skipped") - -**Once the coefficient arrays are defined, the export should be complete and working!** - ---- - -**Report Date**: October 7, 2025 -**Reported By**: Selen Testing Team -**File**: `/tmp/agprice_test.rs` -**Urgency**: HIGH - File does not compile diff --git a/docs/EXPORT_TO_SELEN.md b/docs/EXPORT_TO_SELEN.md new file mode 100644 index 0000000..9dda45d --- /dev/null +++ b/docs/EXPORT_TO_SELEN.md @@ -0,0 +1 @@ +minizinc --solver org.selen.zelen zinc/hakank/domino2.mzn zinc/hakank/domino2.dzn --export-selen /tmp/domino2_correct_solver.rs diff --git a/share/minizinc/solvers/zelen.msc b/share/minizinc/solvers/zelen.msc index 6e6198c..9ae0b8c 100644 --- a/share/minizinc/solvers/zelen.msc +++ b/share/minizinc/solvers/zelen.msc @@ -5,7 +5,7 @@ "version": "0.2.0", "mznlib": "/full/path/to/zelen/mznlib", "executable": "/full/path/to/zelen/target/release/zelen", - "tags": ["cp", "int", "float", "bool"], + "tags": ["cp", "lp", "int", "float", "bool"], "stdFlags": ["-a", "-f", "-n", "-p", "-r", "-s", "-t", "-v"], "extraFlags": [ ["--mem-limit", "Memory limit in MB (default: 2000)", "int", ""], diff --git a/share/minizinc/zelen/fzn_at_least_int.mzn b/share/minizinc/zelen/fzn_at_least_int.mzn new file mode 100644 index 0000000..95071bf --- /dev/null +++ b/share/minizinc/zelen/fzn_at_least_int.mzn @@ -0,0 +1,7 @@ +%-----------------------------------------------------------------------------% +% At least constraint for Zelen solver +% Requires at least 'n' variables in 'x' to take the value 'v' +% Handled natively by the Selen CSP solver +%-----------------------------------------------------------------------------% + +predicate fzn_at_least_int(int: n, array [int] of var int: x, int: v); diff --git a/share/minizinc/zelen/fzn_at_most_int.mzn b/share/minizinc/zelen/fzn_at_most_int.mzn new file mode 100644 index 0000000..963bd41 --- /dev/null +++ b/share/minizinc/zelen/fzn_at_most_int.mzn @@ -0,0 +1,7 @@ +%-----------------------------------------------------------------------------% +% At most constraint for Zelen solver +% Requires at most 'n' variables in 'x' to take the value 'v' +% Handled natively by the Selen CSP solver +%-----------------------------------------------------------------------------% + +predicate fzn_at_most_int(int: n, array [int] of var int: x, int: v); diff --git a/share/minizinc/zelen/fzn_exactly_int.mzn b/share/minizinc/zelen/fzn_exactly_int.mzn new file mode 100644 index 0000000..e20a8e6 --- /dev/null +++ b/share/minizinc/zelen/fzn_exactly_int.mzn @@ -0,0 +1,7 @@ +%-----------------------------------------------------------------------------% +% Exactly constraint for Zelen solver +% Requires exactly 'n' variables in 'x' to take the value 'v' +% Handled natively by the Selen CSP solver +%-----------------------------------------------------------------------------% + +predicate fzn_exactly_int(int: n, array [int] of var int: x, int: v); diff --git a/share/minizinc/zelen/fzn_int_element.mzn b/share/minizinc/zelen/fzn_int_element.mzn new file mode 100644 index 0000000..001bbd4 --- /dev/null +++ b/share/minizinc/zelen/fzn_int_element.mzn @@ -0,0 +1,8 @@ +%-----------------------------------------------------------------------------% +% Element constraint for Zelen solver +% array[index] == value +% Handled natively by the Selen CSP solver +%-----------------------------------------------------------------------------% + +predicate fzn_array_int_element(var int: idx, array [int] of int: x, var int: c); +predicate fzn_array_var_int_element(var int: idx, array [int] of var int: x, var int: c); diff --git a/share/minizinc/zelen/redefinitions.mzn b/share/minizinc/zelen/redefinitions.mzn index a542403..fd34635 100644 --- a/share/minizinc/zelen/redefinitions.mzn +++ b/share/minizinc/zelen/redefinitions.mzn @@ -3,6 +3,55 @@ % This file redefines high-level predicates to use native Zelen/Selen implementations %-----------------------------------------------------------------------------% +include "fzn_global_cardinality.mzn"; +include "fzn_array_bool.mzn"; +include "fzn_bool.mzn"; +include "fzn_int.mzn"; +include "fzn_array_int.mzn"; + +% Array boolean operations - redirect to fzn_ versions +predicate array_bool_and(array[int] of var bool: as, var bool: r) = + fzn_array_bool_and(as, r); + +predicate array_bool_or(array[int] of var bool: as, var bool: r) = + fzn_array_bool_or(as, r); + +% Boolean clause - redirect to fzn_ version +predicate bool_clause(array[int] of var bool: pos, array[int] of var bool: neg) = + fzn_bool_clause(pos, neg); + +% Integer comparison with reification - redirect to fzn_ versions +predicate int_eq_reif(var int: x, var int: y, var bool: b) = + fzn_int_eq_reif(x, y, b); + +predicate int_ne_reif(var int: x, var int: y, var bool: b) = + fzn_int_ne_reif(x, y, b); + +predicate int_le_reif(var int: x, var int: y, var bool: b) = + fzn_int_le_reif(x, y, b); + +predicate int_lt_reif(var int: x, var int: y, var bool: b) = + fzn_int_lt_reif(x, y, b); + +predicate int_ge_reif(var int: x, var int: y, var bool: b) = + fzn_int_ge_reif(x, y, b); + +predicate int_gt_reif(var int: x, var int: y, var bool: b) = + fzn_int_gt_reif(x, y, b); + +% Array element access - redirect to fzn_ versions +predicate array_int_element(var int: idx, array[int] of int: x, var int: c) = + fzn_array_int_element(idx, x, c); + +predicate array_var_int_element(var int: idx, array[int] of var int: x, var int: c) = + fzn_array_var_int_element(idx, x, c); + +predicate array_bool_element(var int: idx, array[int] of bool: x, var bool: c) = + fzn_array_bool_element(idx, x, c); + +predicate array_var_bool_element(var int: idx, array[int] of var bool: x, var bool: c) = + fzn_array_var_bool_element(idx, x, c); + % Boolean linear constraints (sum of booleans) predicate bool_lin_eq(array[int] of int: a, array[int] of var bool: x, var int: c); predicate bool_lin_ne(array[int] of int: a, array[int] of var bool: x, var int: c); @@ -24,3 +73,22 @@ predicate bool_sum_ge(array[int] of var bool: x, var int: c) = bool_lin_ge([1 | i in index_set(x)], x, c); predicate bool_sum_gt(array[int] of var bool: x, var int: c) = bool_lin_gt([1 | i in index_set(x)], x, c); + +% Global cardinality constraint +% Redirect to fzn_global_cardinality which is handled natively +predicate global_cardinality(array[int] of var int: x, + array[int] of int: cover, + array[int] of var int: counts) = + fzn_global_cardinality(x, cover, counts); + +predicate global_cardinality_low_up(array[int] of var int: x, + array[int] of int: cover, + array[int] of int: lbound, + array[int] of int: ubound) = + fzn_global_cardinality_low_up(x, cover, lbound, ubound); + +predicate global_cardinality_low_up_closed(array[int] of var int: x, + array[int] of int: cover, + array[int] of int: lbound, + array[int] of int: ubound) = + fzn_global_cardinality_low_up_closed(x, cover, lbound, ubound); diff --git a/src/exporter.rs b/src/exporter.rs index 3e0c4f7..b36f509 100644 --- a/src/exporter.rs +++ b/src/exporter.rs @@ -13,8 +13,15 @@ use crate::ast::*; use crate::error::FlatZincResult; +use std::collections::{HashMap, HashSet}; use std::fs::File; use std::io::Write; +use std::cell::RefCell; + +thread_local! { + static VAR_TO_ARRAY_MAPPING: RefCell> = RefCell::new(HashMap::new()); + static ARRAY_ALIASES: RefCell> = RefCell::new(HashMap::new()); +} /// Represents the different types of variable declarations in FlatZinc #[derive(Debug)] @@ -28,6 +35,17 @@ enum VarCategory<'a> { ScalarVariable(&'a VarDecl), } +/// Information about an array of variables that should be created together +#[derive(Debug, Clone)] +struct ArrayVarGroup { + /// Name of the array variable + array_name: String, + /// Names of individual member variables + member_names: Vec, + /// Type of the array elements (to determine int/float/bool and domain) + element_type: Type, +} + /// Export a FlatZinc AST as a standalone Selen Rust program pub fn export_selen_program(ast: &FlatZincModel, output_path: &str) -> FlatZincResult<()> { let mut file = File::create(output_path)?; @@ -40,15 +58,107 @@ pub fn export_selen_program(ast: &FlatZincModel, output_path: &str) -> FlatZincR // Classify variables into categories let (param_arrays, var_arrays, scalar_vars) = classify_variables(&ast.var_decls); + // Analyze variable arrays to find which individual variables are array members + let original_array_groups = build_array_groups(&var_arrays, &ast.var_decls)?; + + // Merge small arrays (< 10 elements) by type to reduce declaration count + let (merged_groups, merged_original_array_names) = merge_small_arrays(original_array_groups, 10); + + // Detect sequential patterns in scalar variables and create synthetic array groups + let sequential_groups = detect_sequential_patterns(&scalar_vars); + let mut array_groups = merged_groups; + array_groups.extend(sequential_groups); + + // Build mapping: variable_name -> (array_name, index) + // Also track: original_array_name -> new_array_name for arrays that share members + let mut var_to_array: HashMap = HashMap::new(); + let mut array_aliases: HashMap = HashMap::new(); + + // First pass: build member mappings and track which arrays contain which members + let mut member_to_arrays: HashMap> = HashMap::new(); + for group in &array_groups { + let array_name = sanitize_name(&group.array_name); + for (idx, member_name) in group.member_names.iter().enumerate() { + var_to_array.insert(member_name.clone(), (array_name.clone(), idx)); + member_to_arrays.entry(member_name.clone()).or_insert_with(Vec::new).push(array_name.clone()); + } + } + + // Second pass: create aliases for FlatZinc arrays that reference merged members + for var_array_decl in &var_arrays { + if let Some(Expr::ArrayLit(elements)) = &var_array_decl.init_value { + // Get the first member to find which merged array it belongs to + if let Some(Expr::Ident(first_member)) = elements.first() { + if let Some((target_array, _idx)) = var_to_array.get(first_member) { + let original_name = sanitize_name(&var_array_decl.name); + // Only create alias if the original array isn't already being declared + let processed_names: HashSet = array_groups.iter() + .map(|g| sanitize_name(&g.array_name)) + .collect(); + if !processed_names.contains(&original_name) { + array_aliases.insert(original_name, target_array.clone()); + } + } + } + } + } + + let array_members: HashSet = array_groups.iter() + .flat_map(|g| g.member_names.iter().cloned()) + .collect(); + + // Filter scalar vars to exclude those that are array members + let true_scalar_vars: Vec<&VarDecl> = scalar_vars.iter() + .filter(|v| !array_members.contains(&v.name)) + .copied() + .collect(); + + // Build set of all array names that were processed in array_groups + let processed_array_names: HashSet = array_groups.iter() + .map(|g| g.array_name.clone()) + .collect(); + + // Don't write vec![...] for arrays that: + // 1. Were already declared optimally, OR + // 2. Have all members mapped to other arrays (would cause compile errors) + let unmerged_var_arrays: Vec<&VarDecl> = var_arrays.iter() + .filter(|v| { + if processed_array_names.contains(&v.name) { + return false; + } + // Check if all members are mapped (would reference non-existent variables) + if let Some(Expr::ArrayLit(elements)) = &v.init_value { + for elem in elements { + if let Expr::Ident(member_name) = elem { + if !var_to_array.contains_key(member_name) { + return true; // At least one member is not mapped, keep this vec + } + } + } + // All members are mapped, skip this vec + return false; + } + true + }) + .copied() + .collect(); + + // Set the global array alias mapping for constraint writing + ARRAY_ALIASES.with(|aliases| { + *aliases.borrow_mut() = array_aliases; + }); + // Write each section write_parameter_arrays(&mut file, ¶m_arrays)?; - write_scalar_variables(&mut file, &scalar_vars)?; - write_variable_arrays(&mut file, &var_arrays)?; - write_constraints(&mut file, &ast.constraints)?; + write_array_variables_optimized_no_bindings(&mut file, &array_groups, &ast.var_decls, &var_to_array)?; + write_scalar_variables(&mut file, &true_scalar_vars)?; + // Only write vec![...] declarations for arrays that weren't merged + write_variable_arrays_as_vecs(&mut file, &unmerged_var_arrays)?; + write_constraints_with_array_mapping(&mut file, &ast.constraints, &var_to_array)?; let objective_var = write_solve_goal(&mut file, &ast.solve_goal)?; write_solver_invocation(&mut file, &ast.solve_goal, &objective_var)?; - write_output_section(&mut file, &scalar_vars, &objective_var)?; + write_output_section(&mut file, &true_scalar_vars, &objective_var)?; write_main_end(&mut file)?; Ok(()) @@ -145,19 +255,305 @@ fn classify_variables(var_decls: &[VarDecl]) -> (Vec<(&VarDecl, Vec)>, Vec< (param_arrays, var_arrays, scalar_vars) } +/// Build array groups from variable array declarations +/// Each group represents variables that should be created together using model.ints()/floats()/bools() +fn build_array_groups(var_arrays: &[&VarDecl], all_var_decls: &[VarDecl]) -> FlatZincResult> { + let mut groups = Vec::new(); + + for var_array_decl in var_arrays { + // Extract member variable names from the array initialization + if let Some(Expr::ArrayLit(elements)) = &var_array_decl.init_value { + let member_names: Vec = elements.iter() + .filter_map(|e| { + if let Expr::Ident(name) = e { + Some(name.clone()) + } else { + None + } + }) + .collect(); + + if !member_names.is_empty() { + // Get the element type from the array type + if let Type::Array { element_type, .. } = &var_array_decl.var_type { + groups.push(ArrayVarGroup { + array_name: var_array_decl.name.clone(), + member_names, + element_type: (**element_type).clone(), + }); + } + } + } + } + + Ok(groups) +} + +/// Merge small array groups by type to reduce declaration count +/// Also deduplicates arrays with identical member lists +/// Returns (merged_groups, set_of_original_array_names_that_were_merged) +fn merge_small_arrays(groups: Vec, min_size: usize) -> (Vec, HashSet) { + let mut result_groups = Vec::new(); + let mut small_groups_by_type: std::collections::HashMap> = std::collections::HashMap::new(); + let mut merged_original_names = HashSet::new(); + + // First, deduplicate arrays with identical member lists + let mut member_signature_map: HashMap = HashMap::new(); + let mut duplicates: Vec = Vec::new(); + + for group in groups { + // Create signature: sorted member names + type + let mut sorted_members = group.member_names.clone(); + sorted_members.sort(); + let signature = format!("{:?}:{}", sorted_members, format!("{:?}", group.element_type)); + + if let Some(_existing) = member_signature_map.get(&signature) { + // This is a duplicate - track it for alias creation + duplicates.push(group.array_name.clone()); + merged_original_names.insert(group.array_name.clone()); + } else { + // First occurrence of this signature + member_signature_map.insert(signature, group); + } + } + + // Now separate remaining unique arrays into large and small + for (_sig, group) in member_signature_map { + if group.member_names.len() >= min_size { + // Keep large arrays as-is + result_groups.push(group); + } else { + // Small arrays will be merged by type + let type_key = format!("{:?}", group.element_type); + merged_original_names.insert(group.array_name.clone()); + small_groups_by_type.entry(type_key).or_insert_with(Vec::new).push(group); + } + } + + // Merge small groups by type + for (type_key, small_groups) in small_groups_by_type { + if small_groups.is_empty() { + continue; + } + + // Collect all members from small arrays + let mut all_members = Vec::new(); + for small_group in &small_groups { + all_members.extend(small_group.member_names.clone()); + } + + // Create a merged group + let type_desc = if type_key.contains("Bool") { + "bool" + } else if type_key.contains("Float") { + "float" + } else if type_key.contains("Int") { + "int" + } else { + "var" + }; + + let merged_name = format!("merged_{}_vars", type_desc); + result_groups.push(ArrayVarGroup { + array_name: merged_name, + member_names: all_members, + element_type: small_groups[0].element_type.clone(), + }); + } + + (result_groups, merged_original_names) +} + +/// Detect variable patterns and group by type/domain +/// Groups ALL variables with the same base name pattern and type together +/// For example: ALL x_introduced_N_ with type bool -> single array +fn detect_sequential_patterns(scalar_vars: &[&VarDecl]) -> Vec { + let mut groups = Vec::new(); + + // Group variables by type only for very aggressive grouping + let mut type_groups: std::collections::HashMap> = std::collections::HashMap::new(); + + for var in scalar_vars { + // Create a type key for grouping - group ALL vars of same type together + let type_key = format!("{:?}", var.var_type); + type_groups.entry(type_key).or_insert_with(Vec::new).push(var); + } + + // Convert each type group into an ArrayVarGroup + for (type_key, mut vars) in type_groups { + // Create arrays even for small groups to maximize consolidation + if vars.len() >= 2 { + // Sort by name for consistent ordering + vars.sort_by_key(|v| v.name.clone()); + + let member_names: Vec = vars.iter().map(|v| v.name.clone()).collect(); + + // Create a descriptive array name based on type and count + let type_desc = if type_key.contains("Bool") { + "bool" + } else if type_key.contains("Float") { + "float" + } else if type_key.contains("Int") { + "int" + } else { + "var" + }; + + let synthetic_array_name = format!("grouped_{}_array_{}", type_desc, vars.len()); + groups.push(ArrayVarGroup { + array_name: synthetic_array_name, + member_names, + element_type: vars[0].var_type.clone(), + }); + } + } + + groups +} + +/// Extract base name and number from variable name like "X_INTRODUCED_169_" -> ("X_INTRODUCED_", 169) +fn extract_base_and_number(name: &str) -> Option<(String, usize)> { + // Look for pattern: prefix + digits + optional trailing underscore + let name_upper = name.to_uppercase(); + + // Find the last sequence of digits + let mut last_digit_start = None; + let mut last_digit_end = None; + + let chars: Vec = name_upper.chars().collect(); + for i in 0..chars.len() { + if chars[i].is_ascii_digit() { + if last_digit_start.is_none() || (i > 0 && !chars[i-1].is_ascii_digit()) { + last_digit_start = Some(i); + } + last_digit_end = Some(i + 1); + } + } + + if let (Some(start), Some(end)) = (last_digit_start, last_digit_end) { + let base = name_upper[..start].to_string(); + let num_str = &name_upper[start..end]; + if let Ok(num) = num_str.parse::() { + return Some((base, num)); + } + } + + None +} + +/// Check if two types match for grouping purposes +fn types_match(t1: &Type, t2: &Type) -> bool { + match (t1, t2) { + (Type::Bool, Type::Bool) => true, + (Type::IntRange(min1, max1), Type::IntRange(min2, max2)) => min1 == min2 && max1 == max2, + (Type::FloatRange(min1, max1), Type::FloatRange(min2, max2)) => { + (min1 - min2).abs() < 1e-10 && (max1 - max2).abs() < 1e-10 + } + (Type::Var(inner1), Type::Var(inner2)) => types_match(inner1, inner2), + _ => false, + } +} + +/// Write optimized array variable declarations using model.ints()/floats()/bools() +/// WITHOUT individual bindings - constraints will use array indexing directly +fn write_array_variables_optimized_no_bindings(file: &mut File, array_groups: &[ArrayVarGroup], all_var_decls: &[VarDecl], var_to_array: &HashMap) -> FlatZincResult<()> { + if array_groups.is_empty() { + return Ok(()); + } + + // Filter out arrays whose members are all mapped to OTHER arrays (would be duplicates) + let filtered_groups: Vec<&ArrayVarGroup> = array_groups.iter() + .filter(|group| { + let group_name = sanitize_name(&group.array_name); + // Keep this array if at least one member maps to THIS array (or is not mapped at all) + group.member_names.iter().any(|member| { + match var_to_array.get(member) { + Some((array_name, _idx)) => array_name == &group_name, // Keep if member maps to this array + None => true, // Keep if member not mapped anywhere + } + }) + }) + .collect(); + + if filtered_groups.is_empty() { + return Ok(()); + } + + writeln!(file, " // ===== ARRAY VARIABLES (optimized) =====")?; + + for group in filtered_groups { + // Look up the first member to get domain information + if let Some(first_member_name) = group.member_names.first() { + if let Some(first_member_decl) = all_var_decls.iter().find(|v| &v.name == first_member_name) { + let array_name = sanitize_name(&group.array_name); + let n = group.member_names.len(); + + writeln!(file, " // Array: {} ({} elements from {} to {})", + group.array_name, n, + group.member_names.first().unwrap(), + group.member_names.last().unwrap())?; + + // Generate the appropriate model.ints()/floats()/bools() call based on type + match &first_member_decl.var_type { + Type::IntRange(min, max) => { + writeln!(file, " let {} = model.ints({}, {}, {});", array_name, n, min, max)?; + } + Type::FloatRange(min, max) => { + writeln!(file, " let {} = model.floats({}, {}, {});", array_name, n, min, max)?; + } + Type::Bool => { + writeln!(file, " let {} = model.bools({});", array_name, n)?; + } + Type::Var(inner_type) => { + // Unwrap the Var() wrapper + match &**inner_type { + Type::IntRange(min, max) => { + writeln!(file, " let {} = model.ints({}, {}, {});", array_name, n, min, max)?; + } + Type::FloatRange(min, max) => { + writeln!(file, " let {} = model.floats({}, {}, {});", array_name, n, min, max)?; + } + Type::Bool => { + writeln!(file, " let {} = model.bools({});", array_name, n)?; + } + _ => { + writeln!(file, " // TODO: Unsupported array element type for {}: {:?}", group.array_name, inner_type)?; + } + } + } + _ => { + writeln!(file, " // TODO: Unsupported array element type for {}: {:?}", group.array_name, first_member_decl.var_type)?; + } + } + } + } + } + + writeln!(file)?; + Ok(()) +} + /// Write parameter array declarations (constant coefficient vectors) fn write_parameter_arrays(file: &mut File, param_arrays: &[(&VarDecl, Vec)]) -> FlatZincResult<()> { if !param_arrays.is_empty() { writeln!(file, " // ===== PARAMETER ARRAYS =====")?; for (decl, values) in param_arrays { - // Format all values as floats with .0 suffix to avoid type inference issues + // Check if this is an int array or float array based on the type + let is_int_array = matches!(&decl.var_type, + Type::Array { element_type, .. } if matches!(&**element_type, Type::Int | Type::IntRange(_, _) | Type::IntSet(_))); + + // Format values based on array type let formatted_values: Vec = values.iter().map(|v| { - if v.fract() == 0.0 && !v.is_infinite() && !v.is_nan() { - // Integer-valued floats get .0 suffix + if is_int_array { + // Integer array: format as integers without .0 + let int_val = *v as i64; + format!("{}", int_val) + } else if v.fract() == 0.0 && !v.is_infinite() && !v.is_nan() { + // Float array with integer-valued floats: add .0 suffix let int_val = *v as i64; format!("{}.0", int_val) } else { - // Already has decimal point + // Float array with non-integer values format!("{}", v) } }).collect(); @@ -181,7 +577,19 @@ fn write_scalar_variables(file: &mut File, scalar_vars: &[&VarDecl]) -> FlatZinc Ok(()) } -/// Write variable array declarations +/// Write variable array declarations as vec![...] (for backwards compatibility) +fn write_variable_arrays_as_vecs(file: &mut File, var_arrays: &[&VarDecl]) -> FlatZincResult<()> { + if !var_arrays.is_empty() { + writeln!(file, " // ===== VARIABLE ARRAYS (as vecs for constraint compatibility) =====")?; + for var_decl in var_arrays { + write_variable_array_declaration(file, var_decl)?; + } + writeln!(file)?; + } + Ok(()) +} + +/// Write variable array declarations (legacy) fn write_variable_arrays(file: &mut File, var_arrays: &[&VarDecl]) -> FlatZincResult<()> { if !var_arrays.is_empty() { writeln!(file, " // ===== VARIABLE ARRAYS =====")?; @@ -194,10 +602,10 @@ fn write_variable_arrays(file: &mut File, var_arrays: &[&VarDecl]) -> FlatZincRe } /// Write all constraints -fn write_constraints(file: &mut File, constraints: &[Constraint]) -> FlatZincResult<()> { +fn write_constraints_with_array_mapping(file: &mut File, constraints: &[Constraint], var_to_array: &HashMap) -> FlatZincResult<()> { writeln!(file, " // ===== CONSTRAINTS ===== ({} total)", constraints.len())?; for constraint in constraints { - write_constraint(file, constraint)?; + write_constraint_with_mapping(file, constraint, var_to_array)?; } writeln!(file)?; Ok(()) @@ -371,7 +779,17 @@ fn write_variable_array_declaration(file: &mut File, var_decl: &VarDecl) -> Flat Ok(()) } -fn write_constraint(file: &mut File, constraint: &Constraint) -> FlatZincResult<()> { +fn write_constraint_with_mapping(file: &mut File, constraint: &Constraint, var_to_array: &HashMap) -> FlatZincResult<()> { + // Set the thread-local mapping for this constraint + VAR_TO_ARRAY_MAPPING.with(|mapping| { + *mapping.borrow_mut() = var_to_array.clone(); + }); + + // Delegate to the regular constraint writer which will now use the mapping via format_expr + write_constraint_impl(file, constraint) +} + +fn write_constraint_impl(file: &mut File, constraint: &Constraint) -> FlatZincResult<()> { let predicate = &constraint.predicate; match predicate.as_str() { @@ -398,9 +816,32 @@ fn write_constraint(file: &mut File, constraint: &Constraint) -> FlatZincResult< // Integer comparison constraints - convert to linear form "int_eq" | "int_le" | "int_lt" | "int_ne" => write_int_comparison(file, predicate, &constraint.args)?, - "int_eq_reif" | "int_le_reif" | "int_lt_reif" | "int_ne_reif" => + "fzn_int_eq_reif" | "int_eq_reif" | "int_le_reif" | "int_lt_reif" | "int_ne_reif" | + "int_eq_imp" | "int_le_imp" | "int_lt_imp" | "int_ne_imp" | + "fzn_int_le_reif" | "fzn_int_lt_reif" | "fzn_int_ne_reif" | + "fzn_int_ge_reif" | "fzn_int_gt_reif" => write_int_comparison_reif(file, predicate, &constraint.args)?, + // Global cardinality constraints + "fzn_global_cardinality" | "global_cardinality" | "gecode_global_cardinality" => + write_global_cardinality(file, &constraint.args)?, + + // Element constraints + "fzn_array_int_element" | "array_int_element" => write_array_int_element(file, &constraint.args)?, + "fzn_array_var_int_element" | "array_var_int_element" | "gecode_int_element" => write_array_var_int_element(file, &constraint.args)?, + "fzn_array_bool_element" | "array_bool_element" => write_array_bool_element(file, &constraint.args)?, + "fzn_array_var_bool_element" | "array_var_bool_element" => write_array_var_bool_element(file, &constraint.args)?, + + // Boolean operations + "fzn_array_bool_and" | "array_bool_and" => write_array_bool_and(file, &constraint.args)?, + "fzn_array_bool_or" | "array_bool_or" => write_array_bool_or(file, &constraint.args)?, + "fzn_bool_clause" | "bool_clause" => write_bool_clause(file, &constraint.args)?, + + // Cardinality constraints + "fzn_at_least_int" | "at_least_int" => write_at_least(file, &constraint.args)?, + "fzn_at_most_int" | "at_most_int" => write_at_most(file, &constraint.args)?, + "fzn_exactly_int" | "exactly_int" => write_exactly(file, &constraint.args)?, + _ => { writeln!(file, " // TODO: Unimplemented constraint: {}({} args)", predicate, constraint.args.len())?; @@ -602,9 +1043,12 @@ fn write_int_comparison_reif(file: &mut File, predicate: &str, args: &[Expr]) -> let b = format_expr(&args[1]); let reif = format_expr(&args[2]); match predicate { - "int_le_reif" => writeln!(file, " model.lin_le_reif(&vec![1, -1], &vec![{}, {}], 0, {});", a, b, reif)?, - "int_lt_reif" => writeln!(file, " model.lin_le_reif(&vec![1, -1], &vec![{}, {}], -1, {});", a, b, reif)?, - "int_eq_reif" => writeln!(file, " model.lin_eq_reif(&vec![1, -1], &vec![{}, {}], 0, {});", a, b, reif)?, + "fzn_int_le_reif" | "int_le_reif" => writeln!(file, " model.lin_le_reif(&[1, -1], &[{}, {}], 0, {});", a, b, reif)?, + "fzn_int_lt_reif" | "int_lt_reif" => writeln!(file, " model.lin_le_reif(&[1, -1], &[{}, {}], -1, {});", a, b, reif)?, + "fzn_int_eq_reif" | "int_eq_reif" => writeln!(file, " model.lin_eq_reif(&[1, -1], &[{}, {}], 0, {});", a, b, reif)?, + "fzn_int_ge_reif" | "int_ge_reif" => writeln!(file, " model.lin_le_reif(&[-1, 1], &[{}, {}], 0, {});", a, b, reif)?, + "fzn_int_gt_reif" | "int_gt_reif" => writeln!(file, " model.lin_le_reif(&[-1, 1], &[{}, {}], -1, {});", a, b, reif)?, + "fzn_int_ne_reif" | "int_ne_reif" => writeln!(file, " model.lin_ne_reif(&[1, -1], &[{}, {}], 0, {});", a, b, reif)?, _ => writeln!(file, " // TODO: Unsupported int comparison reif: {}", predicate)?, } } @@ -712,7 +1156,24 @@ fn format_float_constant(val: f64) -> String { fn format_expr(expr: &Expr) -> String { match expr { - Expr::Ident(name) => sanitize_name(name), + Expr::Ident(name) => { + let sanitized = sanitize_name(name); + // First check if this is an array alias (e.g., x_introduced_73_ -> grouped_int_array_56) + let maybe_aliased = ARRAY_ALIASES.with(|aliases| { + let alias_map = aliases.borrow(); + alias_map.get(&sanitized).cloned().unwrap_or(sanitized.clone()) + }); + + // Then check if this variable is part of an array using thread-local mapping + VAR_TO_ARRAY_MAPPING.with(|mapping| { + let map = mapping.borrow(); + if let Some((array_name, idx)) = map.get(name) { + format!("{}[{}]", array_name, idx) + } else { + maybe_aliased + } + }) + } Expr::IntLit(i) => i.to_string(), Expr::FloatLit(f) => { if f.is_infinite() { @@ -730,13 +1191,216 @@ fn format_expr(expr: &Expr) -> String { } Expr::BoolLit(b) => b.to_string(), Expr::ArrayLit(elements) => { - let formatted: Vec = elements.iter().map(format_expr).collect(); + // Check if this array contains any literals (constants) + // If so, wrap them in int()/float()/bool() for Selen + let has_literals = elements.iter().any(|e| { + matches!(e, Expr::IntLit(_) | Expr::FloatLit(_) | Expr::BoolLit(_)) + }); + let has_idents = elements.iter().any(|e| { + matches!(e, Expr::Ident(_)) + }); + let has_mixed_types = has_literals && has_idents; + + // Debug: Print first array with mixed types + if has_mixed_types && elements.len() == 2 { + eprintln!("DEBUG: Mixed array detected - literals:{} idents:{} elements:{:?}", + has_literals, has_idents, elements); + } + + let formatted: Vec = elements.iter() + .map(|e| { + match e { + Expr::IntLit(i) if has_mixed_types => format!("int({})", i), + Expr::FloatLit(f) if has_mixed_types => { + if f.fract() == 0.0 && !f.is_nan() && !f.is_infinite() { + format!("float({}.0)", *f as i64) + } else { + format!("float({})", f) + } + } + Expr::BoolLit(b) if has_mixed_types => format!("bool({})", b), + _ => format_expr(e) + } + }) + .collect(); format!("vec![{}]", formatted.join(", ")) } _ => format!("{:?}", expr), // Fallback } } +/// Format expression with array variable optimization +fn format_expr_with_arrays(expr: &Expr, var_to_array: &HashMap) -> String { + match expr { + Expr::Ident(name) => translate_var_name(name, var_to_array), + Expr::IntLit(i) => i.to_string(), + Expr::FloatLit(f) => { + if f.is_infinite() { + if f.is_sign_positive() { + "f64::INFINITY".to_string() + } else { + "f64::NEG_INFINITY".to_string() + } + } else if f.fract() == 0.0 && !f.is_nan() { + // Ensure integer-valued floats have .0 suffix + format!("{}.0", *f as i64) + } else { + f.to_string() + } + } + Expr::BoolLit(b) => b.to_string(), + Expr::ArrayLit(elements) => { + let formatted: Vec = elements.iter().map(|e| format_expr_with_arrays(e, var_to_array)).collect(); + format!("vec![{}]", formatted.join(", ")) + } + _ => format!("{:?}", expr), // Fallback + } +} + +// Global cardinality constraint +fn write_global_cardinality(file: &mut File, args: &[Expr]) -> FlatZincResult<()> { + // fzn_global_cardinality(vars, values, counts) + if args.len() >= 3 { + let vars = format_expr(&args[0]); + let values = format_expr(&args[1]); + let counts = format_expr(&args[2]); + writeln!(file, " model.gcc(&{}, &{}, &{});", vars, values, counts)?; + } + Ok(()) +} + +// Element constraints +fn write_array_int_element(file: &mut File, args: &[Expr]) -> FlatZincResult<()> { + // array_int_element(index_1based, array, value) + if args.len() >= 3 { + let index_1based = format_expr(&args[0]); + let array = format_expr(&args[1]); + let value = format_expr(&args[2]); + writeln!(file, " let index_0based = model.sub({}, selen::variables::Val::ValI(1));", index_1based)?; + writeln!(file, " model.elem(&{}, index_0based, {});", array, value)?; + } + Ok(()) +} + +fn write_array_var_int_element(file: &mut File, args: &[Expr]) -> FlatZincResult<()> { + if args.len() == 4 { + // gecode_int_element(index, offset, array, value) + let index = format_expr(&args[0]); + let offset = format_expr(&args[1]); + let array = format_expr(&args[2]); + let value = format_expr(&args[3]); + writeln!(file, " let index_0based = model.sub({}, {});", index, offset)?; + writeln!(file, " model.elem(&{}, index_0based, {});", array, value)?; + } else if args.len() >= 3 { + // array_var_int_element(index_1based, array, value) + let index_1based = format_expr(&args[0]); + let array = format_expr(&args[1]); + let value = format_expr(&args[2]); + writeln!(file, " let index_0based = model.sub({}, selen::variables::Val::ValI(1));", index_1based)?; + writeln!(file, " model.elem(&{}, index_0based, {});", array, value)?; + } + Ok(()) +} + +fn write_array_bool_element(file: &mut File, args: &[Expr]) -> FlatZincResult<()> { + // array_bool_element(index_1based, array, value) + if args.len() >= 3 { + let index_1based = format_expr(&args[0]); + let array = format_expr(&args[1]); + let value = format_expr(&args[2]); + writeln!(file, " let index_0based = model.sub({}, selen::variables::Val::ValI(1));", index_1based)?; + writeln!(file, " model.elem(&{}, index_0based, {});", array, value)?; + } + Ok(()) +} + +fn write_array_var_bool_element(file: &mut File, args: &[Expr]) -> FlatZincResult<()> { + if args.len() == 4 { + // gecode variant with offset + let index = format_expr(&args[0]); + let offset = format_expr(&args[1]); + let array = format_expr(&args[2]); + let value = format_expr(&args[3]); + writeln!(file, " let index_0based = model.sub({}, {});", index, offset)?; + writeln!(file, " model.elem(&{}, index_0based, {});", array, value)?; + } else if args.len() >= 3 { + // array_var_bool_element(index_1based, array, value) + let index_1based = format_expr(&args[0]); + let array = format_expr(&args[1]); + let value = format_expr(&args[2]); + writeln!(file, " let index_0based = model.sub({}, selen::variables::Val::ValI(1));", index_1based)?; + writeln!(file, " model.elem(&{}, index_0based, {});", array, value)?; + } + Ok(()) +} + +// Boolean operations +fn write_array_bool_and(file: &mut File, args: &[Expr]) -> FlatZincResult<()> { + // array_bool_and(vars, result) + if args.len() >= 2 { + let vars = format_expr(&args[0]); + let result = format_expr(&args[1]); + writeln!(file, " let and_result = model.bool_and(&{});", vars)?; + writeln!(file, " model.new({}.eq(and_result));", result)?; + } + Ok(()) +} + +fn write_array_bool_or(file: &mut File, args: &[Expr]) -> FlatZincResult<()> { + // array_bool_or(vars, result) + if args.len() >= 2 { + let vars = format_expr(&args[0]); + let result = format_expr(&args[1]); + writeln!(file, " let or_result = model.bool_or(&{});", vars)?; + writeln!(file, " model.new({}.eq(or_result));", result)?; + } + Ok(()) +} + +fn write_bool_clause(file: &mut File, args: &[Expr]) -> FlatZincResult<()> { + // bool_clause(pos_lits, neg_lits) + if args.len() >= 2 { + let pos = format_expr(&args[0]); + let neg = format_expr(&args[1]); + writeln!(file, " model.bool_clause(&{}, &{});", pos, neg)?; + } + Ok(()) +} + +// Cardinality constraints +fn write_at_least(file: &mut File, args: &[Expr]) -> FlatZincResult<()> { + // fzn_at_least_int(n, vars, value) + if args.len() >= 3 { + let n = format_expr(&args[0]); + let vars = format_expr(&args[1]); + let value = format_expr(&args[2]); + writeln!(file, " model.at_least(&{}, {}, {});", vars, value, n)?; + } + Ok(()) +} + +fn write_at_most(file: &mut File, args: &[Expr]) -> FlatZincResult<()> { + // fzn_at_most_int(n, vars, value) + if args.len() >= 3 { + let n = format_expr(&args[0]); + let vars = format_expr(&args[1]); + let value = format_expr(&args[2]); + writeln!(file, " model.at_most(&{}, {}, {});", vars, value, n)?; + } + Ok(()) +} + +fn write_exactly(file: &mut File, args: &[Expr]) -> FlatZincResult<()> { + // fzn_exactly_int(n, vars, value) + if args.len() >= 3 { + let n = format_expr(&args[0]); + let vars = format_expr(&args[1]); + let value = format_expr(&args[2]); + writeln!(file, " model.exactly(&{}, {}, {});", vars, value, n)?; + } + Ok(()) +} + fn sanitize_name(name: &str) -> String { name.replace("::", "_") .replace(".", "_") @@ -746,6 +1410,16 @@ fn sanitize_name(name: &str) -> String { .to_lowercase() } +/// Translate a variable name to array access if it's part of an array +/// Returns either "array_name[idx]" or the sanitized variable name +fn translate_var_name(name: &str, var_to_array: &HashMap) -> String { + if let Some((array_name, idx)) = var_to_array.get(name) { + format!("{}[{}]", array_name, idx) + } else { + sanitize_name(name) + } +} + fn get_var_name(name: &str) -> Option { if name.starts_with("X_INTRODUCED") || name.contains("::") { return None; // Skip internal variables diff --git a/src/mapper.rs b/src/mapper.rs index aeb4f31..9766a42 100644 --- a/src/mapper.rs +++ b/src/mapper.rs @@ -443,16 +443,16 @@ impl<'a> MappingContext<'a> { "nvalue" => self.map_nvalue(constraint), "fixed_fzn_cumulative" | "cumulative" => self.map_fixed_fzn_cumulative(constraint), "var_fzn_cumulative" => self.map_var_fzn_cumulative(constraint), - "int_eq_reif" => self.map_int_eq_reif(constraint), - "int_ne_reif" => self.map_int_ne_reif(constraint), - "int_lt_reif" => self.map_int_lt_reif(constraint), - "int_le_reif" => self.map_int_le_reif(constraint), - "int_gt_reif" => self.map_int_gt_reif(constraint), - "int_ge_reif" => self.map_int_ge_reif(constraint), + "fzn_int_eq_reif" | "int_eq_reif" | "int_eq_imp" => self.map_int_eq_reif(constraint), + "fzn_int_ne_reif" | "int_ne_reif" | "int_ne_imp" => self.map_int_ne_reif(constraint), + "fzn_int_lt_reif" | "int_lt_reif" | "int_lt_imp" => self.map_int_lt_reif(constraint), + "fzn_int_le_reif" | "int_le_reif" | "int_le_imp" => self.map_int_le_reif(constraint), + "fzn_int_gt_reif" | "int_gt_reif" | "int_gt_imp" => self.map_int_gt_reif(constraint), + "fzn_int_ge_reif" | "int_ge_reif" | "int_ge_imp" => self.map_int_ge_reif(constraint), "int_lin_eq_reif" => self.map_int_lin_eq_reif(constraint), "int_lin_ne_reif" => self.map_int_lin_ne_reif(constraint), "int_lin_le_reif" => self.map_int_lin_le_reif(constraint), - "bool_clause" => self.map_bool_clause(constraint), + "fzn_bool_clause" | "bool_clause" => self.map_bool_clause(constraint), // Boolean linear constraints "bool_lin_eq" => self.map_bool_lin_eq(constraint), "bool_lin_le" => self.map_bool_lin_le(constraint), @@ -465,20 +465,27 @@ impl<'a> MappingContext<'a> { "array_int_maximum" | "maximum_int" => self.map_array_int_maximum(constraint), "array_float_minimum" | "minimum_float" => self.map_array_float_minimum(constraint), "array_float_maximum" | "maximum_float" => self.map_array_float_maximum(constraint), - "array_bool_and" => self.map_array_bool_and(constraint), - "array_bool_or" => self.map_array_bool_or(constraint), + "fzn_array_bool_and" | "array_bool_and" => self.map_array_bool_and(constraint), + "fzn_array_bool_or" | "array_bool_or" => self.map_array_bool_or(constraint), // Bool-int conversion "bool2int" => self.map_bool2int(constraint), "bool_eq_reif" => self.map_bool_eq_reif(constraint), // Count constraints "count_eq" | "count" => self.map_count_eq(constraint), + // Cardinality constraints + "fzn_at_least_int" | "at_least_int" => self.map_at_least_int(constraint), + "fzn_at_most_int" | "at_most_int" => self.map_at_most_int(constraint), + "fzn_exactly_int" | "exactly_int" => self.map_exactly_int(constraint), + // Global cardinality constraints + "fzn_global_cardinality" | "global_cardinality" | "gecode_global_cardinality" => self.map_global_cardinality(constraint), + "fzn_global_cardinality_low_up_closed" | "global_cardinality_low_up_closed" | "gecode_global_cardinality_low_up_closed" => self.map_global_cardinality_low_up_closed(constraint), // Element constraints (array indexing) - "array_var_int_element" => self.map_array_var_int_element(constraint), - "array_int_element" => self.map_array_int_element(constraint), - "array_var_bool_element" => self.map_array_var_bool_element(constraint), - "array_bool_element" => self.map_array_bool_element(constraint), - "array_var_float_element" => self.map_array_var_float_element(constraint), - "array_float_element" => self.map_array_float_element(constraint), + "fzn_array_var_int_element" | "array_var_int_element" | "gecode_int_element" => self.map_array_var_int_element(constraint), + "fzn_array_int_element" | "array_int_element" => self.map_array_int_element(constraint), + "fzn_array_var_bool_element" | "array_var_bool_element" => self.map_array_var_bool_element(constraint), + "fzn_array_bool_element" | "array_bool_element" => self.map_array_bool_element(constraint), + "fzn_array_var_float_element" | "array_var_float_element" => self.map_array_var_float_element(constraint), + "fzn_array_float_element" | "array_float_element" => self.map_array_float_element(constraint), // Arithmetic operations "int_abs" => self.map_int_abs(constraint), "int_plus" => self.map_int_plus(constraint), @@ -497,9 +504,6 @@ impl<'a> MappingContext<'a> { // Set constraints "set_in_reif" => self.map_set_in_reif(constraint), "set_in" => self.map_set_in(constraint), - // Global cardinality - "global_cardinality" => self.map_global_cardinality(constraint), - "global_cardinality_low_up_closed" => self.map_global_cardinality_low_up_closed(constraint), // Float constraints "float_eq" => self.map_float_eq(constraint), "float_ne" => self.map_float_ne(constraint), diff --git a/src/mapper/constraints/cardinality.rs b/src/mapper/constraints/cardinality.rs new file mode 100644 index 0000000..037bc37 --- /dev/null +++ b/src/mapper/constraints/cardinality.rs @@ -0,0 +1,69 @@ +//! At least, at most, exactly constraint mappers +//! +//! Maps FlatZinc counting constraints to Selen's native cardinality constraints. + +use crate::ast::*; +use crate::error::{FlatZincError, FlatZincResult}; +use crate::mapper::MappingContext; + +impl<'a> MappingContext<'a> { + /// Map at_least: at least n variables in array equal value + /// FlatZinc signature: fzn_at_least_int(n, x, v) + pub(in crate::mapper) fn map_at_least_int(&mut self, constraint: &Constraint) -> FlatZincResult<()> { + if constraint.args.len() != 3 { + return Err(FlatZincError::MapError { + message: "at_least_int requires 3 arguments (n, x, v)".to_string(), + line: Some(constraint.location.line), + column: Some(constraint.location.column), + }); + } + + let n = self.extract_int(&constraint.args[0])?; + let arr_vars = self.extract_var_array(&constraint.args[1])?; + let value = self.extract_int(&constraint.args[2])?; + + // Use Selen's at_least constraint + self.model.at_least(&arr_vars, value, n); + Ok(()) + } + + /// Map at_most: at most n variables in array equal value + /// FlatZinc signature: fzn_at_most_int(n, x, v) + pub(in crate::mapper) fn map_at_most_int(&mut self, constraint: &Constraint) -> FlatZincResult<()> { + if constraint.args.len() != 3 { + return Err(FlatZincError::MapError { + message: "at_most_int requires 3 arguments (n, x, v)".to_string(), + line: Some(constraint.location.line), + column: Some(constraint.location.column), + }); + } + + let n = self.extract_int(&constraint.args[0])?; + let arr_vars = self.extract_var_array(&constraint.args[1])?; + let value = self.extract_int(&constraint.args[2])?; + + // Use Selen's at_most constraint + self.model.at_most(&arr_vars, value, n); + Ok(()) + } + + /// Map exactly: exactly n variables in array equal value + /// FlatZinc signature: fzn_exactly_int(n, x, v) + pub(in crate::mapper) fn map_exactly_int(&mut self, constraint: &Constraint) -> FlatZincResult<()> { + if constraint.args.len() != 3 { + return Err(FlatZincError::MapError { + message: "exactly_int requires 3 arguments (n, x, v)".to_string(), + line: Some(constraint.location.line), + column: Some(constraint.location.column), + }); + } + + let n = self.extract_int(&constraint.args[0])?; + let arr_vars = self.extract_var_array(&constraint.args[1])?; + let value = self.extract_int(&constraint.args[2])?; + + // Use Selen's exactly constraint + self.model.exactly(&arr_vars, value, n); + Ok(()) + } +} diff --git a/src/mapper/constraints/counting.rs b/src/mapper/constraints/counting.rs index 68a20d5..a843f63 100644 --- a/src/mapper/constraints/counting.rs +++ b/src/mapper/constraints/counting.rs @@ -23,7 +23,8 @@ impl<'a> MappingContext<'a> { let value = self.extract_int(&constraint.args[1])?; let count_var = self.get_var_or_const(&constraint.args[2])?; - // Use Selen's count constraint + // Use Selen's count constraint: count(&vars, value, count_var) + // This constrains: count_var = |{i : vars[i] = value}| self.model.count(&arr_vars, selen::variables::Val::ValI(value), count_var); Ok(()) } diff --git a/src/mapper/constraints/element.rs b/src/mapper/constraints/element.rs index f5962e2..b137f8a 100644 --- a/src/mapper/constraints/element.rs +++ b/src/mapper/constraints/element.rs @@ -12,33 +12,39 @@ use selen::variables::VarId; impl<'a> MappingContext<'a> { /// Map array_var_int_element: array[index] = value /// FlatZinc signature: array_var_int_element(index, array, value) + /// Gecode signature: gecode_int_element(index, idxoffset, array, value) /// Note: FlatZinc uses 1-based indexing, Selen uses 0-based pub(in crate::mapper) fn map_array_var_int_element(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { + // Handle both standard (3 args) and gecode (4 args with offset) variants + let (index_var, array, value) = if constraint.args.len() == 4 { + // gecode_int_element(idx, idxoffset, array, value) + let index = self.get_var_or_const(&constraint.args[0])?; + let offset = self.extract_int(&constraint.args[1])?; + let array = self.extract_var_array(&constraint.args[2])?; + let value = self.get_var_or_const(&constraint.args[3])?; + + // Convert: index_0based = index - offset + let index_0based = self.model.sub(index, selen::variables::Val::ValI(offset)); + (index_0based, array, value) + } else if constraint.args.len() == 3 { + // array_var_int_element(index, array, value) - standard 1-based + let index_1based = self.get_var_or_const(&constraint.args[0])?; + let array = self.extract_var_array(&constraint.args[1])?; + let value = self.get_var_or_const(&constraint.args[2])?; + + // Convert to 0-based index for Selen + let index_0based = self.model.sub(index_1based, selen::variables::Val::ValI(1)); + (index_0based, array, value) + } else { return Err(FlatZincError::MapError { - message: "array_var_int_element requires 3 arguments (index, array, value)".to_string(), + message: format!("array_var_int_element requires 3 or 4 arguments, got {}", constraint.args.len()), line: Some(constraint.location.line), column: Some(constraint.location.column), }); - } - - // Get index variable (1-based in FlatZinc) - // Supports: variables, array access (x[i]), integer literals - let index_1based = self.get_var_or_const(&constraint.args[0])?; - - // Convert to 0-based index for Selen - // Create: index_0based = index_1based - 1 - let index_0based = self.model.sub(index_1based, selen::variables::Val::ValI(1)); - - // Get array - let array = self.extract_var_array(&constraint.args[1])?; - - // Get value (can be variable, array access, or constant) - // Supports: variables, array access (y[j]), integer literals - let value = self.get_var_or_const(&constraint.args[2])?; + }; - // Apply element constraint: array[index_0based] = value - self.model.elem(&array, index_0based, value); + // Apply element constraint: array[index_var] = value + self.model.elem(&array, index_var, value); Ok(()) } diff --git a/src/mapper/constraints/global_cardinality.rs b/src/mapper/constraints/global_cardinality.rs index 301acfd..4d7b4c3 100644 --- a/src/mapper/constraints/global_cardinality.rs +++ b/src/mapper/constraints/global_cardinality.rs @@ -48,12 +48,10 @@ impl<'a> MappingContext<'a> { }); } - // For each value, create a count constraint - for (&value, &count_var) in values.iter().zip(counts.iter()) { - // Use Selen's count constraint: count(vars, value, count_var) - // This constrains: count_var = |{j : vars[j] = value}| - self.model.count(&vars, selen::variables::Val::ValI(value), count_var); - } + // Use Selen's gcc (global cardinality constraint) method + // gcc(&vars, values, counts) constrains that for each i, + // counts[i] = |{j : vars[j] = values[i]}| + self.model.gcc(&vars, &values, &counts); Ok(()) } @@ -103,19 +101,17 @@ impl<'a> MappingContext<'a> { }); } - // For each value, create a count variable and constrain it with bounds + // For each value, constrain count with bounds using at_least and at_most for i in 0..values.len() { let value = values[i]; let low_bound = low[i]; let up_bound = up[i]; - // Create a variable to hold the count with appropriate bounds - let count_var = self.model.int(low_bound, up_bound); - - // Use Selen's count constraint: count(vars, value, count_var) - // This constrains: count_var = |{j : vars[j] = value}| - // The count_var's domain already enforces low_bound <= count_var <= up_bound - self.model.count(&vars, selen::variables::Val::ValI(value), count_var); + // Use Selen's at_least and at_most constraints + // at_least(&vars, value, n) constrains: at least n vars == value + // at_most(&vars, value, n) constrains: at most n vars == value + self.model.at_least(&vars, value, low_bound); + self.model.at_most(&vars, value, up_bound); } Ok(()) diff --git a/src/mapper/constraints/mod.rs b/src/mapper/constraints/mod.rs index ec60414..7dd3d80 100644 --- a/src/mapper/constraints/mod.rs +++ b/src/mapper/constraints/mod.rs @@ -12,6 +12,7 @@ pub(super) mod array; pub(super) mod element; pub(super) mod arithmetic; pub(super) mod counting; +pub(super) mod cardinality; pub(super) mod set; pub(super) mod global_cardinality; pub(super) mod float; diff --git a/test_problems.sh b/test_problems.sh deleted file mode 100755 index 290de62..0000000 --- a/test_problems.sh +++ /dev/null @@ -1,69 +0,0 @@ -#!/bin/bash -# Test script for Zelen solver with hakank problems -# Usage: ./test_problems.sh [number_of_problems] - -cd "$(dirname "$0")/zinc/hakank" || exit 1 - -TIMEOUT=30 -TIME_LIMIT=25000 -NUM_PROBLEMS=${1:-50} - -echo "=== Testing $NUM_PROBLEMS problems with Zelen solver ===" -echo "Timeout: ${TIMEOUT}s, Time limit: ${TIME_LIMIT}ms" -echo "" - -passed=0 -failed=0 -skipped=0 - -# Get list of .mzn files -mzn_files=$(ls *.mzn | head -$NUM_PROBLEMS) - -for mzn in $mzn_files; do - base="${mzn%.mzn}" - - # Check if there are numbered data files (e.g., problem1.dzn, problem2.dzn) - dzn_files=$(ls ${base}[0-9]*.dzn 2>/dev/null | sort) - - if [ -n "$dzn_files" ]; then - # Multiple data files - test with first one only for speed - dzn=$(echo "$dzn_files" | head -1) - printf "%-45s [%s] " "$mzn" "$(basename $dzn)" - result=$(timeout $TIMEOUT minizinc --solver zelen --time-limit $TIME_LIMIT "$mzn" "$dzn" 2>&1) - elif [ -f "${base}.dzn" ]; then - # Single data file with same name - printf "%-45s [.dzn] " "$mzn" - result=$(timeout $TIMEOUT minizinc --solver zelen --time-limit $TIME_LIMIT "$mzn" "${base}.dzn" 2>&1) - else - # No data file needed - printf "%-45s " "$mzn" - result=$(timeout $TIMEOUT minizinc --solver zelen --time-limit $TIME_LIMIT "$mzn" 2>&1) - fi - - exit_code=$? - - if [ $exit_code -eq 124 ]; then - echo "⏱ TIMEOUT" - ((failed++)) - elif echo "$result" | grep -q "=========="; then - echo "✓ SOLVED" - ((passed++)) - elif echo "$result" | grep -q "=====UNSATISFIABLE====="; then - echo "✓ UNSAT" - ((passed++)) - elif echo "$result" | grep -qi "error"; then - echo "✗ ERROR" - ((failed++)) - # Uncomment to see error details: - # echo "$result" | grep -i error | head -3 - else - echo "✗ FAILED" - ((failed++)) - fi -done - -echo "" -echo "=========================================" -echo "RESULTS: $passed passed, $failed failed" -echo "Success rate: $(( passed * 100 / NUM_PROBLEMS ))%" -echo "========================================="