使用 clpfd 生成闰年序列

Question

下面的代码检查给定年份是否为闰年。该算术是使用库clpfd 中的声明性整数算术制定的，以便可以“反向”运行查询以生成闰年序列。代码有两个变体，改变了年份是否为世纪的测试，但每个变体的行为不同，并且它们都不能正常工作。

我想生成从 1990 年到 2005 年的闰年序列。为此，我输入查询 Year in 1990..2005,leap_year1(Year),indomain(Year).（或 leap_year2 以测试第二个变体）。

我写的代码是（使用 SWI-Prolog 8.0.2）：

:- use_module(library(clpfd)).

leap_year1(Year) :-
  Year #> 0,
  Year mod 4 #= 0,
  (
    Year mod 100 #= 0 ->
      Year mod 400 #= 0      % 2000 is a leap year, 1900 is not
    ;
      true                   % Not a century
  ).

leap_year2(Year) :-
  Year #> 0,
  Year mod 4 #= 0,
  (
    Year mod 100 #\= 0 ->
      true                   % Not a century
    ;
      Year mod 400 #= 0      % 2000 is a leap year, 1900 is not
  ).

查询结果为 (SWI-Prolog 8.0.2)：

?- Year in 1990..2005,leap_year1(Year),indomain(Year).
Year = 2000.

?- Year in 1990..2005,leap_year2(Year),indomain(Year).
Year = 1992 ;
Year = 1996 ;
Year = 2004.

如您所见，这两个查询都没有正确生成完整的闰年序列（1992、1996、2000、2004）。

此外，1900 年左右的以下查询也会产生异常结果（添加了 cmets）：

% Verify that 1900 is not a leap year
?- not(leap_year1(1900)), not(leap_year2(1900)).
true.

% Verify that 1892, 1896, 1904 are leap years
?- leap_year1(1892), leap_year1(1896), leap_year1(1904).
true.

?- leap_year2(1892), leap_year2(1896), leap_year2(1904).
true.

% No solutions found (!)
?- Year in 1890..1905,leap_year1(Year),indomain(Year).
false.

% Solutions found as expected (complete result)
?- Year in 1890..1905,leap_year2(Year),indomain(Year).
Year = 1892 ;
Year = 1896 ;
Year = 1904.

对这种行为有解释吗？我应该如何修改leap_year() 使其生成完整的序列？

更新：（更多？）完成，但不明白为什么（！）

拆分几个世纪的检查提高了查询的完整性：

leap_year_century_fix(Year) :-
  Year mod 100 #\= 0.

leap_year_century_fix(Year) :-
  Year mod 100 #= 0,
  Year mod 400 #= 0.      % 2000 is a leap year, 1900 is not

leap_year3(Year) :-
  Year #> 0,
  Year mod 4 #= 0,
  leap_year_century_fix(Year).

现在：

?- Year in 1890..1905,leap_year3(Year),indomain(Year).
Year = 1892 ;
Year = 1896 ;
Year = 1904 ;
false.

?- Year in 1990..2015,leap_year3(Year),indomain(Year).
Year = 1992 ;
Year = 1996 ;
Year = 2004 ;
Year = 2008 ;
Year = 2012 ;
Year = 2000.

Answer 1

简单地用and和or来表达，reification表示or：

leap(Y) :-
    Y #> 0,
    Y mod 4 #= 0,
    (Y mod 100 #\= 0) #\/ (Y mod 400 #= 0).