Add integer GCD, divisibility, and n-ary product constraints

Makefile.dep

@@ -2144,6 +2144,8 @@ gecode/int/count$(OBJSUFFIX) gecode/int/count$(SBJSUFFIX): \
 	./gecode/support/sort.hpp ./gecode/support/static-stack.hpp ./gecode/support/thread.hpp \
 	./gecode/support/thread/thread.hpp ./gecode/support/timer.hpp
 gecode/int/arithmetic$(OBJSUFFIX) gecode/int/arithmetic$(SBJSUFFIX): \
+	./gecode/int/arithmetic/gcd.hpp ./gecode/int/arithmetic/divides.hpp \
+	./gecode/int/arithmetic/product.hpp ./gecode/int/arithmetic/product-mod.hpp \
 	./gecode/int.hh ./gecode/int/arithmetic.hh ./gecode/int/arithmetic/abs.hpp \
 	./gecode/int/arithmetic/argmax.hpp ./gecode/int/arithmetic/divmod.hpp ./gecode/int/arithmetic/max.hpp \
 	./gecode/int/arithmetic/mult.hpp ./gecode/int/arithmetic/nroot.hpp ./gecode/int/arithmetic/pow-ops.hpp \
@@ -4441,6 +4443,8 @@ gecode/int/branch/chb$(OBJSUFFIX) gecode/int/branch/chb$(SBJSUFFIX): \
 	./gecode/support/sort.hpp ./gecode/support/static-stack.hpp ./gecode/support/thread.hpp \
 	./gecode/support/thread/thread.hpp ./gecode/support/timer.hpp
 gecode/int/arithmetic/mult$(OBJSUFFIX) gecode/int/arithmetic/mult$(SBJSUFFIX): \
+	./gecode/int/arithmetic/gcd.hpp ./gecode/int/arithmetic/divides.hpp \
+	./gecode/int/arithmetic/product.hpp ./gecode/int/arithmetic/product-mod.hpp \
 	./gecode/int.hh ./gecode/int/arithmetic.hh ./gecode/int/arithmetic/abs.hpp \
 	./gecode/int/arithmetic/argmax.hpp ./gecode/int/arithmetic/divmod.hpp ./gecode/int/arithmetic/max.hpp \
 	./gecode/int/arithmetic/mult.hpp ./gecode/int/arithmetic/nroot.hpp ./gecode/int/arithmetic/pow-ops.hpp \
@@ -19260,6 +19264,20 @@ test/int/channel$(OBJSUFFIX) test/int/channel$(SBJSUFFIX): \
 	./test/int.hh ./test/int.hpp ./test/test.hh \
 	./test/test.hpp
 test/int/arithmetic$(OBJSUFFIX) test/int/arithmetic$(SBJSUFFIX): \
+	./gecode/int/arithmetic.hh ./gecode/int/arithmetic/abs.hpp ./gecode/int/arithmetic/argmax.hpp \
+	./gecode/int/arithmetic/divides.hpp ./gecode/int/arithmetic/divmod.hpp ./gecode/int/arithmetic/gcd.hpp \
+	./gecode/int/arithmetic/max.hpp ./gecode/int/arithmetic/mult.hpp ./gecode/int/arithmetic/nroot.hpp \
+	./gecode/int/arithmetic/pow-ops.hpp ./gecode/int/arithmetic/pow.hpp ./gecode/int/arithmetic/product-mod.hpp \
+	./gecode/int/arithmetic/product.hpp ./gecode/int/bool.hh ./gecode/int/bool/base.hpp \
+	./gecode/int/bool/clause.hpp ./gecode/int/bool/eq.hpp ./gecode/int/bool/eqv.hpp \
+	./gecode/int/bool/ite.hpp ./gecode/int/bool/lq.hpp ./gecode/int/bool/or.hpp \
+	./gecode/int/idx-view.hh ./gecode/int/idx-view.hpp ./gecode/int/linear.hh \
+	./gecode/int/linear/bool-int.hpp ./gecode/int/linear/bool-scale.hpp ./gecode/int/linear/bool-view.hpp \
+	./gecode/int/linear/int-bin.hpp ./gecode/int/linear/int-dom.hpp ./gecode/int/linear/int-nary.hpp \
+	./gecode/int/linear/int-noview.hpp ./gecode/int/linear/int-ter.hpp ./gecode/int/linear/post.hpp \
+	./gecode/int/rel.hh ./gecode/int/rel/eq.hpp ./gecode/int/rel/lex.hpp \
+	./gecode/int/rel/lq-le.hpp ./gecode/int/rel/nq.hpp ./gecode/int/support-values.hh \
+	./gecode/int/support-values.hpp \
 	./gecode/float.hh ./gecode/float/array-traits.hpp ./gecode/float/array.hpp \
 	./gecode/float/branch.hpp ./gecode/float/branch/action.hpp ./gecode/float/branch/afc.hpp \
 	./gecode/float/branch/assign.hpp ./gecode/float/branch/chb.hpp ./gecode/float/branch/traits.hpp \

Makefile.in

@@ -352,7 +352,8 @@ INTHDR0 = \
 	idx-view.hh idx-view.hpp div.hh div.hpp \
 	exec.hh exec/when.hpp \
 	arithmetic/abs.hpp arithmetic/max.hpp arithmetic/argmax.hpp \
-	arithmetic/mult.hpp arithmetic/divmod.hpp \
+	arithmetic/mult.hpp arithmetic/gcd.hpp arithmetic/divides.hpp \
+	arithmetic/product.hpp arithmetic/product-mod.hpp arithmetic/divmod.hpp \
 	arithmetic/pow-ops.hpp arithmetic/pow.hpp arithmetic/nroot.hpp \
 	bool/or.hpp bool/eq.hpp bool/lq.hpp bool/eqv.hpp bool/base.hpp \
 	bool/clause.hpp bool/ite.hpp \

changelog.in

@@ -73,6 +73,19 @@ Date: unreleased
 [DESCRIPTION]
 This is the development changelog for the next Gecode release.
 
+[ENTRY]
+Module: int
+What:   new
+Rank:   major
+[DESCRIPTION]
+Add ordinary and reified gcd, n-ary product, and n-ary product_mod
+constraints, and reified divides. GCD uses nonnegative results and
+gcd(0,0)=0; zero divides zero. Modular products accept a fixed positive
+modulus or a variable modulus and use nonnegative Euclidean residues,
+including for negative products. All reification modes are supported.
+Propagation uses bounds and algebraic reasoning; the propagation-level
+argument does not select different consistency strengths.
+
 [RELEASE]
 Version: 6.4.0
 Date: 2026-07-15

docs/integer-number-theory.md

@@ -0,0 +1,96 @@
+# Integer number theory constraints
+
+These APIs require `<gecode/int.hh>`. They use bounds and algebraic reasoning;
+the `IntPropLevel` argument currently does not select different strengths.
+They do not promise bounds or domain consistency.
+
+Inside a `Space` constructor, this model has `g=6`, `p=-216`, and `r=1`:
+
+```cpp
+IntVar x(*this,-12,-12), y(*this,18,18);
+IntVar g(*this,0,18), p(*this,-300,300), r(*this,0,6);
+gcd(*this,x,y,g);
+product(*this,IntVarArgs({x,y}),p);
+product_mod(*this,IntVarArgs({x,y}),7,r);
+```
+
+Call `status()` on the space to run propagation. `product_mod` uses the
+Euclidean residue: `-216 = -31*7 + 1`. In contrast, Gecode's `mod` uses a
+dividend-signed remainder and would return `-6` for `-216 mod 7`.
+
+To require divisibility, pass a true reification variable:
+
+```cpp
+BoolVar yes(*this,1,1);
+IntVar divisor(*this,6,6), dividend(*this,-30,30);
+divides(*this,divisor,dividend,Reify(yes));
+```
+
+This relation means that some integer multiplier exists. Zero divides zero,
+but does not divide a nonzero value. GCD is always nonnegative, with
+`gcd(0,0)=0`. The exact product of an empty array is one; its modular product
+is `1 mod m`, which is zero when `m=1`.
+
+Every reified overload supports equivalence (`RM_EQV`), `b` implying the
+relation (`RM_IMP`), and the relation implying `b` (`RM_PMI`). For example,
+`product_mod(*this,factors,m,result,Reify(enabled,RM_IMP))` requires the
+modular relation only when `enabled=1`.
+
+A fixed integer modulus must lie in `1..Int::Limits::max`; an invalid constant
+throws `Int::OutOfLimits` even when an implication is inactive. With an
+`IntVar` modulus, positivity is part of the reified proposition. Consequently,
+an inactive implication does not constrain that modulus or the result.
+
+## Propagation and cost
+
+For a fixed positive modulus `m`, assigned factors are reduced to a coefficient
+`c`. Every result is a multiple of `gcd(c,m)`, even with several unassigned
+factors. A zero coefficient fixes the result to zero. Thus `6*x*z mod 12 = 1`
+fails without branching, and assigned factors 2 and 3 force a zero residue
+modulo 6. With one free factor and an assigned result, a linear congruence
+also restricts the factor bounds.
+
+A nonzero dividend bounds the magnitude of every possible divisor, including
+when the dividend is not assigned. Negating `divides(0,x)` removes zero from
+`x`. For GCD, an assigned nonzero operand bounds the result to its magnitude;
+a fixed quotient band can identify its only possible divisor. When both an
+operand and the GCD are assigned, endpoint probes check that the remaining
+quotient is coprime. For example, `gcd(6,x)=3` with `x=6..12` assigns `x=9`.
+The probes inspect at most 64 arithmetic candidates per endpoint and retain
+the original bound if that budget is exhausted. They use the interval hull,
+so interior holes do not change a bounds-subscribed actor's fixpoint.
+
+Exact-product posting sorts equal views together. The grouping survives
+cloning, and subsequent propagation groups adjacent occurrences in linear
+time. Assigned units are compacted in place while preserving that order.
+Fixed- and variable-modulus products use prefix/suffix intervals to
+compute all cofactors in linear time per filtering pass, with linear temporary
+storage. The temporary intervals are rebuilt after bounds change. Repeated
+factors in exact products additionally require integer-root bounds; their
+arithmetic work is at most proportional to the factor count times the number
+of bits in the integer limit. Local closure can require several passes,
+especially across sparse domain endpoints.
+
+Modular interval reasoning uses exact representable endpoints. If an endpoint
+overflows, that interval deduction is skipped; saturation is not valid for
+modular arithmetic. Assigned modular products remain safe because each
+multiplication is reduced before the next factor. Cheap coefficient and
+zero checks precede allocation and cofactor filtering. Fixed-modulus actors
+fold assigned occurrences into a persistent residue coefficient and remove
+them from the active view array. They also retain the exact coefficient while
+it fits in the integer limits, for interval reasoning; an unavailable exact
+coefficient never replaces the modular one. Later scans and clones visit only
+the remaining occurrences. Variable-modulus actors remove assigned ones, but
+retain other constants until the modulus is fixed. Both forms exclude zero
+endpoints from factors when the result is strictly positive, including factors
+with negative domains.
+
+These are deliberately incomplete rules. They do not enumerate all divisors
+or all supported residues. Undecided or negated reified constraints generally
+perform less filtering than asserted relations. The variable-modulus interval
+stage handles nonnegative factors in a single quotient band; fixing the
+modulus enables the fixed-modulus rules. Bounds subscriptions can miss
+opportunities caused solely by interior domain removal in the propagators
+that declare weak monotonicity. Fully assigned tuples are still checked
+exactly. Faster propagation passes alone do not establish faster solving;
+compare search and end-to-end time on representative models.

gecode/int.hh

@@ -3031,6 +3031,118 @@ namespace Gecode {
   mult(Home home, IntVar x0, IntVar x1, IntVar x2,
        IntPropLevel ipl=IPL_DEF);
 
+  /** \brief Post propagator for \f$\gcd(x_0,x_1)=x_2\f$
+   *
+   * The greatest common divisor is nonnegative, with
+   * \f$\gcd(0,0)=0\f$. Negative operands are interpreted by absolute
+   * value. Uses sound bounds and algebraic propagation; bounds consistency
+   * is not guaranteed. The propagation level \a ipl is currently ignored.
+   */
+  GECODE_INT_EXPORT void
+  gcd(Home home, IntVar x0, IntVar x1, IntVar x2,
+      IntPropLevel ipl=IPL_DEF);
+
+  /** \brief Post propagator for
+   * \f$(\gcd(x_0,x_1)=x_2)\leftrightarrow r\f$
+   *
+   * Supports all reification modes. The greatest common divisor is
+   * nonnegative, with \f$\gcd(0,0)=0\f$. Uses conservative algebraic
+   * entailment and disentailment tests. The propagation level \a ipl is
+   * currently ignored.
+   */
+  GECODE_INT_EXPORT void
+  gcd(Home home, IntVar x0, IntVar x1, IntVar x2, Reify r,
+      IntPropLevel ipl=IPL_DEF);
+
+  /** \brief Reify whether \a divisor divides \a dividend
+   *
+   * Divisibility means that an integer \f$k\f$ exists such that
+   * \f$dividend=divisor\cdot k\f$. Consequently, zero divides zero, but
+   * zero does not divide a nonzero integer. Supports all reification modes.
+   * Uses bounds and conservative algebraic propagation. The propagation
+   * level \a ipl is currently ignored.
+   */
+  GECODE_INT_EXPORT void
+  divides(Home home, IntVar divisor, IntVar dividend, Reify r,
+          IntPropLevel ipl=IPL_DEF);
+
+  /** \brief Constrain \a y to the exact product of the variables in \a x
+   *
+   * The product of an empty array is one.
+   * Uses bounds and algebraic propagation, without guaranteeing bounds
+   * consistency. The propagation level \a ipl is currently ignored.
+   * \ingroup TaskModelInt
+   */
+  GECODE_INT_EXPORT void
+  product(Home home, const IntVarArgs& x, IntVar y,
+          IntPropLevel ipl=IPL_DEF);
+
+  /** \brief Reify whether \a y is the exact product of the variables in \a x
+   *
+   * The product of an empty array is one.
+   * Supports all reification modes using conservative algebraic tests.
+   * The propagation level \a ipl is currently ignored.
+   * \ingroup TaskModelInt
+   */
+  GECODE_INT_EXPORT void
+  product(Home home, const IntVarArgs& x, IntVar y, Reify r,
+          IntPropLevel ipl=IPL_DEF);
+
+  /** \brief Constrain \a y to the product of \a x modulo \a m
+   *
+   * The modulus \a m must be positive. The result uses the canonical
+   * Euclidean residue in the range zero through \a m minus one. The product
+   * of an empty array is one.
+   * Unlike mod(), a negative product still has a nonnegative residue.
+   * Uses bounds and algebraic propagation; \a ipl is currently ignored.
+   * Throws Int::OutOfLimits if \a m is nonpositive or exceeds Int::Limits::max.
+   * \ingroup TaskModelInt
+   */
+  GECODE_INT_EXPORT void
+  product_mod(Home home, const IntVarArgs& x, int m, IntVar y,
+              IntPropLevel ipl=IPL_DEF);
+
+  /** \brief Reify whether \a y is the product of \a x modulo \a m
+   *
+   * The modulus \a m must be positive. The result uses the canonical
+   * Euclidean residue in the range zero through \a m minus one. The product
+   * of an empty array is one.
+   * Supports all reification modes using conservative algebraic tests;
+   * \a ipl is currently ignored.
+   * Throws Int::OutOfLimits if \a m is nonpositive or exceeds Int::Limits::max,
+   * even for an inactive implication.
+   * \ingroup TaskModelInt
+   */
+  GECODE_INT_EXPORT void
+  product_mod(Home home, const IntVarArgs& x, int m, IntVar y, Reify r,
+              IntPropLevel ipl=IPL_DEF);
+
+  /** \brief Constrain \a y to the product of \a x modulo \a m
+   *
+   * The variable modulus \a m is constrained to be positive and \a y uses
+   * the canonical Euclidean residue, so that \f$0\leq y<m\f$. The product
+   * of an empty array is one.
+   * Uses bounds and algebraic propagation; \a ipl is currently ignored.
+   * \ingroup TaskModelInt
+   */
+  GECODE_INT_EXPORT void
+  product_mod(Home home, const IntVarArgs& x, IntVar m, IntVar y,
+              IntPropLevel ipl=IPL_DEF);
+
+  /** \brief Reify whether \a y is the product of \a x modulo \a m
+   *
+   * The reified proposition includes \f$m>0\f$, the canonical range
+   * \f$0\leq y<m\f$, and congruence with the product. The product of an
+   * empty array is one.
+   * Supports all reification modes using conservative algebraic tests;
+   * \a ipl is currently ignored. An inactive implication does not constrain
+   * the modulus or result.
+   * \ingroup TaskModelInt
+   */
+  GECODE_INT_EXPORT void
+  product_mod(Home home, const IntVarArgs& x, IntVar m, IntVar y, Reify r,
+              IntPropLevel ipl=IPL_DEF);
+
   /** \brief Post propagator for \f$x_0\ \mathrm{div}\ x_1=x_2 \land x_0\ \mathrm{mod}\ x_1 = x_3\f$
    *
    * Supports bounds consistency (\a ipl = IPL_BND, default).