diff --git a/Makefile.in b/Makefile.in index 8e5d2c625d..aa182f5cde 100755 --- a/Makefile.in +++ b/Makefile.in @@ -1157,6 +1157,7 @@ FLATZINCTESTSRC0 = \ test/flatzinc/bugfix_r7854.cpp \ test/flatzinc/empty_domain_1.cpp \ test/flatzinc/empty_domain_2.cpp \ + test/flatzinc/native-registry.cpp \ test/flatzinc/int_set_as_type1.cpp \ test/flatzinc/int_set_as_type2.cpp \ test/flatzinc/issue166.cpp \ diff --git a/changelog.in b/changelog.in index 394b936a5d..2f7c886add 100755 --- a/changelog.in +++ b/changelog.in @@ -73,6 +73,27 @@ Date: unreleased [DESCRIPTION] This is the development changelog for the next Gecode release. +[ENTRY] +Module: flatzinc +What: new +Rank: major +[DESCRIPTION] +Use standard MiniZinc FlatZinc hooks for native conditionals, count inequalities, +nondeterministic regular, and optional distinctness and scheduling. Expose +additional arithmetic, distance, rectangle, and set constraints through +documented modelling predicates with typed FlatZinc bindings. Add annotations +for basic, advanced, and combined propagation algorithms, and minimum-distance +actor organization. + +[ENTRY] +Module: float +What: bug +Rank: minor +[DESCRIPTION] +Keep exact fixed-base power and logarithm solutions using explicitly rounded +MPFR bounds, handle base-one powers, and remove an invalid shared-variable +shortcut. + [ENTRY] Module: int diff --git a/cmake/GecodeSources.cmake b/cmake/GecodeSources.cmake index 58a415eb36..e762f19034 100644 --- a/cmake/GecodeSources.cmake +++ b/cmake/GecodeSources.cmake @@ -316,6 +316,7 @@ set(GECODE_TEST_SOURCES test/flatzinc/eq20.cpp test/flatzinc/factory_planning_instance.cpp test/flatzinc/golomb.cpp + test/flatzinc/native-registry.cpp test/flatzinc/int_set_as_type1.cpp test/flatzinc/int_set_as_type2.cpp test/flatzinc/issue166.cpp diff --git a/gecode/flatzinc/flatzinc.cpp b/gecode/flatzinc/flatzinc.cpp index e35bd3638c..c378bcf0e9 100644 --- a/gecode/flatzinc/flatzinc.cpp +++ b/gecode/flatzinc/flatzinc.cpp @@ -2647,19 +2647,28 @@ namespace Gecode { namespace FlatZinc { #endif IntPropLevel FlatZincSpace::ann2ipl(AST::Node* ann) { + int ipl = IPL_DEF; if (ann) { if (ann->hasAtom("val") || ann->hasAtom("value_propagation")) - return IPL_VAL; - if (ann->hasAtom("domain") || ann->hasAtom("domain_propagation")) - return IPL_DOM; - if (ann->hasAtom("bounds") || - ann->hasAtom("bounds_propagation") || - ann->hasAtom("boundsR") || - ann->hasAtom("boundsD") || - ann->hasAtom("boundsZ")) - return IPL_BND; - } - return IPL_DEF; + ipl = IPL_VAL; + else if (ann->hasAtom("domain") || ann->hasAtom("domain_propagation")) + ipl = IPL_DOM; + else if (ann->hasAtom("bounds") || + ann->hasAtom("bounds_propagation") || + ann->hasAtom("boundsR") || + ann->hasAtom("boundsD") || + ann->hasAtom("boundsZ")) + ipl = IPL_BND; + if (ann->hasAtom("gecode_full_propagation")) + ipl |= IPL_FULL; + else { + if (ann->hasAtom("gecode_basic_propagation")) + ipl |= IPL_BASIC; + if (ann->hasAtom("gecode_advanced_propagation")) + ipl |= IPL_ADVANCED; + } + } + return static_cast(ipl); } DFA diff --git a/gecode/flatzinc/mznlib/fzn_all_different_int_opt.mzn b/gecode/flatzinc/mznlib/fzn_all_different_int_opt.mzn new file mode 100644 index 0000000000..54e55b7284 --- /dev/null +++ b/gecode/flatzinc/mznlib/fzn_all_different_int_opt.mzn @@ -0,0 +1,62 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +predicate gecode_all_different_optional( + array[int] of var int: x, + array[int] of var bool: present, +); + +predicate fzn_all_different_int_opt(array[int] of var opt int: xs) = + if length(xs) = 0 then + true + else + % Fixed absent values have no deopt value; their integer is ignored. + gecode_all_different_optional( + [if is_fixed(x) /\ absent(fix(x)) then 0 else deopt(x) endif | x in xs], + [occurs(x) | x in xs], + ) + endif; + +% Reification has no native optional-distinct propagator. +predicate fzn_all_different_int_opt_reif( + array[int] of var opt int: xs, + var bool: b, +) = + let { + array[index_set(xs)] of var int: values = array1d( + index_set(xs), + [if is_fixed(x) /\ absent(fix(x)) then 0 else deopt(x) endif | x in xs], + ); + } in + b <-> forall (i, j in index_set(xs) where i < j) ( + (occurs(xs[i]) /\ occurs(xs[j])) -> values[i] != values[j] + ); diff --git a/gecode/flatzinc/mznlib/fzn_all_equal_int_reif.mzn b/gecode/flatzinc/mznlib/fzn_all_equal_int_reif.mzn new file mode 100644 index 0000000000..714301f48b --- /dev/null +++ b/gecode/flatzinc/mznlib/fzn_all_equal_int_reif.mzn @@ -0,0 +1,46 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +predicate gecode_not_all_equal_int(array[int] of var int: xs); + +predicate fzn_all_equal_int_reif(array[int] of var int: xs, var bool: b) = + if is_fixed(b) /\ not fix(b) then + gecode_not_all_equal_int(xs) + else + b <-> (if length(xs) = 0 then + true + else + forall (i in index_set(xs)) ( + xs[i] = xs[min(index_set(xs))] + ) + endif) + endif; diff --git a/gecode/flatzinc/mznlib/fzn_alldifferent_except.mzn b/gecode/flatzinc/mznlib/fzn_alldifferent_except.mzn new file mode 100644 index 0000000000..9f66256810 --- /dev/null +++ b/gecode/flatzinc/mznlib/fzn_alldifferent_except.mzn @@ -0,0 +1,59 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +include "global_cardinality_low_up.mzn"; +include "fzn_all_different_int.mzn"; + +predicate gecode_all_different_except(array[int] of var int: x, int: except_value); + +predicate fzn_alldifferent_except(array[int] of var int: xs, set of int: except) = + if length(xs) = 0 then + true + elseif card(except) = 1 then + if min(except) < lb_array(xs) \/ min(except) > ub_array(xs) then + % Drop irrelevant exceptions before FlatZinc checks integer limits. + fzn_all_different_int(xs) + else + gecode_all_different_except(xs, min(except)) + endif + elseif forall (i in index_set(xs)) (has_bounds(xs[i])) then + % Native distinct supports one exception; retain the standard translation + % for larger exception sets. + let { + set of int: values = dom_array(xs) diff except; + } in + global_cardinality(xs, set2array(values), [0 | i in values], [1 | i in values]) + else + forall (i, j in index_set(xs) where i < j) ( + (xs[i] in except /\ xs[j] in except) \/ xs[i] != xs[j] + ) + endif; diff --git a/gecode/flatzinc/mznlib/fzn_alldifferent_except_0.mzn b/gecode/flatzinc/mznlib/fzn_alldifferent_except_0.mzn index 967f001da9..dede4ad0d0 100644 --- a/gecode/flatzinc/mznlib/fzn_alldifferent_except_0.mzn +++ b/gecode/flatzinc/mznlib/fzn_alldifferent_except_0.mzn @@ -1,24 +1,39 @@ -include "global_cardinality_low_up_closed.mzn"; +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% -/** @group globals.alldifferent +include "fzn_alldifferent_except.mzn"; + +/** @group globals.alldifferent Constrain the array of integers \a vs to be all different except those elements that are assigned the value 0. */ -predicate fzn_alldifferent_except_0(array[int] of var int: vs) = - if length(vs)==0 then true - else - let { - int: l = lb_array(vs); - int: u = ub_array(vs); - } in - if l != -infinity /\ u != infinity then - global_cardinality_low_up_closed(vs, [i | i in l..u], - [0 | i in l..u], - [if i==0 then length(vs) else 1 endif | i in l..u] - ) - else - forall(i, j in index_set(vs) where i < j) ( - (vs[i] != 0 /\ vs[j] != 0) -> vs[i] != vs[j] - ) - endif - endif; +predicate fzn_alldifferent_except_0(array[int] of var int: vs) = fzn_alldifferent_except(vs, {0}); diff --git a/gecode/flatzinc/mznlib/fzn_array_set_intersect.mzn b/gecode/flatzinc/mznlib/fzn_array_set_intersect.mzn new file mode 100644 index 0000000000..441c0b52cd --- /dev/null +++ b/gecode/flatzinc/mznlib/fzn_array_set_intersect.mzn @@ -0,0 +1,47 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +predicate gecode_array_set_intersect( + array[int] of var set of int: x, + var set of int: y, +); + +% The intersection of an empty array is undefined in the standard library. +predicate fzn_array_set_intersect( + array[int] of var set of int: x, + var set of int: y, +) = + if length(x) = 0 then + false + else + gecode_array_set_intersect(x, y) + endif; diff --git a/gecode/flatzinc/mznlib/fzn_count_geq.mzn b/gecode/flatzinc/mznlib/fzn_count_geq.mzn new file mode 100644 index 0000000000..bc0c00f492 --- /dev/null +++ b/gecode/flatzinc/mznlib/fzn_count_geq.mzn @@ -0,0 +1,41 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +predicate gecode_count_int_fzn( + array[int] of var int: x, + var int: value, + int: relation, + var int: n, +); + +% Requires n >= the number of occurrences of value in xs. +predicate fzn_count_geq(array[int] of var int: xs, var int: value, var int: n) = gecode_count_int_fzn(xs, value, 3, n); diff --git a/gecode/flatzinc/mznlib/fzn_count_gt.mzn b/gecode/flatzinc/mznlib/fzn_count_gt.mzn new file mode 100644 index 0000000000..8cda47ffbb --- /dev/null +++ b/gecode/flatzinc/mznlib/fzn_count_gt.mzn @@ -0,0 +1,41 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +predicate gecode_count_int_fzn( + array[int] of var int: x, + var int: value, + int: relation, + var int: n, +); + +% Requires n > the number of occurrences of value in xs. +predicate fzn_count_gt(array[int] of var int: xs, var int: value, var int: n) = gecode_count_int_fzn(xs, value, 4, n); diff --git a/gecode/flatzinc/mznlib/fzn_count_leq.mzn b/gecode/flatzinc/mznlib/fzn_count_leq.mzn new file mode 100644 index 0000000000..6ffb4b953c --- /dev/null +++ b/gecode/flatzinc/mznlib/fzn_count_leq.mzn @@ -0,0 +1,41 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +predicate gecode_count_int_fzn( + array[int] of var int: x, + var int: value, + int: relation, + var int: n, +); + +% Requires n <= the number of occurrences of value in xs. +predicate fzn_count_leq(array[int] of var int: xs, var int: value, var int: n) = gecode_count_int_fzn(xs, value, 5, n); diff --git a/gecode/flatzinc/mznlib/fzn_count_lt.mzn b/gecode/flatzinc/mznlib/fzn_count_lt.mzn new file mode 100644 index 0000000000..6c82182929 --- /dev/null +++ b/gecode/flatzinc/mznlib/fzn_count_lt.mzn @@ -0,0 +1,41 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +predicate gecode_count_int_fzn( + array[int] of var int: x, + var int: value, + int: relation, + var int: n, +); + +% Requires n < the number of occurrences of value in xs. +predicate fzn_count_lt(array[int] of var int: xs, var int: value, var int: n) = gecode_count_int_fzn(xs, value, 6, n); diff --git a/gecode/flatzinc/mznlib/fzn_cumulative_opt.mzn b/gecode/flatzinc/mznlib/fzn_cumulative_opt.mzn index ecea229ea5..43097f37f4 100644 --- a/gecode/flatzinc/mznlib/fzn_cumulative_opt.mzn +++ b/gecode/flatzinc/mznlib/fzn_cumulative_opt.mzn @@ -34,25 +34,56 @@ include "fzn_cumulative_opt_decomp.mzn"; -predicate gecode_schedule_cumulative_optional(array[int] of var int: start, - array[int] of int: duration, array[int] of int: usage, - array[int] of var bool: m, int: capacity); +predicate gecode_schedule_cumulative_optional( + array[int] of var int: start, + array[int] of int: duration, + array[int] of int: usage, + array[int] of var bool: m, + var int: capacity, +); -predicate fzn_cumulative_opt(array[int] of var opt int: s, - array[int] of var int: d, - array[int] of var int: r, var int: b) = - if - forall (i in index_set(d)) (is_fixed(d[i])) /\ - forall (i in index_set(r)) (is_fixed(r[i])) /\ - is_fixed(b) - then - gecode_schedule_cumulative_optional( - [ if is_fixed(si) /\ absent(fix(si)) then 0 else deopt(si) endif | si in s ], - [ fix(di) | di in d ], - [ fix(ri) | ri in r ], - [ occurs(si) | si in s ], - fix(b) - ) - else - fzn_cumulative_opt_decomp(s,d,r,b) - endif; +predicate gecode_cumulative_flex_optional( + array[int] of var int: start, + array[int] of var int: duration, + array[int] of var int: end, + array[int] of int: usage, + var int: capacity, + array[int] of var bool: present, +); + +predicate fzn_cumulative_opt( + array[int] of var opt int: s, + array[int] of var int: d, + array[int] of var int: r, + var int: b, +) = + if ub(b) < 0 then + false + elseif forall (i in index_set(d)) (is_fixed(d[i])) /\ forall (i in index_set(r)) (is_fixed(r[i])) then + % Zero-duration tasks consume no capacity in MiniZinc. + gecode_schedule_cumulative_optional( + [if is_fixed(si) /\ absent(fix(si)) then 0 else deopt(si) endif | si in s], + [fix(di) | di in d], + [fix(ri) | ri in r], + [occurs(s[i]) /\ fix(d[i]) > 0 | i in index_set(s)], + b, + ) + elseif forall (i in index_set(r)) (is_fixed(r[i])) then + let { + array[int] of var int: start = [if is_fixed(si) /\ absent(fix(si)) then 0 else deopt(si) endif | si in s]; + array[int] of var int: duration = array1d(d); + % Zero-duration tasks consume no capacity in MiniZinc. + array[int] of var bool: present = [occurs(array1d(s)[i]) /\ duration[i] > 0 | i in index_set(duration)]; + array[int] of var int: end = [if present[i] then start[i] + duration[i] else 0 endif | i in index_set(start)]; + } in + gecode_cumulative_flex_optional( + start, + duration, + end, + [fix(ri) | ri in r], + b, + present, + ) + else + fzn_cumulative_opt_decomp(s, d, r, b) + endif; diff --git a/gecode/flatzinc/mznlib/fzn_diffn.mzn b/gecode/flatzinc/mznlib/fzn_diffn.mzn index 070402e9ef..3c1abcc248 100644 --- a/gecode/flatzinc/mznlib/fzn_diffn.mzn +++ b/gecode/flatzinc/mznlib/fzn_diffn.mzn @@ -30,11 +30,16 @@ % % -predicate gecode_nooverlap(array[int] of var int: x, array[int] of var int: w, - array[int] of var int: y, array[int] of var int: h); +predicate gecode_nooverlap_fzn( + array[int] of var int: x, + array[int] of var int: w, + array[int] of var int: y, + array[int] of var int: h, +); -predicate fzn_diffn(array[int] of var int: x, - array[int] of var int: y, - array[int] of var int: dx, - array[int] of var int: dy) = - gecode_nooverlap(x,dx,y,dy); +predicate fzn_diffn( + array[int] of var int: x, + array[int] of var int: y, + array[int] of var int: dx, + array[int] of var int: dy, +) = gecode_nooverlap_fzn(x, dx, y, dy); diff --git a/gecode/flatzinc/mznlib/fzn_disjunctive_strict_opt.mzn b/gecode/flatzinc/mznlib/fzn_disjunctive_strict_opt.mzn index d3aa941c90..d877409249 100644 --- a/gecode/flatzinc/mznlib/fzn_disjunctive_strict_opt.mzn +++ b/gecode/flatzinc/mznlib/fzn_disjunctive_strict_opt.mzn @@ -32,18 +32,38 @@ % % -predicate gecode_schedule_unary_optional(array[int] of var int: x, - array[int] of int: p, array[int] of var bool: m); +predicate gecode_schedule_unary_optional( + array[int] of var int: x, + array[int] of int: p, + array[int] of var bool: m, +); -include "fzn_disjunctive_strict_opt_decomp.mzn"; +predicate gecode_unary_flex_optional( + array[int] of var int: start, + array[int] of var int: duration, + array[int] of var int: end, + array[int] of var bool: present, +); -predicate fzn_disjunctive_strict_opt(array[int] of var opt int: s, - array[int] of var int: d) = - forall (i in index_set(d)) (d[i] >= 0) /\ - if forall (i in index_set(d)) (is_fixed(d[i])) then - gecode_schedule_unary_optional( - [ if is_fixed(si) /\ absent(fix(si)) then 0 else deopt(si) endif | si in s], - [ fix(di) | di in d], - [ occurs(si) | si in s ] - ) - else fzn_disjunctive_strict_opt_decomp(s,d) endif; +predicate fzn_disjunctive_strict_opt( + array[int] of var opt int: s, + array[int] of var int: d, +) = + forall (i in index_set(d)) ( + d[i] >= 0 + ) /\ + if forall (i in index_set(d)) (is_fixed(d[i])) then + gecode_schedule_unary_optional( + [if is_fixed(si) /\ absent(fix(si)) then 0 else deopt(si) endif | si in s], + [fix(di) | di in d], + [occurs(si) | si in s], + ) + else + let { + array[int] of var int: start = [if is_fixed(si) /\ absent(fix(si)) then 0 else deopt(si) endif | si in s]; + array[int] of var bool: present = [occurs(si) | si in s]; + array[int] of var int: duration = array1d(d); + array[int] of var int: end = [if present[i] then start[i] + duration[i] else 0 endif | i in index_set(start)]; + } in + gecode_unary_flex_optional(start, duration, end, present) + endif; diff --git a/gecode/flatzinc/mznlib/fzn_if_then_else_bool.mzn b/gecode/flatzinc/mznlib/fzn_if_then_else_bool.mzn new file mode 100644 index 0000000000..27d3860c91 --- /dev/null +++ b/gecode/flatzinc/mznlib/fzn_if_then_else_bool.mzn @@ -0,0 +1,40 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +include "fzn_if_then_else_var_bool.mzn"; + +predicate fzn_if_then_else_bool( + array [int] of var bool: c, + array [int] of bool: x, + var bool: y, +) = + fzn_if_then_else_var_bool(c, x, y); diff --git a/gecode/flatzinc/mznlib/fzn_if_then_else_float.mzn b/gecode/flatzinc/mznlib/fzn_if_then_else_float.mzn new file mode 100644 index 0000000000..275da6bbc8 --- /dev/null +++ b/gecode/flatzinc/mznlib/fzn_if_then_else_float.mzn @@ -0,0 +1,40 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +include "fzn_if_then_else_var_float.mzn"; + +predicate fzn_if_then_else_float( + array [int] of var bool: c, + array [int] of float: x, + var float: y, +) = + fzn_if_then_else_var_float(c, x, y); diff --git a/gecode/flatzinc/mznlib/fzn_if_then_else_int.mzn b/gecode/flatzinc/mznlib/fzn_if_then_else_int.mzn new file mode 100644 index 0000000000..32c94a26b6 --- /dev/null +++ b/gecode/flatzinc/mznlib/fzn_if_then_else_int.mzn @@ -0,0 +1,40 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +include "fzn_if_then_else_var_int.mzn"; + +predicate fzn_if_then_else_int( + array [int] of var bool: c, + array [int] of int: x, + var int: y, +) = + fzn_if_then_else_var_int(c, x, y); diff --git a/gecode/flatzinc/mznlib/fzn_if_then_else_set.mzn b/gecode/flatzinc/mznlib/fzn_if_then_else_set.mzn new file mode 100644 index 0000000000..2422d8ec6a --- /dev/null +++ b/gecode/flatzinc/mznlib/fzn_if_then_else_set.mzn @@ -0,0 +1,40 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +include "fzn_if_then_else_var_set.mzn"; + +predicate fzn_if_then_else_set( + array [int] of var bool: c, + array [int] of set of int: x, + var set of int: y, +) = + fzn_if_then_else_var_set(c, x, y); diff --git a/gecode/flatzinc/mznlib/fzn_if_then_else_var_bool.mzn b/gecode/flatzinc/mznlib/fzn_if_then_else_var_bool.mzn new file mode 100644 index 0000000000..814606b32b --- /dev/null +++ b/gecode/flatzinc/mznlib/fzn_if_then_else_var_bool.mzn @@ -0,0 +1,68 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +predicate gecode_bool_ite( + var bool: b, + var bool: x, + var bool: y, + var bool: z, +); + +% A two-branch conditional ends with a fixed true condition for else. +predicate fzn_if_then_else_var_bool( + array [int] of var bool: c, + array [int] of var bool: x, + var bool: y, +) = + if length(c) = 2 /\ + index_sets_agree(c, x) /\ + (if is_fixed(c[max(index_set(c))]) then + fix(c[max(index_set(c))]) + else + false + endif) then + gecode_bool_ite(c[min(index_set(c))], x[min(index_set(c))], x[max(index_set(c))], y) + else + let { + array [index_set(c)] of var bool: d; + } in + forall (i in index_set(c)) ( + if i > min(index_set(c)) then + d[i] = (not c[i - 1] /\ d[i - 1]) + else + d[i] = true + endif + ) /\ + forall (i in index_set(c)) ( + c[i] /\ d[i] -> y = x[i] + ) + endif; diff --git a/gecode/flatzinc/mznlib/fzn_if_then_else_var_float.mzn b/gecode/flatzinc/mznlib/fzn_if_then_else_var_float.mzn new file mode 100644 index 0000000000..e16f978fad --- /dev/null +++ b/gecode/flatzinc/mznlib/fzn_if_then_else_var_float.mzn @@ -0,0 +1,68 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +predicate gecode_float_ite( + var bool: b, + var float: x, + var float: y, + var float: z, +); + +% A two-branch conditional ends with a fixed true condition for else. +predicate fzn_if_then_else_var_float( + array [int] of var bool: c, + array [int] of var float: x, + var float: y, +) = + if length(c) = 2 /\ + index_sets_agree(c, x) /\ + (if is_fixed(c[max(index_set(c))]) then + fix(c[max(index_set(c))]) + else + false + endif) then + gecode_float_ite(c[min(index_set(c))], x[min(index_set(c))], x[max(index_set(c))], y) + else + let { + array [index_set(c)] of var bool: d; + } in + forall (i in index_set(c)) ( + if i > min(index_set(c)) then + d[i] = (not c[i - 1] /\ d[i - 1]) + else + d[i] = true + endif + ) /\ + forall (i in index_set(c)) ( + c[i] /\ d[i] -> y = x[i] + ) + endif; diff --git a/gecode/flatzinc/mznlib/fzn_if_then_else_var_int.mzn b/gecode/flatzinc/mznlib/fzn_if_then_else_var_int.mzn new file mode 100644 index 0000000000..d9bd87334e --- /dev/null +++ b/gecode/flatzinc/mznlib/fzn_if_then_else_var_int.mzn @@ -0,0 +1,68 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +predicate gecode_int_ite( + var bool: b, + var int: x, + var int: y, + var int: z, +); + +% A two-branch conditional ends with a fixed true condition for else. +predicate fzn_if_then_else_var_int( + array [int] of var bool: c, + array [int] of var int: x, + var int: y, +) = + if length(c) = 2 /\ + index_sets_agree(c, x) /\ + (if is_fixed(c[max(index_set(c))]) then + fix(c[max(index_set(c))]) + else + false + endif) then + gecode_int_ite(c[min(index_set(c))], x[min(index_set(c))], x[max(index_set(c))], y) + else + let { + array [index_set(c)] of var bool: d; + } in + forall (i in index_set(c)) ( + if i > min(index_set(c)) then + d[i] = (not c[i - 1] /\ d[i - 1]) + else + d[i] = true + endif + ) /\ + forall (i in index_set(c)) ( + c[i] /\ d[i] -> y = x[i] + ) + endif; diff --git a/gecode/flatzinc/mznlib/fzn_if_then_else_var_set.mzn b/gecode/flatzinc/mznlib/fzn_if_then_else_var_set.mzn new file mode 100644 index 0000000000..bfb2d0d85a --- /dev/null +++ b/gecode/flatzinc/mznlib/fzn_if_then_else_var_set.mzn @@ -0,0 +1,68 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +predicate gecode_set_ite( + var bool: b, + var set of int: x, + var set of int: y, + var set of int: z, +); + +% A two-branch conditional ends with a fixed true condition for else. +predicate fzn_if_then_else_var_set( + array [int] of var bool: c, + array [int] of var set of int: x, + var set of int: y, +) = + if length(c) = 2 /\ + index_sets_agree(c, x) /\ + (if is_fixed(c[max(index_set(c))]) then + fix(c[max(index_set(c))]) + else + false + endif) then + gecode_set_ite(c[min(index_set(c))], x[min(index_set(c))], x[max(index_set(c))], y) + else + let { + array [index_set(c)] of var bool: d; + } in + forall (i in index_set(c)) ( + if i > min(index_set(c)) then + d[i] = (not c[i - 1] /\ d[i - 1]) + else + d[i] = true + endif + ) /\ + forall (i in index_set(c)) ( + c[i] /\ d[i] -> y = x[i] + ) + endif; diff --git a/gecode/flatzinc/mznlib/fzn_regular_nfa.mzn b/gecode/flatzinc/mznlib/fzn_regular_nfa.mzn new file mode 100644 index 0000000000..3da70bb2e9 --- /dev/null +++ b/gecode/flatzinc/mznlib/fzn_regular_nfa.mzn @@ -0,0 +1,55 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +predicate gecode_regular_nfa_int_fzn( + array[int] of var int: x, + int: q, + int: first_symbol, + int: symbols, + array[int] of set of int: transitions, + int: initial, + set of int: final, +); + +predicate fzn_regular_nfa( + array[int] of var int: xs, + int: Q, + int: S, + array[int, int] of set of int: d, + int: q0, + set of int: F, +) = + if length(xs) = 0 then + q0 in F + else + gecode_regular_nfa_int_fzn(xs, Q, 1, S, array1d(d), q0, F) + endif; diff --git a/gecode/flatzinc/mznlib/fzn_regular_nfa_set.mzn b/gecode/flatzinc/mznlib/fzn_regular_nfa_set.mzn new file mode 100644 index 0000000000..ef192e2ae7 --- /dev/null +++ b/gecode/flatzinc/mznlib/fzn_regular_nfa_set.mzn @@ -0,0 +1,63 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +predicate gecode_regular_nfa_int_fzn( + array[int] of var int: x, + int: q, + int: first_symbol, + int: symbols, + array[int] of set of int: transitions, + int: initial, + set of int: final, +); + +predicate fzn_regular_nfa( + array[int] of var int: xs, + int: Q, + set of int: S, + array[int, int] of set of int: d, + int: q0, + set of int: F, +) = + if length(xs) = 0 then + q0 in F + else + gecode_regular_nfa_int_fzn( + xs, + Q, + min(S), + card(S), + array1d(d), + q0, + F, + ) + endif; diff --git a/gecode/flatzinc/mznlib/gecode.mzn b/gecode/flatzinc/mznlib/gecode.mzn index ca4b5190de..c3d598148e 100644 --- a/gecode/flatzinc/mznlib/gecode.mzn +++ b/gecode/flatzinc/mznlib/gecode.mzn @@ -38,7 +38,7 @@ */ /*** - @groupdef gecode.annotations Additional Gecode search annotations + @groupdef gecode.annotations Additional Gecode annotations */ /** @group gecode.annotations Select variable with smallest accumulated failure count */ @@ -60,6 +60,21 @@ annotation action_size_max; /** @group gecode.annotations Select random variable */ annotation random; +/** @group gecode.annotations Use the basic algorithm where supported. */ +annotation gecode_basic_propagation; +/** @group gecode.annotations Use the advanced algorithm where supported. */ +annotation gecode_advanced_propagation; +/** @group gecode.annotations Use both basic and advanced algorithms where supported. + These may be combined with domain_propagation or bounds_propagation; + constraints without algorithm choices ignore them. */ +annotation gecode_full_propagation; +/** @group gecode.annotations + Use a separate propagator for each pair in minimum-distance constraints. + The default is a single propagator. The basic, advanced, and full propagation + annotations select the algorithm in either case. +*/ +annotation gecode_decomposed_propagation; + annotation int_assign(array[int] of var int: x, ann:a); /** @group gecode.annotations Specify default search strategy for integer variables to use variable selection @@ -163,4 +178,432 @@ predicate gecode_schedule_unary_optional(array[int] of var int: x, predicate gecode_schedule_cumulative_optional(array[int] of var int: start, array[int] of int: duration, array[int] of int: usage, - array[int] of var bool: m, int: capacity); + array[int] of var bool: m, var int: capacity); + + +include "all_different.mzn"; +include "gecode_fzn.mzn"; + +/** @group gecode.constraints + Requires every pair of values in \a x to differ by at least \a distance. + The distance must be nonnegative, including for empty and singleton arrays. +*/ +predicate gecode_inter_distance(array[$$X] of var int: x, var int: distance) = + if mzn_in_root_context() then + gecode_inter_distance_fzn(array1d(x), distance) + else + distance >= 0 /\ + forall (i, j in index_set(x) where i < j) ( + abs(x[i] - x[j]) >= distance + ) + endif; + +/** @group gecode.constraints + Requires the sums \a x[i] + \a offset[i] to be pairwise distinct. + The arrays must have identical index sets. + The offsets do not require additional variables for the sums. +*/ +predicate gecode_all_different_offset( + array[$$X] of int: offset, + array[$$X] of var int: x, +) = + assert( + index_set(offset) = index_set(x), + "gecode_all_different_offset: index set mismatch", + if mzn_in_root_context() then + gecode_all_different_offset_fzn(array1d(offset), array1d(x)) + else + all_different([x[i] + offset[i] | i in index_set(x)]) + endif, + ); + +/** @group gecode.constraints + Constrains \a y to be the sorted values of \a x, with + \a x[i] = \a y[\a permutation[i]]. Equal values may appear in either order. + The index sets of \a x and \a permutation must agree, and all arrays + must have equal lengths. + Reification is not supported. +*/ +predicate gecode_sort_permutation( + array[$$X] of var $$V: x, + array[$$Y] of var $$V: y, + array[$$X] of var $$Y: permutation, +) = + assert( + index_set(x) = index_set(permutation) /\ length(x) = length(y), + "gecode_sort_permutation: incompatible array indexes or lengths", + if length(y) = 0 then + true + else + gecode_sort_permutation( + enum2int(array1d(x)), + enum2int(array1d(y)), + enum2int(array1d(permutation)), + min(enum2int(index_set(y))), + ) + endif, + ); + +/** @group gecode.constraints + Requires at least one corresponding pair of elements in \a x and \a y + to differ. The arrays must have identical index sets. +*/ +predicate gecode_array_ne(array[$$X] of var $$E: x, array[$$X] of var $$E: y) = + assert( + index_set(x) = index_set(y), + "gecode_array_ne: index set mismatch", + if mzn_in_root_context() then + gecode_array_int_ne(enum2int(array1d(x)), enum2int(array1d(y))) + else + exists (i in index_set(x)) (x[i] != y[i]) + endif, + ); + +/** @group gecode.constraints + Requires at least one corresponding pair of Boolean elements in \a x + and \a y to differ. The arrays must have identical index sets. +*/ +predicate gecode_array_ne(array[$$X] of var bool: x, array[$$X] of var bool: y) = + assert( + index_set(x) = index_set(y), + "gecode_array_ne: index set mismatch", + if mzn_in_root_context() then + gecode_array_bool_ne(array1d(x), array1d(y)) + else + exists (i in index_set(x)) (x[i] != y[i]) + endif, + ); + +/** @group gecode.constraints + Requires at most \a n positions where \a x matches \a values. + The arrays must have identical index sets. + The fixed comparison values do not require additional difference variables. +*/ +predicate gecode_count_matches_at_most(var int: n, array[$$X] of var $$E: x, array[$$X] of $$E: values) = + assert( + index_set(x) = index_set(values), + "gecode_count_matches_at_most: index set mismatch", + if mzn_in_root_context() then + gecode_count_matches_fzn(enum2int(array1d(x)), enum2int(array1d(values)), 3, n) + else + sum (i in index_set(x)) (bool2int(x[i] = values[i])) <= n + endif, + ); + +/** @group gecode.constraints + Requires at least \a n positions where \a x matches \a values. + The arrays must have identical index sets. + The fixed comparison values do not require additional difference variables. +*/ +predicate gecode_count_matches_at_least(var int: n, array[$$X] of var $$E: x, array[$$X] of $$E: values) = + assert( + index_set(x) = index_set(values), + "gecode_count_matches_at_least: index set mismatch", + if mzn_in_root_context() then + gecode_count_matches_fzn(enum2int(array1d(x)), enum2int(array1d(values)), 5, n) + else + sum (i in index_set(x)) (bool2int(x[i] = values[i])) >= n + endif, + ); + +/** @group gecode.constraints + Constrains \a n to be the number of positions where \a x matches + \a values. The arrays must have identical index sets. + The fixed comparison values do not require additional difference variables. +*/ +predicate gecode_count_matches( + var int: n, + array[$$X] of var $$E: x, + array[$$X] of $$E: values, +) = + assert( + index_set(x) = index_set(values), + "gecode_count_matches: index set mismatch", + if mzn_in_root_context() then + gecode_count_matches_fzn(enum2int(array1d(x)), enum2int(array1d(values)), 1, n) + else + sum (i in index_set(x)) (bool2int(x[i] = values[i])) = n + endif, + ); + +/** @group gecode.constraints + Constrains \a result to be the nonnegative greatest common divisor + of \a x and \a y. Negative operands use their absolute values, and + gcd(0, 0) = 0. +*/ +predicate gecode_gcd(var int: x, var int: y, var int: result) = gecode_gcd_int(x, y, result); + +/** @group gecode.constraints + Requires \a dividend to be an integer multiple of \a divisor. + A zero divisor is permitted only when \a dividend is zero. +*/ +predicate gecode_divides(var int: divisor, var int: dividend) = gecode_divides_int(divisor, dividend); + +/** @group gecode.constraints + Constrains \a result to be the product of \a x. + The product of an empty array is one. +*/ +predicate gecode_product(array[$$X] of var int: x, var int: result) = gecode_product_int(array1d(x), result); + +/** @group gecode.constraints + Constrains \a result to be the Euclidean remainder of the product + of \a x modulo \a modulus, with 0 <= \a result < \a modulus. + A nonpositive modulus makes the proposition false. + The product of an empty array is one. +*/ +predicate gecode_product_mod( + array[$$X] of var int: x, + var int: modulus, + var int: result, +) = + if is_fixed(modulus) then + if fix(modulus) > 0 then + gecode_product_mod_fixed_fzn(array1d(x), fix(modulus), result) + else + gecode_product_mod_var_fzn(array1d(x), modulus, result) + endif + else + gecode_product_mod_var_fzn(array1d(x), modulus, result) + endif; + +/** @group gecode.constraints + Constrains \a result to be the smallest distance between any two + positions in \a sites, using \a distances[\a sites[i], \a sites[j]]. + There must be at least two positions. Both matrix axes use the same site + indexes, and the matrix must be symmetric and nonnegative with a zero + diagonal. Repeated sites are permitted. + Reification is not supported. +*/ +predicate gecode_minimum_distance( + array[$$Position] of var $$Site: sites, + array[$$Site, $$Site] of int: distances, + var int: result, +) = + assert( + length(sites) >= 2 /\ + length(distances) > 0 /\ + index_set_1of2(distances) = index_set_2of2(distances), + "gecode_minimum_distance: need at least two positions and a square nonempty distance matrix", + gecode_minimum_distance_fzn( + [enum2int(v) - min(enum2int(index_set_1of2(distances))) | v in sites], + card(index_set_1of2(distances)), + array1d(distances), + result, + ), + ); + +/** @group gecode.constraints + Constrains \a result to be the smallest distance between any two + positions in \a sites. Each pair must also meet the lower bound in + \a requirements[i,j]. There must be at least two positions. + Both axes of \a distances use the same site indexes, and both axes of + \a requirements use the index set of \a sites. Both matrices must be + symmetric and nonnegative with a zero diagonal. Repeated sites are permitted. + Reification is not supported. +*/ +predicate gecode_minimum_distance( + array[$$Position] of var $$Site: sites, + array[$$Site, $$Site] of int: distances, + var int: result, + array[$$Position, $$Position] of int: requirements, +) = + assert( + length(sites) >= 2 /\ + length(distances) > 0 /\ + index_set_1of2(distances) = index_set_2of2(distances) /\ + index_set_1of2(requirements) = index_set(sites) /\ + index_set_2of2(requirements) = index_set(sites), + "gecode_minimum_distance: incompatible distance/requirements matrix or too few positions", + gecode_minimum_distance_required_fzn( + [enum2int(v) - min(enum2int(index_set_1of2(distances))) | v in sites], + card(index_set_1of2(distances)), + array1d(distances), + result, + array1d(requirements), + ), + ); + +/** @group gecode.constraints + Constrains \a y to be the integer root of degree \a degree of \a x, + rounded down. The degree must be positive, and negative \a x is permitted + only for odd degrees. + Reification is not supported. +*/ +predicate gecode_nroot(var int: x, int: degree, var int: y) = + assert(degree > 0, "gecode_nroot: degree must be positive", gecode_int_nroot(x, degree, y)); + +/** @group gecode.constraints + Requires the present rectangles with origins (\a x[i], \a y[i]) + and sizes (\a width[i], \a height[i]) not to overlap. + The two origins of a rectangle must be absent together. + Zero-sized rectangles still participate in non-overlap. + Sizes must be nonnegative, and all arrays must have identical index sets. + Reification is not supported. +*/ +predicate gecode_nooverlap( + array[$$X] of var opt int: x, + array[$$X] of var int: width, + array[$$X] of var opt int: y, + array[$$X] of var int: height, +) = + assert( + index_set(x) = index_set(width) /\ + index_set(x) = index_set(y) /\ + index_set(x) = index_set(height), + "gecode_nooverlap: index set mismatch", + forall (i in index_set(x)) ( + occurs(x[i]) = occurs(y[i]) /\ width[i] >= 0 /\ height[i] >= 0 + ) /\ + let { + array[int] of var bool: present = [occurs(xi) | xi in x]; + array[int] of var int: xx = [xi default 0 | xi in x]; + array[int] of var int: yy = [yi default 0 | yi in y]; + } in + if forall (w in width) (is_fixed(w)) /\ forall (h in height) (is_fixed(h)) then + gecode_nooverlap_optional( + xx, + [fix(w) | w in width], + yy, + [fix(h) | h in height], + present, + ) + else + let { + array[int] of var int: w = array1d(width); + array[int] of var int: h = array1d(height); + array[int] of var int: right = [if present[i] then xx[i] + w[i] else 0 endif | i in index_set(xx)]; + array[int] of var int: top = [if present[i] then yy[i] + h[i] else 0 endif | i in index_set(yy)]; + } in + gecode_nooverlap_flex_optional(xx, w, right, yy, h, top, present) + endif, + ); + +/** @group gecode.constraints + Requires \a x to be empty or a consecutive interval of values. + Enum values follow their declaration order. + Reification is not supported. +*/ +predicate gecode_convex(var set of $$E: x) = gecode_set_convex(enum2int(x)); + +/** @group gecode.constraints + Constrains \a hull to be the smallest consecutive interval + containing \a x. The hull of an empty set is empty. + Enum values follow their declaration order. + Reification is not supported. +*/ +predicate gecode_convex(var set of $$E: x, var set of $$E: hull) = gecode_set_convex_hull(enum2int(x), enum2int(hull)); + +/** @group gecode.constraints + Requires every element of each set in \a x to be smaller than + every element of each later set. Empty sets and arrays are permitted. + Reification is not supported. +*/ +predicate gecode_set_sequence(array[$$X] of var set of $$E: x) = gecode_array_set_seq(enum2int(array1d(x))); + +/** @group gecode.constraints + Requires every element of each set in \a x to be smaller than + every element of each later set, and constrains \a y to their union. + Empty sets and arrays are permitted. An empty array has an empty union. + Reification is not supported. +*/ +predicate gecode_set_sequence(array[$$X] of var set of $$E: x, var set of $$E: y) = + gecode_array_set_seq_union(enum2int(array1d(x)), enum2int(y)); + +/** @group gecode.constraints + Requires each pair of sets in \a x to share at most one element, + and every set to have cardinality \a size. + Reification is not supported. +*/ +predicate gecode_at_most_one_intersection(array[$$X] of var set of $$E: x, int: size) = + assert( + size >= 0, + "gecode_at_most_one_intersection: negative cardinality", + gecode_set_atmost_one(enum2int(array1d(x)), size), + ); + +/** @group gecode.constraints + Constrains \a x to be the elements of \a values in strictly increasing order. + Reification is not supported. +*/ +predicate gecode_sorted_set(array[$$X] of var $$E: x, var set of $$E: values) = + gecode_set_channel_sorted(enum2int(array1d(x)), enum2int(values)); + +/** @group gecode.constraints + Constrains \a index to be the index of a smallest value in \a x. + Any qualifying index is permitted. The array must be nonempty. + Reification is not supported. +*/ +predicate gecode_arg_min_any(array[$$X] of var $$E: x, var $$X: index) = + assert( + length(x) > 0, + "gecode_arg_min_any: empty array", + gecode_arg_min_int( + enum2int(array1d(x)), + 0, + enum2int(index) - min(enum2int(index_set(x))), + false, + ), + ); + +/** @group gecode.constraints + Constrains \a index to be the index of a smallest value in \a x. + Any qualifying index is permitted. The array must be nonempty. + Reification is not supported. +*/ +predicate gecode_arg_min_any(array[$$X] of var bool: x, var $$X: index) = + assert( + length(x) > 0, + "gecode_arg_min_any: empty array", + gecode_arg_min_bool( + array1d(x), + 0, + enum2int(index) - min(enum2int(index_set(x))), + false, + ), + ); + +/** @group gecode.constraints + Constrains \a index to be the index of a largest value in \a x. + Any qualifying index is permitted. The array must be nonempty. + Reification is not supported. +*/ +predicate gecode_arg_max_any(array[$$X] of var $$E: x, var $$X: index) = + assert( + length(x) > 0, + "gecode_arg_max_any: empty array", + gecode_arg_max_int( + enum2int(array1d(x)), + 0, + enum2int(index) - min(enum2int(index_set(x))), + false, + ), + ); + +/** @group gecode.constraints + Constrains \a index to be the index of a largest value in \a x. + Any qualifying index is permitted. The array must be nonempty. + Reification is not supported. +*/ +predicate gecode_arg_max_any(array[$$X] of var bool: x, var $$X: index) = + assert( + length(x) > 0, + "gecode_arg_max_any: empty array", + gecode_arg_max_bool( + array1d(x), + 0, + enum2int(index) - min(enum2int(index_set(x))), + false, + ), + ); + +/** @group gecode.constraints + Requires exactly one element of \a x to be true, with \a value + equal to its array index. The array must be nonempty. + Reification is not supported. +*/ +predicate gecode_one_hot(array[$$X] of var bool: x, var $$X: value) = + assert( + length(x) > 0, + "gecode_one_hot: empty array", + gecode_bool_int_channel(array1d(x), enum2int(value), min(enum2int(index_set(x)))), + ); diff --git a/gecode/flatzinc/mznlib/gecode_fzn.mzn b/gecode/flatzinc/mznlib/gecode_fzn.mzn new file mode 100644 index 0000000000..2ec406d24d --- /dev/null +++ b/gecode/flatzinc/mznlib/gecode_fzn.mzn @@ -0,0 +1,306 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +% Integer relation codes: 1 =, 2 !=, 3 <=, 4 <, 5 >=, 6 >. +% Set relation codes: 1 =, 2 !=, 3 subset, 4 superset. +% Arrays correspond by position unless stated otherwise. +% _reif predicates equate b with the relation; _imp require it when b is true. + +% Constrain every pair of values in x to differ by at least distance. +% The distance is nonnegative, including for empty and singleton arrays. +predicate gecode_inter_distance_fzn(array[int] of var int: x, var int: distance); + +% Constrain values in x whose corresponding present entry is true to +% be pairwise distinct. The arrays have equal lengths. +predicate gecode_all_different_optional( + array[int] of var int: x, + array[int] of var bool: present, +); + +% Constrain the values in x to be pairwise distinct, except that +% except_value may occur more than once. +predicate gecode_all_different_except(array[int] of var int: x, int: except_value); + +% Constrain the sums of corresponding entries in x and offset to be +% pairwise distinct. The arrays must have equal lengths. +predicate gecode_all_different_offset_fzn( + array[int] of int: offset, + array[int] of var int: x, +); + +% Exactly one entry is true; its zero-based position plus offset equals value. +predicate gecode_bool_int_channel( + array[int] of var bool: x, + var int: value, + int: offset, +); + +% Sort x into y; permutation[i]-offset is the zero-based position of x[i] in y. +predicate gecode_sort_permutation( + array[int] of var int: x, + array[int] of var int: y, + array[int] of var int: permutation, + int: offset, +); + +% Compare the number of occurrences of value in x with count. +predicate gecode_count_int_fzn( + array[int] of var int: x, + var int: value, + int: relation, + var int: count, +); + +% Compare the number of position-wise matches between x and values with count. +predicate gecode_count_matches_fzn( + array[int] of var int: x, + array[int] of int: values, + int: relation, + var int: count, +); + +% Arrays have unequal lengths or at least one pair of corresponding entries differs. +predicate gecode_array_int_ne(array[int] of var int: x, array[int] of var int: y); + +predicate gecode_array_bool_ne(array[int] of var bool: x, array[int] of var bool: y); + +% At least two entries differ; empty and singleton arrays cannot satisfy this. +predicate gecode_not_all_equal_int(array[int] of var int: x); + +% z equals x when b is true, and y otherwise. +predicate gecode_int_ite(var bool: b, var int: x, var int: y, var int: z); + +predicate gecode_bool_ite(var bool: b, var bool: x, var bool: y, var bool: z); + +predicate gecode_set_ite( + var bool: b, + var set of int: x, + var set of int: y, + var set of int: z, +); + +predicate gecode_float_ite(var bool: b, var float: x, var float: y, var float: z); + +% result is the nonnegative gcd of x and y; gcd(0,0) is zero. +predicate gecode_gcd_int(var int: x, var int: y, var int: result); +predicate gecode_gcd_int_reif(var int: x, var int: y, var int: result, var bool: b); +predicate gecode_gcd_int_imp(var int: x, var int: y, var int: result, var bool: b); + +% divisor divides dividend; zero divides only zero. +predicate gecode_divides_int(var int: divisor, var int: dividend); +predicate gecode_divides_int_reif(var int: divisor, var int: dividend, var bool: b); +predicate gecode_divides_int_imp(var int: divisor, var int: dividend, var bool: b); + +% result is the product of x; an empty product is one. +predicate gecode_product_int(array[int] of var int: x, var int: result); +predicate gecode_product_int_reif(array[int] of var int: x, var int: result, var bool: b); +predicate gecode_product_int_imp(array[int] of var int: x, var int: result, var bool: b); + +% The product has Euclidean residue result: modulus > 0 and 0 <= result < modulus. +predicate gecode_product_mod_fixed_fzn(array[int] of var int: x, int: modulus, var int: result); +predicate gecode_product_mod_fixed_fzn_reif(array[int] of var int: x, int: modulus, var int: result, var bool: b); +predicate gecode_product_mod_fixed_fzn_imp(array[int] of var int: x, int: modulus, var int: result, var bool: b); +predicate gecode_product_mod_var_fzn(array[int] of var int: x, var int: modulus, var int: result); +predicate gecode_product_mod_var_fzn_reif(array[int] of var int: x, var int: modulus, var int: result, var bool: b); +predicate gecode_product_mod_var_fzn_imp(array[int] of var int: x, var int: modulus, var int: result, var bool: b); + +% sites use zero-based labels; distances is a row-major size-by-size matrix. +predicate gecode_minimum_distance_fzn( + array[int] of var int: sites, + int: size, + array[int] of int: distances, + var int: result, +); + +% requirements is a row-major square matrix of pairwise lower bounds, +% with one row per entry in sites. +predicate gecode_minimum_distance_required_fzn( + array[int] of var int: sites, + int: size, + array[int] of int: distances, + var int: result, + array[int] of int: requirements, +); + +% y is floor(root(x,n)); n is positive, and negative x requires odd n. +predicate gecode_int_nroot(var int: x, int: n, var int: y); + +% NFA rows are states 1..q, columns are first_symbol..first_symbol+symbols-1. +% Each entry gives the set of target states; an empty set rejects. +predicate gecode_regular_nfa_int_fzn( + array[int] of var int: x, + int: q, + int: first_symbol, + int: symbols, + array[int] of set of int: transitions, + int: initial, + set of int: final, +); + +% Constrain tasks whose present entry is true not to overlap. Durations are +% nonnegative. The arrays have equal lengths. The caller must also constrain +% start[i] + duration[i] = end[i] for each present task. +predicate gecode_unary_flex_optional( + array[int] of var int: start, + array[int] of var int: duration, + array[int] of var int: end, + array[int] of var bool: present, +); + +% Constrain the total usage of tasks whose present entry is true not to +% exceed capacity. Durations, usage, and capacity are nonnegative. +% The arrays have equal lengths. The caller must also constrain +% start[i] + duration[i] = end[i] for each present task. +predicate gecode_cumulative_flex_optional( + array[int] of var int: start, + array[int] of var int: duration, + array[int] of var int: end, + array[int] of int: usage, + var int: capacity, + array[int] of var bool: present, +); + +% Present rectangles have nonnegative fixed widths and heights and cannot overlap. +predicate gecode_nooverlap_optional( + array[int] of var int: x, + array[int] of int: width, + array[int] of var int: y, + array[int] of int: height, + array[int] of var bool: present, +); + +% Present rectangles cannot overlap. The caller must also constrain +% x[i]+width[i]=right[i] and y[i]+height[i]=top[i] for present rectangles. +predicate gecode_nooverlap_flex_optional( + array[int] of var int: x, + array[int] of var int: width, + array[int] of var int: right, + array[int] of var int: y, + array[int] of var int: height, + array[int] of var int: top, + array[int] of var bool: present, +); + +% hull is empty when x is empty, and min(x)..max(x) otherwise. +predicate gecode_set_convex_hull(var set of int: x, var set of int: hull); + +% x is empty or contains every integer between its minimum and maximum. +predicate gecode_set_convex(var set of int: x); + +% Constrain each set in x to have cardinality elements and each pair of +% sets to intersect in at most one element. The cardinality is nonnegative. +predicate gecode_set_atmost_one(array[int] of var set of int: x, int: cardinality); + +% Constrain x to list the elements of y in strictly increasing order. +predicate gecode_set_channel_sorted(array[int] of var int: x, var set of int: y); + +% Constrain y to be the intersection of all sets in x. +% The intersection of an empty array is the full Gecode set universe. +predicate gecode_array_set_intersect( + array[int] of var set of int: x, + var set of int: y, +); + +% Constrain value to be the set at (column, row) in the row-major +% x matrix. Coordinates are zero-based; width and height are positive +% and their product equals the length of x. +predicate gecode_set_element2d( + array[int] of var set of int: x, + var int: column, + int: width, + var int: row, + int: height, + var set of int: value, +); + +% Constrain y to be x raised to the nonnegative integer n. +predicate gecode_float_pow(var float: x, int: n, var float: y); + +% Constrain y to be the minimum of the nonempty array x. +predicate gecode_float_array_min(array[int] of var float: x, var float: y); + +% Constrain y to be the maximum of the nonempty array x. +predicate gecode_float_array_max(array[int] of var float: x, var float: y); + +% Constrain y to be the positive fixed base raised to x. Requires MPFR. +predicate gecode_float_pow_base(float: base, var float: x, var float: y); + +% index is the zero-based position plus offset of an extremum. +% If break_ties is true, choose the first such position. Arrays are nonempty. +predicate gecode_arg_min_int( + array[int] of var int: x, + int: offset, + var int: index, + bool: break_ties, +); + +predicate gecode_arg_max_int( + array[int] of var int: x, + int: offset, + var int: index, + bool: break_ties, +); + +predicate gecode_arg_min_bool( + array[int] of var bool: x, + int: offset, + var int: index, + bool: break_ties, +); + +predicate gecode_arg_max_bool( + array[int] of var bool: x, + int: offset, + var int: index, + bool: break_ties, +); + +% x is the minimum of the nonempty set s; reified forms are false for empty s. +predicate gecode_set_min(var set of int: s, var int: x); + +predicate gecode_set_min_reif(var set of int: s, var int: x, var bool: b); + +predicate gecode_set_min_imp(var set of int: s, var int: x, var bool: b); + +% x is the maximum of the nonempty set s; reified forms are false for empty s. +predicate gecode_set_max(var set of int: s, var int: x); + +predicate gecode_set_max_reif(var set of int: s, var int: x, var bool: b); + +predicate gecode_set_max_imp(var set of int: s, var int: x, var bool: b); + +% Every element precedes all elements in later nonempty sets; sets are disjoint. +predicate gecode_array_set_seq(array[int] of var set of int: x); +predicate gecode_array_set_seq_union(array[int] of var set of int: x, var set of int: y); + +predicate gecode_float_rel_imp_fzn(var float: x, int: relation, var float: y, var bool: b); +predicate gecode_set_rel_imp_fzn(var set of int: x, int: relation, var set of int: y, var bool: b); diff --git a/gecode/flatzinc/mznlib/redefinitions-2.0.mzn b/gecode/flatzinc/mznlib/redefinitions-2.0.mzn index 2bc9c419de..591486424e 100644 --- a/gecode/flatzinc/mznlib/redefinitions-2.0.mzn +++ b/gecode/flatzinc/mznlib/redefinitions-2.0.mzn @@ -7,24 +7,50 @@ predicate bool_clause_reif(array[int] of var bool: as, predicate array_int_maximum(var int: m, array[int] of var int: x); +predicate gecode_float_array_max(array[int] of var float: x, var float: m); + predicate array_float_maximum(var float: m, array[int] of var float: x) = - let { int: l = min(index_set(x)), - int: u = max(index_set(x)), - float: ly = lb_array(x), - float: uy = ub_array(x), - array[l..u] of var ly..uy: y } in - y[l] = x[l] /\ - m = y[u] /\ - forall (i in l+1 .. u) ( y[i] == max(x[i],y[i-1]) ); + if length(x) = 0 then + false + else + gecode_float_array_max(x, m) + endif; predicate array_int_minimum(var int: m, array[int] of var int: x); +predicate gecode_float_array_min(array[int] of var float: x, var float: m); + predicate array_float_minimum(var float: m, array[int] of var float: x) = - let { int: l = min(index_set(x)), - int: u = max(index_set(x)), - float: ly = lb_array(x), - float: uy = ub_array(x), - array[l..u] of var ly..uy: y } in - y[l] = x[l] /\ - m = y[u] /\ - forall (i in l+1 .. u) ( y[i] == min(x[i],y[i-1]) ); + if length(x) = 0 then + false + else + gecode_float_array_min(x, m) + endif; + +predicate gecode_float_pow(var float: x, int: n, var float: y); +predicate gecode_float_pow_base(float: base, var float: x, var float: y); + +% Nonnegative integer exponents permit zero or negative bases. +predicate float_pow(var float: x, var float: exponent, var float: y) = + let { + float: n = if is_fixed(exponent) then + fix(exponent) + else + -1.0 + endif; + bool: integer_exponent = if n >= 0.0 /\ n <= 2147483646.0 then + n = int2float(floor(n)) + else + false + endif; + } in + if integer_exponent then + gecode_float_pow(x, floor(n), y) + elseif is_fixed(x) /\ fix(x) > 0.0 then + gecode_float_pow_base(fix(x), exponent, y) + else + assert( + false, + "Gecode float_pow requires a nonnegative integer exponent or a fixed positive base", + ) + endif; diff --git a/gecode/flatzinc/mznlib/redefinitions-2.1.1.mzn b/gecode/flatzinc/mznlib/redefinitions-2.1.1.mzn new file mode 100644 index 0000000000..fa1bd421c8 --- /dev/null +++ b/gecode/flatzinc/mznlib/redefinitions-2.1.1.mzn @@ -0,0 +1,116 @@ +% +% Main authors: +% Mikael Zayenz Lagerkvist +% +% Copyright: +% Mikael Zayenz Lagerkvist, 2026 +% +% This file is part of Gecode, the generic constraint +% development environment: +% http://www.gecode.dev +% +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% "Software"), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be +% included in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +% EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +% +% + +% Set extrema are undefined for empty sets. The partial functions guard the +% extremum constraint with set nonemptiness, for use in inactive expressions. +predicate gecode_set_min(var set of int: s, var int: m); +predicate gecode_set_min_reif(var set of int: s, var int: m, var bool: b); +predicate gecode_set_min_imp(var set of int: s, var int: m, var bool: b); +predicate gecode_set_max(var set of int: s, var int: m); +predicate gecode_set_max_reif(var set of int: s, var int: m, var bool: b); +predicate gecode_set_max_imp(var set of int: s, var int: m, var bool: b); + +function var $$E: min(var set of $$E: s) = + if card(ub(enum2int(s))) = 0 then + % An empty upper bound makes the extremum undefined at compilation. + let { + var set of int: si = enum2int(s); + var min(ub(si)) .. max(ub(si)): m = min([e + (max(ub(si)) + 1 - e) * (1 - (e in si)) | e in ub(si)]); + } in + to_enum_internal(enum_of(s), m) + else + to_enum_internal( + enum_of(s), + if mzn_in_root_context() then + gecode_set_min_value(enum2int(s)) + else + let { + constraint card(s) > 0; + } in + gecode_set_min_partial(enum2int(s)) + endif, + ) + endif; + +function var int: gecode_set_min_value(var set of int: s) :: promise_total = + let { + var min(ub(s) union {1}) .. max(ub(s) union {1}): m :: is_defined_var; + constraint card(s) > 0; + constraint gecode_set_min(s, m) :: defines_var(m); + } in + m; + +function var int: gecode_set_min_partial(var set of int: s) :: promise_total = + let { + var min(ub(s) union {1}) .. max(ub(s) union {1}): m :: is_defined_var; + var bool: present = card(s) > 0; + constraint gecode_set_min_imp(s, m, present) :: defines_var(m); + } in + m; + +function var $$E: max(var set of $$E: s) = + if card(ub(enum2int(s))) = 0 then + % An empty upper bound makes the extremum undefined at compilation. + let { + var set of int: si = enum2int(s); + var min(ub(si)) .. max(ub(si)): m = max([e + (min(ub(si)) - 1 - e) * (1 - (e in si)) | e in ub(si)]); + } in + to_enum_internal(enum_of(s), m) + else + to_enum_internal( + enum_of(s), + if mzn_in_root_context() then + gecode_set_max_value(enum2int(s)) + else + let { + constraint card(s) > 0; + } in + gecode_set_max_partial(enum2int(s)) + endif, + ) + endif; + +function var int: gecode_set_max_value(var set of int: s) :: promise_total = + let { + var min(ub(s) union {1}) .. max(ub(s) union {1}): m :: is_defined_var; + constraint card(s) > 0; + constraint gecode_set_max(s, m) :: defines_var(m); + } in + m; + +function var int: gecode_set_max_partial(var set of int: s) :: promise_total = + let { + var min(ub(s) union {1}) .. max(ub(s) union {1}): m :: is_defined_var; + var bool: present = card(s) > 0; + constraint gecode_set_max_imp(s, m, present) :: defines_var(m); + } in + m; diff --git a/gecode/flatzinc/mznlib/redefinitions-2.5.2.mzn b/gecode/flatzinc/mznlib/redefinitions-2.5.2.mzn index 45f8c949db..451382ee54 100644 --- a/gecode/flatzinc/mznlib/redefinitions-2.5.2.mzn +++ b/gecode/flatzinc/mznlib/redefinitions-2.5.2.mzn @@ -14,8 +14,30 @@ predicate array_var_float_element2d_nonshifted(var int: idx1, var int: idx2, arr int: min_flat = min(index_set_1of2(x))*dim+min(index_set_2of2(x))-1; } in array_var_float_element_nonshifted((idx1*dim+idx2-min_flat)::domain, array1d(x), c); -predicate array_var_set_element2d_nonshifted(var int: idx1, var int: idx2, array[int,int] of var set of int: x, var set of int: c) = - let { - int: dim = card(index_set_2of2(x)); - int: min_flat = min(index_set_1of2(x))*dim+min(index_set_2of2(x))-1; - } in array_var_set_element_nonshifted((idx1*dim+idx2-min_flat)::domain, array1d(x), c); +predicate gecode_set_element2d( + array[int] of var set of int: x, + var int: column, + int: width, + var int: row, + int: height, + var set of int: value, +); + +predicate array_var_set_element2d_nonshifted( + var int: idx1, + var int: idx2, + array[int, int] of var set of int: x, + var set of int: c, +) = + if length(x) = 0 then + false + else + gecode_set_element2d( + array1d(x), + idx2 - min(index_set_2of2(x)), + card(index_set_2of2(x)), + idx1 - min(index_set_1of2(x)), + card(index_set_1of2(x)), + c, + ) + endif; diff --git a/gecode/flatzinc/mznlib/redefinitions.mzn b/gecode/flatzinc/mznlib/redefinitions.mzn index e1e388009a..3629dbfb84 100644 --- a/gecode/flatzinc/mznlib/redefinitions.mzn +++ b/gecode/flatzinc/mznlib/redefinitions.mzn @@ -136,3 +136,86 @@ predicate int_lin_ne_imp(array [int] of int: as, array [int] of var int: bs, int: c, var bool: r); predicate set_in_imp(var int: x, set of int: S, var bool: r); + +% b implies the scalar float relation; a false b leaves x and y unconstrained. +predicate gecode_float_rel_imp_fzn( + var float: x, + int: relation, + var float: y, + var bool: b, +); +predicate float_eq_imp(var float: x, var float: y, var bool: b) = gecode_float_rel_imp_fzn(x, 1, y, b); +predicate float_ne_imp(var float: x, var float: y, var bool: b) = gecode_float_rel_imp_fzn(x, 2, y, b); +predicate float_le_imp(var float: x, var float: y, var bool: b) = gecode_float_rel_imp_fzn(x, 3, y, b); +predicate float_lt_imp(var float: x, var float: y, var bool: b) = gecode_float_rel_imp_fzn(x, 4, y, b); + +% MiniZinc represents scalar comparisons as one- or two-term linear forms. +% Other linear expressions use full reification followed by implication. +predicate gecode_float_lin_scalar_imp( + array[int] of float: a, + array[int] of var float: x, + float: y, + int: relation, + var bool: b, +) = + let { + array[int] of float: aa = array1d(a); + array[int] of var float: xx = array1d(x); + } in + if length(aa) = 1 /\ length(xx) = 1 /\ aa[1] = 1.0 then + gecode_float_rel_imp_fzn(xx[1], relation, y, b) + elseif length(aa) = 2 /\ length(xx) = 2 /\ y = 0.0 /\ aa[1] = 1.0 /\ aa[2] = -1.0 then + gecode_float_rel_imp_fzn(xx[1], relation, xx[2], b) + elseif length(aa) = 2 /\ length(xx) = 2 /\ y = 0.0 /\ aa[1] = -1.0 /\ aa[2] = 1.0 then + gecode_float_rel_imp_fzn(xx[2], relation, xx[1], b) + else + let { + var bool: r; + } in + (if relation = 1 then + float_lin_eq_reif(a, x, y, r) + elseif relation = 2 then + float_lin_eq_reif(a, x, y, not r) + elseif relation = 3 then + float_lin_le_reif(a, x, y, r) + else + float_lin_lt_reif(a, x, y, r) + endif) /\ + bool_clause([r], [b]) + endif; + +predicate float_lin_eq_imp( + array[int] of float: a, + array[int] of var float: x, + float: y, + var bool: b, +) = gecode_float_lin_scalar_imp(a, x, y, 1, b); +predicate float_lin_ne_imp( + array[int] of float: a, + array[int] of var float: x, + float: y, + var bool: b, +) = gecode_float_lin_scalar_imp(a, x, y, 2, b); +predicate float_lin_le_imp( + array[int] of float: a, + array[int] of var float: x, + float: y, + var bool: b, +) = gecode_float_lin_scalar_imp(a, x, y, 3, b); +predicate float_lin_lt_imp( + array[int] of float: a, + array[int] of var float: x, + float: y, + var bool: b, +) = gecode_float_lin_scalar_imp(a, x, y, 4, b); + +predicate gecode_set_rel_imp_fzn( + var set of int: x, + int: relation, + var set of int: y, + var bool: b, +); +predicate set_eq_imp(var set of int: x, var set of int: y, var bool: b) = gecode_set_rel_imp_fzn(x, 1, y, b); +predicate set_ne_imp(var set of int: x, var set of int: y, var bool: b) = gecode_set_rel_imp_fzn(x, 2, y, b); +predicate set_subset_imp(var set of int: x, var set of int: y, var bool: b) = gecode_set_rel_imp_fzn(x, 3, y, b); +predicate set_superset_imp(var set of int: x, var set of int: y, var bool: b) = gecode_set_rel_imp_fzn(x, 4, y, b); diff --git a/gecode/flatzinc/registry.cpp b/gecode/flatzinc/registry.cpp index 8df3f19214..4c05a3dd66 100755 --- a/gecode/flatzinc/registry.cpp +++ b/gecode/flatzinc/registry.cpp @@ -1213,6 +1213,40 @@ namespace Gecode { namespace FlatZinc { ce[6]->getSet(), ann); } + + void p_regular_nfa_int(FlatZincSpace& s, const ConExpr& ce, + AST::Node* ann) { + IntVarArgs x = s.arg2intvarargs(ce[0]); + int q = ce[1]->getInt(), first_symbol = ce[2]->getInt(); + int symbols = ce[3]->getInt(), initial = ce[5]->getInt(); + IntSetArgs table = s.arg2intsetargs(ce[4]); + IntSet finals = s.arg2intset(ce[6]); + if ((q <= 0) || (symbols <= 0) || + (static_cast(q)*symbols != table.size()) || + (initial < 1) || (initial > q) || + ((finals.size() != 0) && ((finals.min() < 1) || (finals.max() > q))) || + (first_symbol < Int::Limits::min) || + (static_cast(first_symbol)+symbols-1 > Int::Limits::max)) + throw FlatZinc::Error("Registry", "invalid NFA dimensions or states"); + std::vector transitions; + for (int state=0; state q))) + throw FlatZinc::Error("Registry", "invalid NFA transition"); + for (IntSetValues target(targets); target(); ++target) + transitions.push_back(DFA::Transition(state+1,first_symbol+symbol,target.val())); + } + transitions.push_back(DFA::Transition(-1,0,0)); + std::vector accepting; + for (IntSetValues final(finals); final(); ++final) + accepting.push_back(final.val()); + accepting.push_back(-1); + DFA automaton = DFA::nfa(initial,transitions.data(),accepting.data()); + unshare(s,x); + extensional(s,x,s.getSharedDFA(automaton),s.ann2ipl(ann)); + } + void p_sort(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs x = s.arg2intvarargs(ce[0]); @@ -1325,7 +1359,7 @@ namespace Gecode { namespace FlatZinc { IntArgs duration = s.arg2intargs(ce[1]); IntArgs height = s.arg2intargs(ce[2]); BoolVarArgs opt = s.arg2boolvarargs(ce[3]); - int bound = ce[4]->getInt(); + IntVar bound = s.arg2IntVar(ce[4]); unshare(s,start); cumulative(s,bound,start,duration,height,opt,s.ann2ipl(ann)); } @@ -1769,11 +1803,272 @@ fvar, mode, target, args, reason); } + + // The codes follow the declaration order of GecodeIntRelation in gecode.mzn. + IntRelType int_relation(AST::Node* arg) { + switch (arg->getInt()) { + case 1: return IRT_EQ; + case 2: return IRT_NQ; + case 3: return IRT_LQ; + case 4: return IRT_LE; + case 5: return IRT_GQ; + case 6: return IRT_GR; + default: throw FlatZinc::Error("Registry", "invalid integer relation"); + } + } + + void p_inter_distance(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + IntVarArgs x = s.arg2intvarargs(ce[0]); + if (ce[1]->isIntVar()) { + // The native propagator rejects aliases between x and the distance. + x << s.arg2IntVar(ce[1]); + unshare(s, x); + inter_distance(s, x.slice(0,1,x.size()-1), x[x.size()-1], + s.ann2ipl(ann)); + } else { + if (ce[1]->getInt() < 0) { + s.fail(); + return; + } + unshare(s, x); + inter_distance(s, x, ce[1]->getInt(), s.ann2ipl(ann)); + } + } + + void p_distinct_optional(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + IntVarArgs x = s.arg2intvarargs(ce[0]); + BoolVarArgs present = s.arg2boolvarargs(ce[1]); + if (x.size() != present.size()) + throw FlatZinc::Error("Registry", "optional distinct arrays must have equal lengths"); + int lo = Int::Limits::max, hi = Int::Limits::min, n = 0; + bool mandatory = true; + for (int i=0; i Int::Limits::min+n)) { + unshare(s, x); + distinct(s, present, x, s.ann2ipl(ann)); + } else if (mandatory) { + IntVarArgs active; + for (int i=0; igetInt(); + // An excluded value outside the variable limits cannot occur in x. + if ((c < Int::Limits::min) || (c > Int::Limits::max)) { + unshare(s, x); + distinct(s, x, s.ann2ipl(ann)); + return; + } + int lo = Int::Limits::max, hi = Int::Limits::min, n = 0; + for (int i=0; i Int::Limits::min+n)) { + unshare(s, x); + distinct(s, x, c, s.ann2ipl(ann)); + } else { + for (int i=0; igetInt(), s.ann2ipl(ann)); + } + void p_sort_permutation(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + IntVarArgs x = s.arg2intvarargs(ce[0]); + IntVarArgs y = s.arg2intvarargs(ce[1]); + IntVarArgs z = s.arg2intvarargs(ce[2]); + if ((x.size() != y.size()) || (x.size() != z.size())) + throw FlatZinc::Error("Registry", "sort arrays must have equal lengths"); + int offset = ce[3]->getInt(); + for (int i=0; i + void p_gcd_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + gcd(s, s.arg2IntVar(ce[0]), s.arg2IntVar(ce[1]), s.arg2IntVar(ce[2]), + Reify(s.arg2BoolVar(ce[3]), mode), s.ann2ipl(ann)); + } + void p_divides(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + divides(s, s.arg2IntVar(ce[0]), s.arg2IntVar(ce[1]), + Reify(BoolVar(s,1,1),RM_EQV), s.ann2ipl(ann)); + } + template + void p_divides_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + divides(s, s.arg2IntVar(ce[0]), s.arg2IntVar(ce[1]), + Reify(s.arg2BoolVar(ce[2]),mode), s.ann2ipl(ann)); + } + void p_product(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + product(s, s.arg2intvarargs(ce[0]), s.arg2IntVar(ce[1]), s.ann2ipl(ann)); + } + template + void p_product_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + product(s, s.arg2intvarargs(ce[0]), s.arg2IntVar(ce[1]), + Reify(s.arg2BoolVar(ce[2]),mode), s.ann2ipl(ann)); + } + template + void p_product_mod(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + IntVarArgs x = s.arg2intvarargs(ce[0]); + IntVar y = s.arg2IntVar(ce[2]); + if (fixed) + product_mod(s,x,ce[1]->getInt(),y,s.ann2ipl(ann)); + else + product_mod(s,x,s.arg2IntVar(ce[1]),y,s.ann2ipl(ann)); + } + template + void p_product_mod_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + IntVarArgs x = s.arg2intvarargs(ce[0]); + IntVar y = s.arg2IntVar(ce[2]); + Reify r(s.arg2BoolVar(ce[3]),mode); + if (fixed) + product_mod(s,x,ce[1]->getInt(),y,r,s.ann2ipl(ann)); + else + product_mod(s,x,s.arg2IntVar(ce[1]),y,r,s.ann2ipl(ann)); + } + void p_minimum_distance(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + IntVarArgs x = s.arg2intvarargs(ce[0]); + IntDistance d(ce[1]->getInt(),s.arg2intargs(ce[2])); + MinDistancePropKind kind = ann && ann->hasAtom("gecode_decomposed_propagation") + ? MDP_DECOMPOSED : MDP_SINGLE; + if (ce.size() == 5) + minimum_distance(s,x,s.arg2IntVar(ce[3]),d, + s.arg2intargs(ce[4]),s.ann2ipl(ann),kind); + else + minimum_distance(s,x,s.arg2IntVar(ce[3]),d,s.ann2ipl(ann),kind); + } + + void p_int_nroot(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + nroot(s, s.arg2IntVar(ce[0]), ce[1]->getInt(), s.arg2IntVar(ce[2]), + s.ann2ipl(ann)); + } + + void p_nooverlap_optional(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + nooverlap(s, s.arg2intvarargs(ce[0]), s.arg2intargs(ce[1]), + s.arg2intvarargs(ce[2]), s.arg2intargs(ce[3]), + s.arg2boolvarargs(ce[4]), s.ann2ipl(ann)); + } + void p_nooverlap_flex(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + nooverlap(s, s.arg2intvarargs(ce[0]), s.arg2intvarargs(ce[1]), + s.arg2intvarargs(ce[2]), s.arg2intvarargs(ce[3]), + s.arg2intvarargs(ce[4]), s.arg2intvarargs(ce[5]), + s.arg2boolvarargs(ce[6]), s.ann2ipl(ann)); + } + + void p_arg_min_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + IntVarArgs xy = s.arg2intvarargs(ce[0]); + xy << s.arg2IntVar(ce[2]); + unshare(s, xy); + argmin(s, xy.slice(0,1,xy.size()-1), ce[1]->getInt(), + xy[xy.size()-1], ce[3]->getBool(), s.ann2ipl(ann)); + } + + void p_arg_max_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + IntVarArgs xy = s.arg2intvarargs(ce[0]); + xy << s.arg2IntVar(ce[2]); + unshare(s, xy); + argmax(s, xy.slice(0,1,xy.size()-1), ce[1]->getInt(), + xy[xy.size()-1], ce[3]->getBool(), s.ann2ipl(ann)); + } + + void p_arg_min_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + BoolVarArgs x = s.arg2boolvarargs(ce[0]); + argmin(s, x, ce[1]->getInt(), s.arg2IntVar(ce[2]), + ce[3]->getBool(), s.ann2ipl(ann)); + } + + void p_arg_max_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + BoolVarArgs x = s.arg2boolvarargs(ce[0]); + argmax(s, x, ce[1]->getInt(), s.arg2IntVar(ce[2]), + ce[3]->getBool(), s.ann2ipl(ann)); + } + + void p_unary_flex_optional(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + IntVarArgs start = s.arg2intvarargs(ce[0]); + unshare(s, start); + unary(s, start, s.arg2intvarargs(ce[1]), s.arg2intvarargs(ce[2]), + s.arg2boolvarargs(ce[3]), s.ann2ipl(ann)); + } + + + void p_cumulative_flex_optional(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + IntVarArgs start = s.arg2intvarargs(ce[0]); + unshare(s, start); + cumulative(s, s.arg2IntVar(ce[4]), start, s.arg2intvarargs(ce[1]), + s.arg2intvarargs(ce[2]), s.arg2intargs(ce[3]), + s.arg2boolvarargs(ce[5]), s.ann2ipl(ann)); + } + class IntPoster { public: IntPoster(void) { registry().add("all_different_int", &p_distinct); registry().add("all_different_offset", &p_distinctOffset); + registry().add("gecode_all_different_offset_fzn", &p_distinctOffset); registry().add("all_equal_int", &p_all_equal); registry().add("int_eq", &p_int_eq); registry().add("int_ne", &p_int_ne); @@ -1950,6 +2245,7 @@ fvar, registry().add("gecode_circuit_cost_array", &p_circuit_cost_array); registry().add("gecode_circuit_cost", &p_circuit_cost); registry().add("gecode_nooverlap", &p_nooverlap); + registry().add("gecode_nooverlap_fzn", &p_nooverlap); registry().add("gecode_precede", &p_precede); registry().add("nvalue",&p_nvalue); registry().add("among",&p_among); @@ -1958,6 +2254,47 @@ fvar, registry().add("member_bool",&p_member_bool); registry().add("gecode_member_bool_reif",&p_member_bool_reif); + registry().add("gecode_unary_flex_optional", &p_unary_flex_optional); + registry().add("gecode_cumulative_flex_optional", &p_cumulative_flex_optional); + registry().add("gecode_array_int_ne", &p_array_int_ne); + registry().add("gecode_not_all_equal_int", &p_not_all_equal_int); + registry().add("gecode_array_bool_ne", &p_array_bool_ne); + registry().add("gecode_inter_distance", &p_inter_distance); + registry().add("gecode_inter_distance_fzn", &p_inter_distance); + registry().add("gecode_bool_int_channel", &p_bool_int_channel); + registry().add("gecode_sort_permutation", &p_sort_permutation); + registry().add("gecode_count_int_fzn", &p_count_int); + registry().add("gecode_count_matches_fzn", &p_count_matches); + registry().add("gecode_int_ite", &p_int_ite); + registry().add("gecode_bool_ite", &p_bool_ite); + registry().add("gecode_gcd_int", &p_gcd); + registry().add("gecode_gcd_int_reif", &p_gcd_reif); + registry().add("gecode_gcd_int_imp", &p_gcd_reif); + registry().add("gecode_divides_int", &p_divides); + registry().add("gecode_divides_int_reif", &p_divides_reif); + registry().add("gecode_divides_int_imp", &p_divides_reif); + registry().add("gecode_product_int", &p_product); + registry().add("gecode_product_int_reif", &p_product_reif); + registry().add("gecode_product_int_imp", &p_product_reif); + registry().add("gecode_product_mod_fixed_fzn", &p_product_mod); + registry().add("gecode_product_mod_fixed_fzn_reif", &p_product_mod_reif); + registry().add("gecode_product_mod_fixed_fzn_imp", &p_product_mod_reif); + registry().add("gecode_product_mod_var_fzn", &p_product_mod); + registry().add("gecode_product_mod_var_fzn_reif", &p_product_mod_reif); + registry().add("gecode_product_mod_var_fzn_imp", &p_product_mod_reif); + registry().add("gecode_minimum_distance_fzn", &p_minimum_distance); + registry().add("gecode_minimum_distance_required_fzn", &p_minimum_distance); + registry().add("gecode_int_nroot", &p_int_nroot); + registry().add("gecode_nooverlap_optional", &p_nooverlap_optional); + registry().add("gecode_all_different_optional", &p_distinct_optional); + registry().add("gecode_all_different_except", &p_distinct_except); + registry().add("gecode_regular_nfa_int_fzn", &p_regular_nfa_int); + registry().add("gecode_nooverlap_flex_optional", &p_nooverlap_flex); + registry().add("gecode_arg_min_int", &p_arg_min_int); + registry().add("gecode_arg_max_int", &p_arg_max_int); + registry().add("gecode_arg_min_bool", &p_arg_min_bool); + registry().add("gecode_arg_max_bool", &p_arg_max_bool); + registry().add("gecode_blackbox", &p_blackbox); registry().add("gecode_blackbox_bounds", &p_blackbox_bounds); } @@ -2201,7 +2538,8 @@ fvar, void p_array_set_seq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { SetVarArgs sv = s.arg2setvarargs(ce[0]); - sequence(s, sv); + if (sv.size() > 0) + sequence(s, sv); } void p_array_set_seq_union(FlatZincSpace& s, const ConExpr& ce, @@ -2259,6 +2597,84 @@ fvar, precede(s,x,p_s,p_t); } + + SetRelType set_relation(AST::Node* arg) { + switch (arg->getInt()) { + case 1: return SRT_EQ; + case 2: return SRT_NQ; + case 3: return SRT_SUB; + case 4: return SRT_SUP; + case 5: return SRT_DISJ; + case 6: return SRT_CMPL; + case 7: return SRT_LQ; + case 8: return SRT_LE; + case 9: return SRT_GQ; + case 10: return SRT_GR; + default: throw FlatZinc::Error("Registry", "invalid set relation"); + } + } + void p_set_ite(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { + ite(s, s.arg2BoolVar(ce[0]), s.arg2SetVar(ce[1]), s.arg2SetVar(ce[2]), + s.arg2SetVar(ce[3])); + } + void p_set_convex_hull(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { + convex(s, s.arg2SetVar(ce[0]), s.arg2SetVar(ce[1])); + } + void p_set_atmost_one(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { + int cardinality = ce[1]->getInt(); + if (cardinality < 0) + throw FlatZinc::Error("Registry", "set cardinality must be nonnegative"); + SetVarArgs x = s.arg2setvarargs(ce[0]); + if ((x.size() < 2) || (cardinality <= 1)) { + // The intersection bound is trivial here. atmostOne skips cardinality + // for fewer than two sets, and its filter divides by cardinality - 1. + for (int i=0; i(cardinality)); + } + } + void p_set_channel_sorted(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { + channelSorted(s, s.arg2intvarargs(ce[0]), s.arg2SetVar(ce[1])); + } + void p_array_set_intersect(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { + rel(s, SOT_INTER, s.arg2setvarargs(ce[0]), s.arg2SetVar(ce[1])); + } + void p_set_element2d(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { + SetVarArgs x = s.arg2setvarargs(ce[0]); + int width = ce[2]->getInt(), height = ce[4]->getInt(); + if ((width <= 0) || (height <= 0) || + (static_cast(width)*height != x.size())) + throw FlatZinc::Error("Registry", "invalid set matrix dimensions"); + element(s, x, s.arg2IntVar(ce[1]), width, + s.arg2IntVar(ce[3]), height, s.arg2SetVar(ce[5])); + } + + void p_set_min(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { + min(s, s.arg2SetVar(ce[0]), s.arg2IntVar(ce[1])); + } + template + void p_set_min_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { + min(s, s.arg2SetVar(ce[0]), s.arg2IntVar(ce[1]), + Reify(s.arg2BoolVar(ce[2]), mode)); + } + + void p_set_max(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { + max(s, s.arg2SetVar(ce[0]), s.arg2IntVar(ce[1])); + } + template + void p_set_max_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { + max(s, s.arg2SetVar(ce[0]), s.arg2IntVar(ce[1]), + Reify(s.arg2BoolVar(ce[2]), mode)); + } + + + + void p_set_rel_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { + rel(s, s.arg2SetVar(ce[0]), set_relation(ce[1]), s.arg2SetVar(ce[2]), + Reify(s.arg2BoolVar(ce[3]), RM_IMP)); + } + class SetPoster { public: SetPoster(void) { @@ -2311,6 +2727,20 @@ fvar, &p_weights); registry().add("gecode_inverse_set", &p_inverse_set); registry().add("gecode_precede_set", &p_precede_set); + registry().add("gecode_set_rel_imp_fzn", &p_set_rel_imp); + registry().add("gecode_set_ite", &p_set_ite); + registry().add("gecode_set_convex_hull", &p_set_convex_hull); + registry().add("gecode_set_atmost_one", &p_set_atmost_one); + registry().add("gecode_set_channel_sorted", &p_set_channel_sorted); + registry().add("gecode_array_set_intersect", &p_array_set_intersect); + registry().add("gecode_set_element2d", &p_set_element2d); + registry().add("gecode_set_min", &p_set_min); + registry().add("gecode_set_min_reif", &p_set_min_reif); + registry().add("gecode_set_min_imp", &p_set_min_reif); + registry().add("gecode_set_max", &p_set_max); + registry().add("gecode_set_max_reif", &p_set_max_reif); + registry().add("gecode_set_max_imp", &p_set_max_reif); + } }; SetPoster __set_poster; @@ -2486,10 +2916,52 @@ fvar, #endif + + void p_float_ite(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { + ite(s, s.arg2BoolVar(ce[0]), s.arg2FloatVar(ce[1]), s.arg2FloatVar(ce[2]), + s.arg2FloatVar(ce[3])); + } + void p_float_pow(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { + pow(s, s.arg2FloatVar(ce[0]), ce[1]->getInt(), s.arg2FloatVar(ce[2])); + } + void p_float_array_min(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { + min(s, s.arg2floatvarargs(ce[0]), s.arg2FloatVar(ce[1])); + } + void p_float_array_max(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { + max(s, s.arg2floatvarargs(ce[0]), s.arg2FloatVar(ce[1])); + } +#ifdef GECODE_HAS_MPFR + void p_float_pow_base(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { + pow(s, ce[0]->getFloat(), s.arg2FloatVar(ce[1]), s.arg2FloatVar(ce[2])); + } +#endif + + void p_float_rel_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { + FloatRelType r; + switch (ce[1]->getInt()) { + case 1: r = FRT_EQ; break; + case 2: r = FRT_NQ; break; + case 3: r = FRT_LQ; break; + case 4: r = FRT_LE; break; + case 5: r = FRT_GQ; break; + case 6: r = FRT_GR; break; + default: throw FlatZinc::Error("Registry", "invalid float relation"); + } + rel(s, s.arg2FloatVar(ce[0]), r, s.arg2FloatVar(ce[2]), + Reify(s.arg2BoolVar(ce[3]), RM_IMP)); + } + class FloatPoster { public: FloatPoster(void) { registry().add("int2float",&p_int2float); + + registry().add("gecode_float_rel_imp_fzn", &p_float_rel_imp); + registry().add("gecode_float_ite", &p_float_ite); + registry().add("gecode_float_pow", &p_float_pow); + registry().add("gecode_float_array_min", &p_float_array_min); + registry().add("gecode_float_array_max", &p_float_array_max); + registry().add("float_abs",&p_float_abs); registry().add("float_sqrt",&p_float_sqrt); registry().add("float_eq",&p_float_eq); @@ -2513,6 +2985,7 @@ fvar, registry().add("float_lin_lt_reif",&p_float_lin_lt_reif); #ifdef GECODE_HAS_MPFR + registry().add("gecode_float_pow_base", &p_float_pow_base); registry().add("float_acos",&p_float_acos); registry().add("float_asin",&p_float_asin); registry().add("float_atan",&p_float_atan); diff --git a/gecode/float/transcendental/exp-log.hpp b/gecode/float/transcendental/exp-log.hpp index 1ff43f0460..82eef89ace 100755 --- a/gecode/float/transcendental/exp-log.hpp +++ b/gecode/float/transcendental/exp-log.hpp @@ -31,8 +31,61 @@ * */ +#include + namespace Gecode { namespace Float { namespace Transcendental { + // Round endpoints explicitly; compiler optimizations can ignore changes to + // the hardware rounding mode. + forceinline FloatVal + fixed_base_pow(FloatNum base, const FloatVal& exponent) { + mpfr_t b, x, y; + mpfr_init2(b, std::numeric_limits::digits); + mpfr_init2(x, std::numeric_limits::digits); + mpfr_init2(y, std::numeric_limits::digits); + mpfr_set_d(b, base, GMP_RNDN); + mpfr_set_d(x, base > 1.0 ? exponent.min() : exponent.max(), GMP_RNDN); + mpfr_pow(y, b, x, GMP_RNDD); + FloatNum lower = mpfr_get_d(y, GMP_RNDD); + mpfr_set_d(x, base > 1.0 ? exponent.max() : exponent.min(), GMP_RNDN); + mpfr_pow(y, b, x, GMP_RNDU); + FloatNum upper = mpfr_get_d(y, GMP_RNDU); + mpfr_clear(b); + mpfr_clear(x); + mpfr_clear(y); + return FloatVal(lower, upper); + } + + forceinline FloatVal + fixed_base_log(FloatNum base, const FloatVal& value) { + FloatVal numerator = log(value); + FloatVal denominator = log(FloatVal(base)); + const FloatNum n[] = {numerator.min(), numerator.max()}; + const FloatNum d[] = {denominator.min(), denominator.max()}; + FloatNum lower = std::numeric_limits::infinity(); + FloatNum upper = -lower; + mpfr_t x, y, q; + mpfr_init2(x, std::numeric_limits::digits); + mpfr_init2(y, std::numeric_limits::digits); + mpfr_init2(q, std::numeric_limits::digits); + // log(base) does not contain zero. Divide all four endpoint pairs with + // outward rounding, including when 0 < base < 1. + for (int i=0; i<2; i++) { + mpfr_set_d(x, n[i], GMP_RNDN); + for (int j=0; j<2; j++) { + mpfr_set_d(y, d[j], GMP_RNDN); + mpfr_div(q, x, y, GMP_RNDD); + lower = std::min(lower, mpfr_get_d(q, GMP_RNDD)); + mpfr_div(q, x, y, GMP_RNDU); + upper = std::max(upper, mpfr_get_d(q, GMP_RNDU)); + } + } + mpfr_clear(x); + mpfr_clear(y); + mpfr_clear(q); + return FloatVal(lower, upper); + } + /* * Bounds consistent exponential operator * @@ -97,16 +150,16 @@ namespace Gecode { namespace Float { namespace Transcendental { ExecStatus Pow::post(Home home, FloatNum base, A x0, B x1) { if (base <= 0) return ES_FAILED; - if (x0 == x1) { - GECODE_ME_CHECK(x0.eq(home,0.0)); - } else { - GECODE_ME_CHECK(x1.gq(home,0.0)); - if (x1.max() == 0.0) - return ES_FAILED; - GECODE_ME_CHECK(x0.eq(home,log(x1.domain())/log(base))); - GECODE_ME_CHECK(x1.eq(home,exp(x0.domain()*log(base)))); - (void) new (home) Pow(home,base,x0,x1); + if (base == 1.0) { + GECODE_ME_CHECK(x1.eq(home,1.0)); + return ES_OK; } + GECODE_ME_CHECK(x1.gq(home,0.0)); + if (x1.max() == 0.0) + return ES_FAILED; + GECODE_ME_CHECK(x0.eq(home,fixed_base_log(base,x1.domain()))); + GECODE_ME_CHECK(x1.eq(home,fixed_base_pow(base,x0.domain()))); + (void) new (home) Pow(home,base,x0,x1); return ES_OK; } @@ -127,9 +180,9 @@ namespace Gecode { namespace Float { namespace Transcendental { Pow::propagate(Space& home, const ModEventDelta&) { if (x1.max() == 0.0) return ES_FAILED; - GECODE_ME_CHECK(x0.eq(home,log(x1.domain())/log(base))); - GECODE_ME_CHECK(x1.eq(home,exp(x0.domain()*log(base)))); - return x0.assigned() ? home.ES_SUBSUMED(*this) : ES_FIX; + GECODE_ME_CHECK(x0.eq(home,fixed_base_log(base,x1.domain()))); + GECODE_ME_CHECK(x1.eq(home,fixed_base_pow(base,x0.domain()))); + return x0.assigned() ? home.ES_SUBSUMED(*this) : ES_NOFIX; } }}} diff --git a/test/flatzinc/native-registry.cpp b/test/flatzinc/native-registry.cpp new file mode 100644 index 0000000000..3b2599ca58 --- /dev/null +++ b/test/flatzinc/native-registry.cpp @@ -0,0 +1,111 @@ +/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */ +/* + * Main authors: + * Mikael Zayenz Lagerkvist + * + * Copyright: + * Mikael Zayenz Lagerkvist, 2026 + * + * This file is part of Gecode, the generic constraint + * development environment: + * http://www.gecode.dev + * + * Permission is hereby granted, free of charge, to any person obtaining + * a copy of this software and associated documentation files (the + * "Software"), to deal in the Software without restriction, including + * without limitation the rights to use, copy, modify, merge, publish, + * distribute, sublicense, and/or sell copies of the Software, and to + * permit persons to whom the Software is furnished to do so, subject to + * the following conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE + * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION + * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION + * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + */ + +#include "test/flatzinc.hh" +#include + +namespace Test { namespace FlatZinc { + namespace { + // Annotations preserve both consistency and algorithm flags. + class AlgorithmAnnotations : public Base { + public: + AlgorithmAnnotations(void) + : Base("FlatZinc::NativeRegistry::AlgorithmAnnotations") {} + virtual bool run(void) { + const char* names[] = {"gecode_basic_propagation", + "gecode_advanced_propagation", "gecode_full_propagation"}; + const Gecode::IntPropLevel levels[] = { + Gecode::IPL_BASIC, Gecode::IPL_ADVANCED, Gecode::IPL_FULL + }; + for (int i=0; i<3; i++) { + Gecode::FlatZinc::FlatZincSpace space; + Gecode::FlatZinc::AST::Array ann; + ann.a.push_back(new Gecode::FlatZinc::AST::Atom(names[i])); + ann.a.push_back(new Gecode::FlatZinc::AST::Atom("domain")); + if (space.ann2ipl(&ann) != (Gecode::IPL_DOM | levels[i])) + return false; + } + return true; + } + } algorithm_annotations; + + class Create { + public: + Create(void) { + const std::string sat = "----------\n"; + const std::string unsat = "=====UNSATISFIABLE=====\n"; + (void) new FlatZincTest("NativeRegistry::DistanceShared", + "var 0..2:x; constraint gecode_inter_distance([x,x],1); solve satisfy;", unsat); + (void) new FlatZincTest("NativeRegistry::DistanceNegativeEmpty", + "constraint gecode_inter_distance_fzn([],-1); solve satisfy;", unsat); + (void) new FlatZincTest("NativeRegistry::DistanceNegativeSingleton", + "constraint gecode_inter_distance_fzn([0],-1); solve satisfy;", unsat); + (void) new FlatZincTest("NativeRegistry::NotAllEqual", + "constraint gecode_not_all_equal_int([1,1,2]); solve satisfy;", sat); + (void) new FlatZincTest("NativeRegistry::CardinalityHoles", + "var {0,3}: count; constraint gecode_global_cardinality_closed([1,1],[1],[count]); solve satisfy;", unsat); + (void) new FlatZincTest("NativeRegistry::SortOrientation", + "constraint gecode_sort_permutation([3,1,2],[1,2,3],[2,3,1],1); solve satisfy;", unsat); + (void) new FlatZincTest("NativeRegistry::ArgMinShared", + "var 1..2:x; constraint gecode_arg_min_int([x,x],1,x,false); solve satisfy;", sat); + (void) new FlatZincTest("NativeRegistry::InvalidModulusReification", + "constraint gecode_product_mod_var_fzn_reif([3],0,3,false); solve satisfy;", sat); + (void) new FlatZincTest("NativeRegistry::MinimumDistanceRepeatedSite", + "constraint gecode_minimum_distance_fzn([0,0,2],3,[0,2,4,2,0,3,4,3,0],1); solve satisfy;", unsat); + (void) new FlatZincTest("NativeRegistry::NondeterministicPrefix", + "constraint gecode_regular_nfa_int_fzn([0,1],3,0,2,[{1,2},{},{},{3},{},{}],1,{3}); solve satisfy;", sat); + (void) new FlatZincErrorTest("NativeRegistry::SortSize", + "constraint gecode_sort_permutation([1,2],[1],[1,2],1); solve satisfy;", + {}, "sort arrays must have equal lengths"); +#ifdef GECODE_HAS_SET_VARS + (void) new FlatZincTest("NativeRegistry::SetSequenceEmpty", + "constraint gecode_array_set_seq([]); solve satisfy;", sat); + (void) new FlatZincTest("NativeRegistry::SetSequenceEmptyUnion", + "constraint gecode_array_set_seq_union([],{1}); solve satisfy;", unsat); + (void) new FlatZincTest("NativeRegistry::AtmostOneSingletonCardinality", + "constraint gecode_set_atmost_one([{1}],2); solve satisfy;", unsat); + (void) new FlatZincTest("NativeRegistry::AtmostOneUnitCardinality", + "constraint gecode_set_atmost_one([{1},{1}],1); solve satisfy;", sat); + (void) new FlatZincErrorTest("NativeRegistry::SetMatrixSize", + "constraint gecode_set_element2d([{1}],0,0,0,1,{1}); solve satisfy;", + {}, "invalid set matrix dimensions"); + (void) new FlatZincTest("NativeRegistry::EmptySetMinReification", + "constraint gecode_set_min_reif({},1,false); solve satisfy;", sat); +#endif + } + }; + Create c; + } +}} + +// STATISTICS: test-flatzinc diff --git a/test/float/transcendental.cpp b/test/float/transcendental.cpp index 0445017139..70ee8703a5 100644 --- a/test/float/transcendental.cpp +++ b/test/float/transcendental.cpp @@ -46,6 +46,64 @@ namespace Test { namespace Float { /// %Tests for transcendental constraints namespace Transcendental { + /// Exact fixed-base powers, inverse logarithms, and shared variables + class PowBaseConsistency : public Test { + protected: + Gecode::FloatNum base; + Gecode::FloatNum input; + Gecode::FloatNum output; + bool logarithm; + bool shared; + bool expected; + public: + PowBaseConsistency(Gecode::FloatNum b, Gecode::FloatNum x, + Gecode::FloatNum y, bool log, bool share, bool valid) + : Test("Transcendental::PowBaseConsistency::"+str(b)+"::"+ + str(x)+"::"+str(y)+(log ? "::Log" : "::Pow")+ + (share ? "::Shared" : "::Separate"), + share ? 1 : 2,-4.0,8.0,1.0,CPLT_ASSIGNMENT,false), + base(b), input(x), output(y), logarithm(log), shared(share), + expected(valid) { + testsearch = false; + } + /// Check one exact example through the standard posting/assignment tests + virtual Assignment* assignment(void) const { + Assignment* a = new RandomAssignment(arity,dom,1,_rand); + a->set(0,input); + if (!shared) + a->set(1,output); + return a; + } + /// Exact expected results avoid checking exp/log against itself + virtual MaybeType solution(const Assignment&) const { + return expected ? MT_TRUE : MT_FALSE; + } + virtual void post(Gecode::Space& home, Gecode::FloatVarArray& x) { + Gecode::FloatVar y = shared ? x[0] : x[1]; + if (!shared) + Gecode::rel(home,y,Gecode::FRT_GQ,0.0); + if (logarithm) + Gecode::log(home,base,y,x[0]); + else + Gecode::pow(home,base,x[0],y); + } + }; + + /// Register the exact powers and their logarithmic forms + class PowBaseExamples { + public: + PowBaseExamples(void) { + for (int logarithm=0; logarithm<2; logarithm++) { + (void) new PowBaseConsistency(2.0,3.0,8.0,logarithm,false,true); + (void) new PowBaseConsistency(2.0,3.0,7.0,logarithm,false,false); + (void) new PowBaseConsistency(0.5,3.0,0.125,logarithm,false,true); + (void) new PowBaseConsistency(1.0,3.0,1.0,logarithm,false,true); + (void) new PowBaseConsistency(2.0,0.0,0.0,logarithm,true,false); + (void) new PowBaseConsistency(0.25,0.5,0.5,logarithm,true,true); + } + } + } pow_base_examples; + /// %Test for exponent constraint class ExpXY : public Test { public: @@ -190,7 +248,7 @@ namespace Test { namespace Float { virtual MaybeType solution(const Assignment& x) const { if ((x[0].max() <= 0.0) || (base <= 0.0)) return MT_FALSE; - return eq(log(x[0]) / log(base), x[1]); + return eq(log(x[0]) / log(Gecode::FloatVal(base)), x[1]); } /// Post constraint on \a x virtual void post(Gecode::Space& home, Gecode::FloatVarArray& x) { @@ -209,13 +267,13 @@ namespace Test { namespace Float { virtual MaybeType solution(const Assignment& x) const { if ((x[0].max() <= 0.0) || (base <= 0.0)) return MT_FALSE; - return eq(log(x[0]) / log(base), x[1]); + return eq(log(x[0]) / log(Gecode::FloatVal(base)), x[1]); } /// Extend assignment \a x virtual bool extendAssignment(Assignment& x) const { if ((x[0].max() <= 0.0) || (base <= 0.0)) return false; - Gecode::FloatVal d = log(x[0])/log(base); + Gecode::FloatVal d = log(x[0])/log(Gecode::FloatVal(base)); if (Gecode::Float::subset(d, dom)) { x.set(1, d); return true; @@ -240,7 +298,7 @@ namespace Test { namespace Float { virtual MaybeType solution(const Assignment& x) const { if ((x[0].max() <= 0.0) || (base <= 0.0)) return MT_FALSE; - return eq(log(x[0]) / log(base), x[0]); + return eq(log(x[0]) / log(Gecode::FloatVal(base)), x[0]); } /// Post constraint on \a x virtual void post(Gecode::Space& home, Gecode::FloatVarArray& x) { @@ -259,7 +317,7 @@ namespace Test { namespace Float { virtual MaybeType solution(const Assignment& x) const { if (base <= 0.0) return MT_FALSE; - return eq(exp(x[0] * log(base)), x[1]); + return eq(exp(x[0] * log(Gecode::FloatVal(base))), x[1]); } /// Post constraint on \a x virtual void post(Gecode::Space& home, Gecode::FloatVarArray& x) { @@ -278,12 +336,12 @@ namespace Test { namespace Float { virtual MaybeType solution(const Assignment& x) const { if (base <= 0.0) return MT_FALSE; - return eq(exp(x[0] * log(base)), x[1]); + return eq(exp(x[0] * log(Gecode::FloatVal(base))), x[1]); } /// Extend assignment \a x virtual bool extendAssignment(Assignment& x) const { if (base <= 0.0) return false; - Gecode::FloatVal d = exp(x[0]*log(base)); + Gecode::FloatVal d = exp(x[0]*log(Gecode::FloatVal(base))); if (Gecode::Float::subset(d, dom)) { x.set(1, d); return true; @@ -312,7 +370,7 @@ namespace Test { namespace Float { virtual MaybeType solution(const Assignment& x) const { if ((x[0].max() <= 0.0) || (base <= 0.0)) return MT_FALSE; - return eq(exp(x[0] * log(base)), x[0]); + return eq(exp(x[0] * log(Gecode::FloatVal(base))), x[0]); } /// Post constraint on \a x virtual void post(Gecode::Space& home, Gecode::FloatVarArray& x) {