/* 

  Grocery problem in Picat using bv module.
  
  Ported from the Gecode example
  """
  A kid goes into a grocery store and buys four items. The cashier
  charges $7.11, the kid pays and is about to leave when the cashier
  calls the kid back, and says "Hold on, I multiplied the four items
  instead of adding them; I'll try again; Hah, with adding them the
  price still comes to $7.11". What were the prices of the four items?

  The model is taken from: Christian Schulte, Gert Smolka, Finite Domain
  Constraint Programming in Oz. A Tutorial. 2001.
  Available from: http://www.mozart-oz.org/documentation/fdt/
  """

  This model uses the bv module.

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

*/

import sat.
import bv_utils.

main => go.

/*
  [120,125,150,316]

  CPU time 0.575 seconds. Backtracks: 0

*/
go =>
  nolog,
  {A,B,C,D}=make_bv_array(4,0,711),
  L = [A,B,C,D],
  A.bv_mul(B).bv_mul(C).bv_mul(D).bv_eq(711*100**3),
  A.bv_add(B).bv_add(C).bv_add(D).bv_eq(711),
  A.bv_le(B),
  B.bv_le(C),
  C.bv_le(D),
  solve(L),
  println(L.bti),
  fail,

  nl.

/*
  Using bv_prod/2 and bv_sum/2.
  This is quite slower (probably due to bv_prod/2)

  [120,125,150,316]

  CPU time 1.617 seconds. Backtracks: 0

*/
go2 ?=>
  nolog,
  G = 711,
  X = make_bv_array(4,0,G),
  bv_sum(X.to_list).bv_eq(G),
  bv_prod(X.to_list).bv_eq(G*100**3),  
  bv_increasing(X),
  solve(X),
  println(X.bti),
  fail,
  nl.
go2 => true.