(* CTM Chapter #12 Examples in Alice ML *)
import structure Space from "x-alice:/lib/gecode/Space"
import structure FS from "x-alice:/lib/gecode/FS"
import structure FD from "x-alice:/lib/gecode/FD"
import structure Search from "x-alice:/lib/gecode/Search"
import structure Linear from "x-alice:/lib/gecode/Linear"
import structure Explorer from "x-alice:/lib/tools/Explorer";

(* syntactic sugar for solutions using promises/futures *)
open Linear
open Promise
open Future
infix 3 ?=
val op?= = fulfill
val ? = future

(* convert term to intvar *)
fun term2intvar (FD(x)) = x
  | term2intvar _ = raise Domain

(* convert int to intvar *)
fun int2intvar (sp, x) = FD.intvar(sp, #[(x,x)])

(* 12.1.2 Propagate-and-search - Calculating with partial information *)
fun partial sp =
   let
      val x = fdterm(sp, [90 `# 110])
      val y = fdterm(sp, [48 `# 53])
      val a = fdterm(sp, [0 `# 10000])
   in
      (* Alice currently only supports linear expressions. Will be
         generalized for non-linear expressions in the next release. *)
      (* post (sp, x `* y `= a, FD.DOM); *)
      FD.mult (sp, term2intvar(x), term2intvar(y), term2intvar(a), FD.DOM);
      post (sp, a `> `4000, FD.DOM);
      post (sp, x `- `2 `* y `= `11, FD.DOM);
      branch (sp, #[a, x, y], FD.B_SIZE_MIN, FD.B_MIN);
      {a, x, y}
   end;
Explorer.exploreAll partial;
val sol = Search.searchAll partial

(* another way to do the same thing *)
fun partial2 sp =
   let
      val x = FD.intvar(sp, #[(90,110)])
      val y = FD.intvar(sp, #[(48,53)])
      val a = FD.intvar(sp, #[(0,10000)])
   in
      FD.mult (sp, x, y, a, FD.DOM);
      post (sp, FD(a) `> `4000, FD.DOM);
      post (sp, FD(x) `- `2 `* FD(y) `= `11, FD.DOM);
      FD.branch (sp, #[x, y], FD.B_SIZE_MIN, FD.B_MIN);
      {x,y}
   end;
Explorer.exploreAll partial2;

(* 12.1.4 Propagate-and-search - Executing the example *)
fun rectangle sp =
   let
      val v as #[x, y] = fdtermVec (sp, 2, [0 `# 9])
      val a = FD.intvar(sp, #[(0,10000)])             (* needed for workaround *)
   in
      (* post (sp, x `* y `= `24, FD.DOM); *)
      FD.mult (sp, term2intvar(x), term2intvar(y), a, FD.DOM);
      post (sp, FD(a) `= `24, FD.DOM);
      post (sp, x `+ y `= `10, FD.DOM);
      post (sp, x `< y, FD.DOM);
      branch (sp, #[x, y], FD.B_SIZE_MIN, FD.B_MIN);
      {x, y}
   end;
Explorer.exploreAll rectangle;

(* 12.2.1 Programming techniques - Calculting with partial information *)

(* Note: this comes straight out of the Alice documentation *)
fun money sp =
   let
      val v as #[s, e, n, d, m, o', r, y] = Linear.fdtermVec (sp, 8, [0 `# 9])
   in
      distinct (sp, v, FD.BND);
      post (sp, s `<> `0, FD.BND);
      post (sp, m `<> `0, FD.BND);
      post (sp, `1000`*s `+ `100`*e  `+ `10`*n `+ d `+
                `1000`*m `+ `100`*o' `+ `10`*r `+ e `=
               `10000`*m `+ `1000`*o' `+ `100`*n `+ `10`*e `+ y, FD.BND);
      branch (sp, v, FD.B_SIZE_MIN, FD.B_MIN);
      {s,e,n,d,m,o',r,y}
   end;
Explorer.exploreAll money;

(* 12.2.2 Programming techniques - Palindrome products revisited *)
fun palindrome sp =
   let
      val a = FD.intvar(sp, #[(0,999999)])
      val b = FD.intvar(sp, #[(0,999)])
      val c = FD.intvar(sp, #[(0,999)])
      val x = FD.intvar(sp, #[(0,9)])
      val y = FD.intvar(sp, #[(0,9)])
      val z = FD.intvar(sp, #[(0,9)])
   in
      (* post (sp, FD(a) `= FD(b) `* FD(c), FD.DOM); *)
      FD.mult (sp, b, c, a, FD.DOM);
      post (sp, FD(a) `= (FD(x) `* `100000) `+
                         (FD(y) `* `10000) `+
                         (FD(z) `* `1000) `+
                         (FD(z) `* `100) `+
                         (FD(y) `* `10) `+
                         FD(x), FD.DOM);
      post (sp, FD(a) `> `100000, FD.DOM);
      branch (sp, #[FD(x),FD(y),FD(z),FD(b),FD(c)], FD.B_SIZE_MIN, FD.B_MIN);
      {a,x,y}
   end;
Explorer.exploreOne palindrome;