/*

  Curious numbers in Picat using bv module.

  """
  Curious Numbers from "Amusements in Mathematics, Dudeney", number 114.

  The number 48 has this peculiarity, that if you add 1 to it the result
  is a square number, and if you add 1 to its half, you also get a
  square number. Now, there is no limit to the numbers that have this
  peculiarity, and it is an interesting puzzle to find three more of
  them---the smallest possible numbers. What are they?
  """ 

  This model uses the bv module.

  The least such numbers are: 
  [
   [48,49,7,24,25,5],
   [1680,1681,41,840,841,29],
   [57120,57121,239,28560,28561,169], 
   [1940448,1940449,1393,970224,970225,985]
  ]


  Model created by Hakan Kjellerstrand, hakank@gmail.com
  See also my Picat page: http://www.hakank.org/picat/

*/

import sat.
import bv_utils.

main => go.

go ?=>
   nolog,
   curious(_X),
   fail,
   nl.
go => true.


curious(LD) =>
  % LD = make_bv_array(6,1,2000000),
  LD = make_bv_array(6,32),
  LD = {X,A,B,C,D,E},

  X.bv_gt(0),
  % X + 1 #= A, % if you add 1 to it
  X.bv_add(1).bv_eq(A),
  
  % A #= B * B, % the result is a square number
  B.bv_mul(B).bv_eq(A),
  
  % X #= 2 * C, % if you to its half
  % C.bv_mul(2).bv_eq(X),
  C.bv_add(C).bv_eq(X),
  
  % C + 1 #= D, % add 1
  C.bv_add(1).bv_eq(D),
  
  % D #= E * E, % you also get a square number
  E.bv_mul(E).bv_eq(D),
  solve(LD),
  println(LD.bti).