;; lib/minikanren/tests/clpfd-bounds.sx — Phase 6 piece B: bounds-consistency
;; for fd-plus and fd-times in the partial- and all-domain cases.
;;
;; We probe domains directly (peek at the FD store) before any labelling
;; happens. This isolates the propagator's narrowing behaviour from the
;; search engine.

(define
  probe-dom
  (fn
    (goal var-key)
    (let
      ((s (first (stream-take 1 (goal empty-s)))))
      (cond ((= s nil) :no-subst) (:else (fd-domain-of s var-key))))))

;; --- fd-plus partial-domain narrowing ---

(mk-test
  "fd-plus-vvn-narrows-x"
  (let
    ((x (mk-var "x")) (y (mk-var "y")))
    (probe-dom
      (mk-conj
        (fd-in
          x
          (list
            1
            2
            3
            4
            5
            6
            7
            8
            9
            10))
        (fd-in y (list 1 2 3))
        (fd-plus x y 10))
      "x"))
  (list 7 8 9))

(mk-test
  "fd-plus-vvn-narrows-y"
  (let
    ((x (mk-var "x")) (y (mk-var "y")))
    (probe-dom
      (mk-conj
        (fd-in
          x
          (list
            1
            2
            3
            4
            5
            6
            7
            8
            9
            10))
        (fd-in y (list 1 2 3))
        (fd-plus x y 10))
      "y"))
  (list 1 2 3))

(mk-test
  "fd-plus-nvv-narrows"
  (let
    ((y (mk-var "y")) (z (mk-var "z")))
    (probe-dom
      (mk-conj
        (fd-in y (list 1 2 3))
        (fd-in
          z
          (list
            1
            2
            3
            4
            5
            6
            7
            8
            9
            10
            11
            12
            13
            14
            15
            16
            17
            18
            19
            20))
        (fd-plus 5 y z))
      "z"))
  (list 6 7 8))

(mk-test
  "fd-plus-vvv-narrows-z"
  (let
    ((x (mk-var "x")) (y (mk-var "y")) (z (mk-var "z")))
    (probe-dom
      (mk-conj
        (fd-in x (list 1 2 3))
        (fd-in y (list 1 2 3))
        (fd-in
          z
          (list
            1
            2
            3
            4
            5
            6
            7
            8
            9
            10
            11
            12
            13
            14
            15
            16
            17
            18
            19
            20))
        (fd-plus x y z))
      "z"))
  (list 2 3 4 5 6))

(mk-test
  "fd-plus-vvv-narrows-x"
  (let
    ((x (mk-var "x")) (y (mk-var "y")) (z (mk-var "z")))
    (probe-dom
      (mk-conj
        (fd-in
          x
          (list
            1
            2
            3
            4
            5
            6
            7
            8
            9
            10))
        (fd-in y (list 1 2 3))
        (fd-in z (list 5 6 7))
        (fd-plus x y z))
      "x"))
  (list 2 3 4 5 6))

;; --- fd-times partial-domain narrowing (positive domains) ---

(mk-test
  "fd-times-vvn-narrows"
  (let
    ((x (mk-var "x")) (y (mk-var "y")))
    (probe-dom
      (mk-conj
        (fd-in
          x
          (list
            1
            2
            3
            4
            5
            6))
        (fd-in
          y
          (list
            1
            2
            3
            4
            5
            6))
        (fd-times x y 12))
      "x"))
  (list 2 3 4 5 6))

(mk-test
  "fd-times-nvv-narrows"
  (let
    ((y (mk-var "y")) (z (mk-var "z")))
    (probe-dom
      (mk-conj
        (fd-in y (list 1 2 3 4))
        (fd-in
          z
          (list
            1
            2
            3
            4
            5
            6
            7
            8
            9
            10
            11
            12
            13
            14
            15
            16
            17
            18
            19
            20))
        (fd-times 3 y z))
      "z"))
  (list
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12))

(mk-test
  "fd-times-vvv-narrows"
  (let
    ((x (mk-var "x")) (y (mk-var "y")) (z (mk-var "z")))
    (probe-dom
      (mk-conj
        (fd-in x (list 1 2 3))
        (fd-in y (list 1 2 3))
        (fd-in
          z
          (list
            1
            2
            3
            4
            5
            6
            7
            8
            9
            10
            11
            12
            13
            14
            15
            16
            17
            18
            19
            20))
        (fd-times x y z))
      "z"))
  (list
    1
    2
    3
    4
    5
    6
    7
    8
    9))

;; --- bounds force impossible branches to fail early ---

(mk-test
  "fd-plus-impossible-via-bounds"
  (let
    ((x (mk-var "x")) (y (mk-var "y")))
    (probe-dom
      (mk-conj
        (fd-in
          x
          (list
            1
            2
            3
            4
            5
            6
            7
            8
            9
            10))
        (fd-in
          y
          (list
            1
            2
            3
            4
            5
            6
            7
            8
            9
            10))
        (fd-plus x y 100))
      "x"))
  :no-subst)

(mk-tests-run!)