minion_sys/ast.rs
1//! Types used for representing Minion models in Rust.
2
3use std::{collections::HashMap, fmt::Display};
4
5use crate::print::{
6 print_const_array, print_constraint_array, print_short_tuple_array, print_tuple_array,
7 print_var_array,
8};
9
10/// The name of a variable in a Minion model.
11pub type VarName = String;
12/// A tuple of constants, used in extensional (table) constraints.
13pub type Tuple = Vec<Constant>;
14/// A short tuple — used by short-tuple constraints (`shortstr2`,
15/// `haggisgac`, `haggisgac-stable`, `shortctuplestr2`). Each entry
16/// is a `(variable_index, value)` literal; the position refers to
17/// the constraint's variable list. For `shortstr2` /
18/// `haggisgac` / `haggisgac-stable` the indexes within one short
19/// tuple must be distinct (the propagators reject duplicates).
20/// `shortctuplestr2` allows multiple entries for the same index
21/// (OR semantics within that short tuple).
22pub type ShortTuple = Vec<(usize, Constant)>;
23/// A pair of variables, used by three-operand arithmetic constraints.
24pub type TwoVars = (Var, Var);
25
26/// A Minion model.
27#[non_exhaustive]
28#[derive(Debug, Clone, PartialEq, Eq)]
29pub struct Model {
30 pub named_variables: SymbolTable,
31 pub constraints: Vec<Constraint>,
32 /// Named tuple tables. Needed by tuple-based constraints that
33 /// reference a table by name rather than carry tuples inline
34 /// (most notably `CT_STR` / `Str2Plus`). Register a table with
35 /// [`Model::add_tuple_table`], then reference it from a
36 /// constraint via `Var::NameRef(table_name)`.
37 ///
38 /// Storage order is preserved so the order in which tables are
39 /// installed into the `CSPInstance` matches insertion order.
40 pub tuple_tables: Vec<(String, Vec<Tuple>)>,
41 /// Optional single-objective optimisation directive. When set,
42 /// minion treats the run as `MINIMISING`/`MAXIMISING` on the
43 /// chosen variable; the best objective value found is reported
44 /// via [`SolverContext::get_from_table`] under the key
45 /// `"OptimumValue"` (with `"OptimumDirection"` returning
46 /// `"min"` or `"max"`).
47 pub optimise: Option<Optimise>,
48}
49
50/// Single-objective optimisation directive carried on
51/// [`Model::optimise`].
52#[derive(Debug, Clone, PartialEq, Eq)]
53pub struct Optimise {
54 pub minimise: bool,
55 pub var: Var,
56}
57
58impl Model {
59 /// Creates an empty Minion model.
60 pub fn new() -> Model {
61 Model {
62 named_variables: SymbolTable::new(),
63 constraints: Vec::new(),
64 tuple_tables: Vec::new(),
65 optimise: None,
66 }
67 }
68
69 /// Registers a named tuple table on the model. The table is
70 /// copied into Minion's `CSPInstance` at solve time so constraints
71 /// like `Str2Plus(vars, Var::NameRef(name))` can look it up.
72 ///
73 /// Returns `None` if a table with that name is already registered.
74 pub fn add_tuple_table(&mut self, name: String, tuples: Vec<Tuple>) -> Option<()> {
75 if self.tuple_tables.iter().any(|(n, _)| n == &name) {
76 return None;
77 }
78 self.tuple_tables.push((name, tuples));
79 Some(())
80 }
81}
82
83impl Default for Model {
84 fn default() -> Self {
85 Self::new()
86 }
87}
88
89/// All supported Minion constraints.
90///
91/// Each variant corresponds to a Minion input-language constraint (see the
92/// [Minion constraint reference](https://minion-solver.readthedocs.io/en/latest/usage/constraints.html)).
93/// Variants are named to match their Minion input names as closely as Rust's
94/// naming conventions permit.
95///
96/// # Argument conventions
97///
98/// - `Vec<Var>` is a list of variables.
99/// - `Var` alone is a single variable (or `Var::ConstantAsVar` for a constant in
100/// variable position).
101/// - `Vec<Constant>` is a list of integer constants (e.g. weights, values).
102/// - `Constant` alone is a single integer constant.
103/// - `(Var, Var)` in the `TwoVars` position means two variables.
104/// - `Vec<Tuple>` is a list of tuples (a `Tuple` is a `Vec<Constant>`).
105/// - `Box<Constraint>` means the variant wraps another constraint (reification,
106/// nested boolean operators, etc.).
107#[non_exhaustive]
108#[derive(Debug, Clone, PartialEq, Eq)]
109pub enum Constraint {
110 // --- Arithmetic: three-operand (x, y, z) ---
111 /// `difference(x, y, z)` — `z = |x - y|`. Bounds consistency.
112 Difference(TwoVars, Var),
113 /// `div(x, y, z)` — `z = floor(x / y)`. False when `y = 0`.
114 Div(TwoVars, Var),
115 /// `div_undefzero(x, y, z)` — like `Div`, but true (not false) when `y = 0`.
116 DivUndefZero(TwoVars, Var),
117 /// `modulo(x, y, z)` — `z = x % y`. False when `y = 0`.
118 Modulo(TwoVars, Var),
119 /// `modulo_undefzero(x, y, z)` — like `Modulo`, but true when `y = 0`.
120 ModuloUndefZero(TwoVars, Var),
121 /// `pow(x, y, z)` — `z = x^y`. False when `y < 0` (with exceptions for ±1).
122 Pow(TwoVars, Var),
123 /// `product(x, y, z)` — `z = x * y`.
124 Product(TwoVars, Var),
125
126 // --- Arithmetic: weighted sums ---
127 /// `weightedsumgeq(weights, vars, total)` — dot product ≥ total.
128 WeightedSumGeq(Vec<Constant>, Vec<Var>, Var),
129 /// `weightedsumleq(weights, vars, total)` — dot product ≤ total.
130 WeightedSumLeq(Vec<Constant>, Vec<Var>, Var),
131
132 // --- Nested / meta constraints ---
133 /// `check[assign](c)` — internal: checks `c` after each assignment.
134 CheckAssign(Box<Constraint>),
135 /// `check[gsa](c)` — internal: checks `c` via GSA (generalised-scope-all).
136 CheckGsa(Box<Constraint>),
137 /// `forwardchecking(c)` — internal: run `c` in forward-checking mode.
138 ForwardChecking(Box<Constraint>),
139 /// `reify(c, r)` — `r = 1` iff `c` is satisfied. `r` must be 0/1.
140 Reify(Box<Constraint>, Var),
141 /// `reifyimply(c, r)` — if `r = 1` then `c` must hold.
142 ReifyImply(Box<Constraint>, Var),
143 /// `reifyimply-quick(c, r)` — like `ReifyImply` but only checks `c` when `r` is assigned.
144 ReifyImplyQuick(Box<Constraint>, Var),
145 /// `watched-and({c1, ..., cn})` — all `ci` must be true.
146 WatchedAnd(Vec<Constraint>),
147 /// `watched-or({c1, ..., cn})` — at least one `ci` must be true.
148 WatchedOr(Vec<Constraint>),
149
150 // --- All-different / cardinality / counting ---
151 /// `gacalldiff(vars)` — all variables in `vars` take distinct values. GAC.
152 GacAllDiff(Vec<Var>),
153 /// `alldiff(vars)` — like `GacAllDiff` but weaker (clique of ≠ constraints).
154 AllDiff(Vec<Var>),
155 /// `alldiffmatrix(matrix, dim)` — Latin-square condition on a `dim×dim` matrix.
156 AllDiffMatrix(Vec<Var>, Constant),
157
158 // --- SAT-style sums (Booleans only) ---
159 /// `watchsumgeq(vars, c)` — sum of 0/1 `vars` ≥ `c`. Fast for small `c`.
160 WatchSumGeq(Vec<Var>, Constant),
161 /// `watchsumleq(vars, c)` — sum of 0/1 `vars` ≤ `c`. Fast for `c` close to len.
162 WatchSumLeq(Vec<Var>, Constant),
163
164 // --- Occurrence ---
165 /// `occurrencegeq(vars, val, count)` — `val` occurs ≥ `count` times. Constants only.
166 OccurrenceGeq(Vec<Var>, Constant, Constant),
167 /// `occurrenceleq(vars, val, count)` — `val` occurs ≤ `count` times. Constants only.
168 OccurrenceLeq(Vec<Var>, Constant, Constant),
169 /// `occurrence(vars, val, count)` — `val` occurs exactly `count` times.
170 Occurrence(Vec<Var>, Constant, Var),
171
172 // --- Literal sum ---
173 /// `litsumgeq(vars, literals, c)` — at least `c` positions where `vars[i] == literals[i]`.
174 LitSumGeq(Vec<Var>, Vec<Constant>, Constant),
175
176 // --- Global cardinality ---
177 /// `gcc(vars, values, caps)` — each value in `values` appears exactly `caps[i]` times. Strong propagation.
178 Gcc(Vec<Var>, Vec<Constant>, Vec<Var>),
179 /// `gccweak(vars, values, caps)` — like `Gcc` but weaker, faster propagation on `caps`.
180 GccWeak(Vec<Var>, Vec<Constant>, Vec<Var>),
181
182 // --- Lexicographic ordering ---
183 /// `lexleq[rv](a, b)` — `a ≤ b` lexicographically. GAC, handles repeated variables.
184 LexLeqRv(Vec<Var>, Vec<Var>),
185 /// `lexleq(a, b)` — `a ≤ b` lexicographically. GAC, assumes no repeated variables.
186 LexLeq(Vec<Var>, Vec<Var>),
187 /// `lexless(a, b)` — `a < b` lexicographically. GAC, assumes no repeated variables.
188 LexLess(Vec<Var>, Vec<Var>),
189 /// `lexleq[quick](a, b)` — `a ≤ b` lexicographically. Fast but weaker propagation.
190 LexLeqQuick(Vec<Var>, Vec<Var>),
191 /// `lexless[quick](a, b)` — `a < b` lexicographically. Fast but weaker propagation.
192 LexLessQuick(Vec<Var>, Vec<Var>),
193
194 // --- Vector comparison ---
195 /// `watchvecneq(a, b)` — vectors `a` and `b` differ in at least one position.
196 WatchVecNeq(Vec<Var>, Vec<Var>),
197 /// `watchvecexists_less(a, b)` — there exists `i` such that `a[i] < b[i]`.
198 WatchVecExistsLess(Vec<Var>, Vec<Var>),
199 /// `hamming(a, b, c)` — Hamming distance between `a` and `b` ≥ `c`.
200 Hamming(Vec<Var>, Vec<Var>, Constant),
201 /// `not-hamming(a, b, c)` — Hamming distance between `a` and `b` < `c`.
202 NotHamming(Vec<Var>, Vec<Var>, Constant),
203
204 // --- Internal ---
205 /// `frameupdate(...)` — internal frame-update constraint.
206 FrameUpdate(Vec<Var>, Vec<Var>, Vec<Var>, Vec<Var>, Constant),
207
208 // --- Table (extensional) constraints ---
209 /// `negativetable(vars, tuples)` — disallows the given tuples. GAC.
210 NegativeTable(Vec<Var>, Vec<Tuple>),
211 /// `table(vars, tuples)` — allows only the given tuples. GAC.
212 Table(Vec<Var>, Vec<Tuple>),
213 /// `gacschema(vars, tuples)` — like `Table` with an alternative GAC algorithm.
214 GacSchema(Vec<Var>, Vec<Tuple>),
215 /// `lighttable(vars, tuples)` — stateless variant of `Table`, faster for small constraints.
216 LightTable(Vec<Var>, Vec<Tuple>),
217 /// `mddc(vars, tuples)` — MDDC propagator (multi-valued decision diagram). GAC.
218 Mddc(Vec<Var>, Vec<Tuple>),
219 /// `negativemddc(vars, tuples)` — negative MDDC. GAC on disallowed tuples.
220 NegativeMddc(Vec<Var>, Vec<Tuple>),
221 /// `str2plus(vars, table_ref)` — STR2+ algorithm. The second argument is a
222 /// `Var::NameRef` referencing a named tuple table registered with
223 /// [`Model::add_tuple_table`].
224 Str2Plus(Vec<Var>, Var),
225
226 // --- Short-tuple constraints ---
227 /// `shortstr2(vars, short_tuples)` — STR2+ over a short-tuple list.
228 /// Each short tuple is a partial assignment; an assignment satisfies
229 /// the constraint iff some short tuple's literals match. GAC.
230 /// Indexes within one short tuple must be distinct.
231 ShortStr2(Vec<Var>, Vec<ShortTuple>),
232 /// `haggisgac(vars, short_tuples)` — HaggisGAC over short tuples.
233 /// Same semantics as `ShortStr2`; different propagator. Discrete vars only.
234 HaggisGac(Vec<Var>, Vec<ShortTuple>),
235 /// `haggisgac-stable(vars, short_tuples)` — backtrack-stable HaggisGAC.
236 /// Same semantics as `HaggisGac`. Discrete vars only.
237 HaggisGacStable(Vec<Var>, Vec<ShortTuple>),
238 /// `shortctuplestr2(vars, short_tuples)` — STR2+ over short cTuples.
239 /// Like `ShortStr2` but allows multiple `(idx, val)` literals for the
240 /// same `idx` within one short tuple (OR semantics for that variable).
241 /// Discrete vars only.
242 ShortCTupleStr2(Vec<Var>, Vec<ShortTuple>),
243
244 // --- Min/max / nvalue ---
245 /// `max(vars, x)` — `x` equals the maximum value in `vars`.
246 Max(Vec<Var>, Var),
247 /// `min(vars, x)` — `x` equals the minimum value in `vars`.
248 Min(Vec<Var>, Var),
249 /// `nvaluegeq(vars, x)` — at least `x` distinct values appear in `vars`.
250 NvalueGeq(Vec<Var>, Var),
251 /// `nvalueleq(vars, x)` — at most `x` distinct values appear in `vars`.
252 NvalueLeq(Vec<Var>, Var),
253
254 // --- Sums ---
255 /// `sumleq(vars, x)` — sum of `vars` ≤ `x`.
256 SumLeq(Vec<Var>, Var),
257 /// `sumgeq(vars, x)` — sum of `vars` ≥ `x`.
258 SumGeq(Vec<Var>, Var),
259
260 // --- Element (array access) ---
261 /// `element(vec, i, e)` — `vec[i] = e`. 0-indexed. Not confluent.
262 Element(Vec<Var>, Var, Var),
263 /// `element_one(vec, i, e)` — like `Element`, 1-indexed.
264 ElementOne(Vec<Var>, Var, Var),
265 /// `element_undefzero(vec, i, e)` — like `Element`, but true with `e=0` when `i` is out of bounds.
266 ElementUndefZero(Vec<Var>, Var, Var),
267 /// `watchelement(vec, i, e)` — like `Element` but watched and GAC.
268 WatchElement(Vec<Var>, Var, Var),
269 /// `watchelement_one(vec, i, e)` — like `WatchElement`, 1-indexed.
270 WatchElementOne(Vec<Var>, Var, Var),
271 /// `watchelement_one_undefzero(vec, i, e)` — like `WatchElementOne` with undefzero semantics.
272 WatchElementOneUndefZero(Vec<Var>, Var, Var),
273 /// `watchelement_undefzero(vec, i, e)` — like `WatchElement` with undefzero semantics.
274 WatchElementUndefZero(Vec<Var>, Var, Var),
275
276 // --- Unary constraints ---
277 /// `w-literal(x, a)` — `x = a`.
278 WLiteral(Var, Constant),
279 /// `w-notliteral(x, a)` — `x ≠ a`.
280 WNotLiteral(Var, Constant),
281 /// `w-inintervalset(x, [a1,a2, b1,b2, ...])` — `x` is in one of the intervals.
282 WInIntervalSet(Var, Vec<Constant>),
283 /// `w-inrange(x, [a, b])` — `a ≤ x ≤ b`.
284 WInRange(Var, Vec<Constant>),
285 /// `w-inset(x, vals)` — `x` is in the set `vals`.
286 WInset(Var, Vec<Constant>),
287 /// `w-notinrange(x, [a, b])` — `x < a` or `x > b`.
288 WNotInRange(Var, Vec<Constant>),
289 /// `w-notinset(x, vals)` — `x` is not in the set `vals`.
290 WNotInset(Var, Vec<Constant>),
291
292 // --- Binary arithmetic / comparison ---
293 /// `abs(x, y)` — `x = |y|`.
294 Abs(Var, Var),
295 /// `diseq(x, y)` — `x ≠ y`. Arc consistency.
296 DisEq(Var, Var),
297 /// `eq(x, y)` — `x = y`. Bounds consistency.
298 Eq(Var, Var),
299 /// `minuseq(x, y)` — `x = -y`. Bounds consistency.
300 MinusEq(Var, Var),
301 /// `gaceq(x, y)` — `x = y`. GAC.
302 GacEq(Var, Var),
303 /// `watchless(x, y)` — `x < y`. Watched.
304 WatchLess(Var, Var),
305 /// `watchneq(x, y)` — `x ≠ y`. Watched (may be faster when one var is assigned early).
306 WatchNeq(Var, Var),
307 /// `ineq(x, y, k)` — `x ≤ y + k`. `k` must be a constant.
308 Ineq(Var, Var, Constant),
309
310 // --- Constant ---
311 /// `false` — always false. Makes a model unsatisfiable.
312 False,
313 /// `true` — always true.
314 True,
315}
316
317#[allow(clippy::todo, unused_variables)]
318impl Display for Constraint {
319 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
320 match self {
321 Constraint::Difference((a, b), var) => write!(f, "difference({a},{b},{var})"),
322 Constraint::Div((a, b), var) => write!(f, "div({a},{b},{var})"),
323 Constraint::DivUndefZero((a, b), var) => write!(f, "div_undefzero({a},{b},{var})"),
324 Constraint::Modulo((a, b), var) => write!(f, "modulo({a},{b},{var})"),
325 Constraint::ModuloUndefZero((a, b), var) => {
326 write!(f, "modulo_undefzero({a},{b},{var})")
327 }
328 Constraint::Pow((a, b), var) => write!(f, "pow({a},{b},{var})"),
329 Constraint::Product((a, b), var) => write!(f, "product({a},{b},{var})"),
330 Constraint::WeightedSumGeq(constants, vars, var) => {
331 write!(
332 f,
333 "weightedsumgeq({},{},{var})",
334 print_const_array(constants),
335 print_var_array(vars)
336 )
337 }
338 Constraint::WeightedSumLeq(constants, vars, var) => {
339 write!(
340 f,
341 "weightedsumleq({},{},{var})",
342 print_const_array(constants),
343 print_var_array(vars)
344 )
345 }
346 Constraint::CheckAssign(constraint) => write!(f, "check[assign]({constraint})"),
347 Constraint::CheckGsa(constraint) => write!(f, "check[gsa]({constraint})"),
348 Constraint::ForwardChecking(constraint) => {
349 write!(f, "forwardchecking({constraint})")
350 }
351 Constraint::Reify(constraint, var) => write!(f, "reify({constraint},{var})"),
352 Constraint::ReifyImply(constraint, var) => write!(f, "reifyimply({constraint},{var})"),
353 Constraint::ReifyImplyQuick(constraint, var) => {
354 write!(f, "reifyimply-quick({constraint},{var})")
355 }
356 Constraint::WatchedAnd(constraints) => {
357 write!(f, "watched-and({})", print_constraint_array(constraints))
358 }
359 Constraint::WatchedOr(constraints) => {
360 write!(f, "watched-or({})", print_constraint_array(constraints))
361 }
362 Constraint::GacAllDiff(vars) => write!(f, "gacalldiff({})", print_var_array(vars)),
363 Constraint::AllDiff(vars) => write!(f, "alldiff({})", print_var_array(vars)),
364 Constraint::AllDiffMatrix(vars, constant) => {
365 write!(f, "alldiffmatrix({},{constant})", print_var_array(vars))
366 }
367 Constraint::WatchSumGeq(vars, constant) => {
368 write!(f, "watchsumgeq({},{constant})", print_var_array(vars))
369 }
370 Constraint::WatchSumLeq(vars, constant) => {
371 write!(f, "watchsumleq({},{constant})", print_var_array(vars))
372 }
373 Constraint::OccurrenceGeq(vars, constant, constant1) => write!(
374 f,
375 "occurrencegeq({},{constant},{constant1})",
376 print_var_array(vars)
377 ),
378 Constraint::OccurrenceLeq(vars, constant, constant1) => write!(
379 f,
380 "occurrenceleq({},{constant},{constant1})",
381 print_var_array(vars)
382 ),
383 Constraint::Occurrence(vars, constant, var) => {
384 write!(f, "occurrence({},{constant},{var})", print_var_array(vars))
385 }
386 Constraint::LitSumGeq(vars, constants, constant) => write!(
387 f,
388 "litsumgeq({},{},{constant})",
389 print_var_array(vars),
390 print_const_array(constants)
391 ),
392 Constraint::Gcc(vars, constants, vars1) => write!(
393 f,
394 "gcc({},{},{})",
395 print_var_array(vars),
396 print_const_array(constants),
397 print_var_array(vars1)
398 ),
399 Constraint::GccWeak(vars, constants, vars1) => write!(
400 f,
401 "gccweak({},{},{})",
402 print_var_array(vars),
403 print_const_array(constants),
404 print_var_array(vars1)
405 ),
406 Constraint::LexLeqRv(vars, vars1) => write!(
407 f,
408 "lexleq[rv]({},{})",
409 print_var_array(vars),
410 print_var_array(vars1)
411 ),
412 Constraint::LexLeq(vars, vars1) => write!(
413 f,
414 "lexleq({},{})",
415 print_var_array(vars),
416 print_var_array(vars1)
417 ),
418 Constraint::LexLeqQuick(vars, vars1) => write!(
419 f,
420 "lexleq[quick]({},{})",
421 print_var_array(vars),
422 print_var_array(vars1)
423 ),
424 Constraint::LexLess(vars, vars1) => write!(
425 f,
426 "lexless({},{})",
427 print_var_array(vars),
428 print_var_array(vars1)
429 ),
430 Constraint::LexLessQuick(vars, vars1) => write!(
431 f,
432 "lexless[quick]({},{})",
433 print_var_array(vars),
434 print_var_array(vars1)
435 ),
436 Constraint::WatchVecNeq(vars, vars1) => write!(
437 f,
438 "watchvecneq({},{})",
439 print_var_array(vars),
440 print_var_array(vars1)
441 ),
442 Constraint::WatchVecExistsLess(vars, vars1) => write!(
443 f,
444 "watchvecexists_less({},{})",
445 print_var_array(vars),
446 print_var_array(vars1)
447 ),
448 Constraint::Hamming(vars, vars1, constant) => write!(
449 f,
450 "hamming({},{},{constant})",
451 print_var_array(vars),
452 print_var_array(vars1)
453 ),
454 Constraint::NotHamming(vars, vars1, constant) => write!(
455 f,
456 "not-hamming({},{},{constant})",
457 print_var_array(vars),
458 print_var_array(vars1)
459 ),
460 Constraint::FrameUpdate(vars, vars1, vars2, vars3, constant) => write!(
461 f,
462 "frameupdate({},{},{},{},{constant})",
463 print_var_array(vars),
464 print_var_array(vars1),
465 print_var_array(vars2),
466 print_var_array(vars3)
467 ),
468 Constraint::Table(vars, tuples) => {
469 write!(
470 f,
471 "table({},{})",
472 print_var_array(vars),
473 print_tuple_array(tuples)
474 )
475 }
476 Constraint::NegativeTable(vars, tuples) => {
477 write!(
478 f,
479 "negativetable({},{})",
480 print_var_array(vars),
481 print_tuple_array(tuples)
482 )
483 }
484 Constraint::GacSchema(vars, tuples) => {
485 write!(
486 f,
487 "gacschema({},{})",
488 print_var_array(vars),
489 print_tuple_array(tuples)
490 )
491 }
492 Constraint::LightTable(vars, tuples) => {
493 write!(
494 f,
495 "lighttable({},{})",
496 print_var_array(vars),
497 print_tuple_array(tuples)
498 )
499 }
500 Constraint::Mddc(vars, tuples) => {
501 write!(
502 f,
503 "mddc({},{})",
504 print_var_array(vars),
505 print_tuple_array(tuples)
506 )
507 }
508 Constraint::NegativeMddc(vars, tuples) => {
509 write!(
510 f,
511 "negativemddc({},{})",
512 print_var_array(vars),
513 print_tuple_array(tuples)
514 )
515 }
516 Constraint::Str2Plus(vars, table_var) => {
517 write!(f, "str2plus({},{table_var})", print_var_array(vars))
518 }
519 Constraint::ShortStr2(vars, short) => write!(
520 f,
521 "shortstr2({},{})",
522 print_var_array(vars),
523 print_short_tuple_array(short)
524 ),
525 Constraint::HaggisGac(vars, short) => write!(
526 f,
527 "haggisgac({},{})",
528 print_var_array(vars),
529 print_short_tuple_array(short)
530 ),
531 Constraint::HaggisGacStable(vars, short) => write!(
532 f,
533 "haggisgac-stable({},{})",
534 print_var_array(vars),
535 print_short_tuple_array(short)
536 ),
537 Constraint::ShortCTupleStr2(vars, short) => write!(
538 f,
539 "shortctuplestr2({},{})",
540 print_var_array(vars),
541 print_short_tuple_array(short)
542 ),
543 Constraint::Max(vars, var) => write!(f, "max({},{var})", print_var_array(vars)),
544 Constraint::Min(vars, var) => write!(f, "min({},{var})", print_var_array(vars)),
545 Constraint::NvalueGeq(vars, var) => {
546 write!(f, "nvaluegeq({},{var})", print_var_array(vars))
547 }
548 Constraint::NvalueLeq(vars, var) => {
549 write!(f, "nvalueleq({},{var})", print_var_array(vars))
550 }
551 Constraint::SumLeq(vars, var) => write!(f, "sumleq({},{var})", print_var_array(vars)),
552 Constraint::SumGeq(vars, var) => write!(f, "sumgeq({},{var})", print_var_array(vars)),
553 Constraint::Element(vars, var, var1) => {
554 write!(f, "element({},{var},{var1})", print_var_array(vars))
555 }
556 Constraint::ElementOne(vars, var, var1) => {
557 write!(f, "element_one({},{var},{var1})", print_var_array(vars))
558 }
559 Constraint::ElementUndefZero(vars, var, var1) => write!(
560 f,
561 "element_undefzero({},{var},{var1})",
562 print_var_array(vars)
563 ),
564 Constraint::WatchElement(vars, var, var1) => {
565 write!(f, "watchelement({},{var},{var1})", print_var_array(vars))
566 }
567 Constraint::WatchElementUndefZero(vars, var, var1) => write!(
568 f,
569 "watchelement_undefzero({},{var},{var1})",
570 print_var_array(vars)
571 ),
572 Constraint::WatchElementOne(vars, var, var1) => write!(
573 f,
574 "watchelement_one({},{var},{var1})",
575 print_var_array(vars)
576 ),
577 Constraint::WatchElementOneUndefZero(vars, var, var1) => write!(
578 f,
579 "watchelement_one_undefzero({},{var},{var1})",
580 print_var_array(vars)
581 ),
582 Constraint::WLiteral(var, constant) => write!(f, "w-literal({var},{constant})"),
583 Constraint::WNotLiteral(var, constant) => write!(f, "w-notliteral({var},{constant})"),
584 Constraint::WInIntervalSet(var, constants) => {
585 write!(f, "w-inintervalset({var},{})", print_const_array(constants))
586 }
587 Constraint::WInRange(var, constants) => {
588 write!(f, "w-inrange({var},{})", print_const_array(constants))
589 }
590 Constraint::WNotInRange(var, constants) => {
591 write!(f, "w-notinrange({var},{})", print_const_array(constants))
592 }
593 Constraint::WInset(var, constants) => {
594 write!(f, "w-inset({var},{})", print_const_array(constants))
595 }
596 Constraint::WNotInset(var, constants) => {
597 write!(f, "w-notinset({var},{})", print_const_array(constants))
598 }
599 Constraint::Abs(var, var1) => write!(f, "abs({var},{var1})"),
600 Constraint::DisEq(var, var1) => write!(f, "diseq({var},{var1})"),
601 Constraint::Eq(var, var1) => write!(f, "eq({var},{var1})"),
602 Constraint::MinusEq(var, var1) => write!(f, "minuseq({var},{var1})"),
603 Constraint::GacEq(var, var1) => write!(f, "gaceq({var},{var1})"),
604 Constraint::WatchLess(var, var1) => write!(f, "watchless({var},{var1})"),
605 Constraint::WatchNeq(var, var1) => write!(f, "watchneq({var},{var1})"),
606 Constraint::Ineq(var, var1, constant) => write!(f, "ineq({var},{var1},{constant})"),
607 Constraint::False => write!(f, "false"),
608 Constraint::True => write!(f, "true"),
609 }
610 }
611}
612
613/// Representation of a Minion Variable.
614///
615/// A variable can either be a named variable, or an anomynous "constant as a variable".
616///
617/// The latter is not stored in the symbol table, or counted in Minions internal list of all
618/// variables, but is used to allow the use of a constant in the place of a variable in a
619/// constraint.
620#[derive(Debug, Clone, Eq, PartialEq)]
621pub enum Var {
622 NameRef(VarName),
623 ConstantAsVar(i32),
624}
625
626impl Display for Var {
627 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
628 match self {
629 Var::NameRef(n) => write!(f, "{n}"),
630 Var::ConstantAsVar(c) => write!(f, "{c}"),
631 }
632 }
633}
634/// Representation of a Minion constant.
635#[non_exhaustive]
636#[derive(Debug, Eq, PartialEq, Clone, Copy)]
637pub enum Constant {
638 Bool(bool),
639 Integer(i32),
640}
641
642impl Display for Constant {
643 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
644 match self {
645 Constant::Bool(true) => write!(f, "1"),
646 Constant::Bool(false) => write!(f, "0"),
647 Constant::Integer(i) => write!(f, "{i}"),
648 }
649 }
650}
651
652/// Representation of variable domains.
653#[derive(Debug, Clone, Eq, PartialEq)]
654#[non_exhaustive]
655pub enum VarDomain {
656 /// A bound variable with domain `[lower, upper]`. O(1) memory. The solver
657 /// only tracks bound changes during search.
658 Bound(i32, i32),
659 /// A discrete variable with domain `[lower, upper]`. O(domain size) memory.
660 /// Supports arbitrary subset removal. Prefer for domains up to ~1000 values.
661 Discrete(i32, i32),
662 /// Sparse bound variable with an explicit non-contiguous set of domain values.
663 /// Unlike Bound/Discrete which take [lower, upper] ranges, this carries the
664 /// full domain, e.g. `SparseBound(vec![-5, -2, 0, 3, 7])`.
665 SparseBound(Vec<i32>),
666 /// A Boolean variable with domain `{0, 1}`.
667 Bool,
668}
669
670#[derive(Debug, Clone, Eq, PartialEq)]
671#[non_exhaustive]
672/// Stores all named variables in a Minion model alongside their domains.
673///
674/// Named variables referenced in [constraints](Constraint) must be in the symbol table for the
675/// model to be valid. In the future, this will raise some sort of type error.
676pub struct SymbolTable {
677 table: HashMap<VarName, VarDomain>,
678
679 // order of all variables
680 var_order: Vec<VarName>,
681
682 // search order
683 search_var_order: Vec<VarName>,
684}
685
686impl SymbolTable {
687 fn new() -> SymbolTable {
688 SymbolTable {
689 table: HashMap::new(),
690 var_order: Vec::new(),
691 search_var_order: Vec::new(),
692 }
693 }
694
695 /// Creates a new search variable and adds it to the symbol table.
696 ///
697 /// # Returns
698 ///
699 /// If a variable already exists with the given name, `None` is returned.
700 pub fn add_var(&mut self, name: VarName, vartype: VarDomain) -> Option<()> {
701 if self.table.contains_key(&name) {
702 return None;
703 }
704
705 self.table.insert(name.clone(), vartype);
706 self.var_order.push(name.clone());
707 self.search_var_order.push(name);
708
709 Some(())
710 }
711
712 /// Creates a new auxiliary variable and adds it to the symbol table.
713 ///
714 /// The variable is excluded from Minion's primary search order, but is
715 /// still branched on: the runner appends every auxiliary variable to a
716 /// trailing find-one-assignment search block, mirroring what Minion's
717 /// text parser does with variables omitted from `VARORDER`. Auxiliary
718 /// variables appear in the print order, and so in solutions.
719 ///
720 /// # Returns
721 ///
722 /// If a variable already exists with the given name, `None` is returned.
723 pub fn add_aux_var(&mut self, name: VarName, vartype: VarDomain) -> Option<()> {
724 if self.table.contains_key(&name) {
725 return None;
726 }
727
728 self.table.insert(name.clone(), vartype);
729 self.var_order.push(name);
730
731 Some(())
732 }
733
734 /// Gets the domain of a named variable.
735 ///
736 /// # Returns
737 ///
738 /// `None` if no variable is known by that name.
739 pub fn get_vartype(&self, name: VarName) -> Option<VarDomain> {
740 self.table.get(&name).cloned()
741 }
742
743 /// Gets the canonical ordering of all variables.
744 pub fn get_variable_order(&self) -> Vec<VarName> {
745 self.var_order.clone()
746 }
747
748 /// Gets the canonical ordering of search variables (i.e excluding aux vars).
749 pub fn get_search_variable_order(&self) -> Vec<VarName> {
750 self.search_var_order.clone()
751 }
752
753 /// Returns `true` if a variable with the given name exists in the symbol table.
754 pub fn contains(&self, name: VarName) -> bool {
755 self.table.contains_key(&name)
756 }
757}