使用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年的查询也会生成异常结果(添加注释)：

% 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

简单地使用和以及或来表示它，并使用或的具体化

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