;; lib/minikanren/tests/clpfd-ord.sx — fd-lt / fd-lte / fd-eq. ;; --- fd-lt --- (mk-test "fd-lt-narrows-x-against-num" (run* q (fresh (x) (fd-in x (list 1 2 3 4 5)) (fd-lt x 3) (fd-label (list x)) (== q x))) (list 1 2)) (mk-test "fd-lt-narrows-x-against-num-symmetric" (run* q (fresh (x) (fd-in x (list 1 2 3 4 5)) (fd-lt 3 x) (fd-label (list x)) (== q x))) (list 4 5)) (mk-test "fd-lt-pair-ordered" (let ((res (run* q (fresh (x y) (fd-in x (list 1 2 3 4)) (fd-in y (list 1 2 3 4)) (fd-lt x y) (fd-label (list x y)) (== q (list x y)))))) (= (len res) 6)) true) (mk-test "fd-lt-impossible-fails" (run* q (fresh (x) (fd-in x (list 5 6 7)) (fd-lt x 3) (fd-label (list x)) (== q x))) (list)) ;; --- fd-lte --- (mk-test "fd-lte-includes-equal" (run* q (fresh (x) (fd-in x (list 1 2 3 4 5)) (fd-lte x 3) (fd-label (list x)) (== q x))) (list 1 2 3)) (mk-test "fd-lte-equal-bound" (run* q (fresh (x) (fd-in x (list 1 2 3 4 5)) (fd-lte 3 x) (fd-label (list x)) (== q x))) (list 3 4 5)) ;; --- fd-eq --- (mk-test "fd-eq-bind" (run* q (fresh (x) (fd-in x (list 1 2 3 4 5)) (fd-eq x 3) (== q x))) (list 3)) (mk-test "fd-eq-out-of-domain-fails" (run* q (fresh (x) (fd-in x (list 1 2 3)) (fd-eq x 5) (== q x))) (list)) (mk-test "fd-eq-two-vars-share-domain" (run* q (fresh (x y) (fd-in x (list 1 2 3)) (fd-in y (list 2 3 4)) (fd-eq x y) (fd-label (list x y)) (== q (list x y)))) (list (list 2 2) (list 3 3))) ;; --- combine fd-lt + fd-neq for "between" puzzle --- (mk-test "fd-lt-neq-combined" (run* q (fresh (x y z) (fd-in x (list 1 2 3)) (fd-in y (list 1 2 3)) (fd-in z (list 1 2 3)) (fd-lt x y) (fd-lt y z) (fd-label (list x y z)) (== q (list x y z)))) (list (list 1 2 3))) (mk-tests-run!)