/* 

  Three consecutive numbers problem in Picat.

  https://mindyourdecisions.com/blog/2017/11/12/the-three-consecutive-numbers-puzzle/
  """
  This problem was created by Ken Edwards.

  I have found three consecutive integers such that their product is equal to their sum.
  
  What could my numbers be? Solve for all possibilities.
  """

  There are three solutions:
   [-3,-2,-1]
   [1,2,3]
   [-1,0,1]

  Without the domain, CP takes a long time to prove that there are only
  three solutions since it checks the full domain of
   -2**56..2**56

  Times for go/0 and go2/0:

  * Without any domain for X:
    SMT: 185s and 0.170s
    SAT: 2.1s and 3.5s
    CP: Finds the 3 solutions directly but then takes "forever" to check
        if there are any other solutions.

  * With a domain of -100..100 for X:
    CP: 0.036s and 0.036s
    SAT: 0.070s and 0.047s
    SMT: 0.185 and 0.182s

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

*/

import smt.

main => go.

go =>
  N = 3,
  X = new_list(N),
  % X :: -100..100, % for cp
  foreach(I in 2..N)
    X[I] #= X[I-1] + 1   
  end,
  all_different(X),
  sum(X) #= prod(X),

  solve($[ff,updown],[X]),  
  println(X),
  fail,

  nl.

% alternative version
go2 =>
  % X :: -100..100, % for cp
  (X-1)+X+(X+1) #= (X-1)*X*(X+1),
  solve($[degree,updown],[X]),
  println([X-1,X,X+1]),
  fail,
  nl.