-
Notifications
You must be signed in to change notification settings - Fork 8
/
Copy pathtabling-tests.scm
108 lines (100 loc) · 3.46 KB
/
tabling-tests.scm
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
(load "mk.scm")
(load "tabling.scm")
(load "z3-driver.scm")
(load "test-check.scm")
;; some tests inspired by
;; https://github.com/webyrd/tabling
(test "path-tabled"
(letrec ((arc (lambda (x y)
(conde
((== x 'a) (== y 'b))
((== x 'b) (== y 'a))
((== x 'b) (== y 'd)))))
(path (tabled (x y)
(conde
((arc x y))
((fresh (z)
(arc x z)
(path z y)))))))
(run* (q)
(path 'a q)))
'(b a d))
(test "facto-7"
(letrec ((facto (tabled (n out)
(conde
((z/assert `(= ,n 0))
(z/assert `(= ,out 1)))
((z/assert `(not (= ,n 0)))
(fresh (n-1 r)
(z/assert `(= (- ,n 1) ,n-1))
(z/assert `(= (* ,n ,r) ,out))
(facto n-1 r)))))))
(run 7 (q)
(fresh (n out)
(facto n out)
(== q `(,n ,out)))))
'((0 1) (1 1) (2 2) (3 6) (4 24) (5 120) (6 720)))
(test "facto-backwards-2"
(letrec ((facto (tabled (n out)
(conde
((z/assert `(= ,n 0))
(z/assert `(= ,out 1)))
((z/assert `(not (= ,n 0)))
(fresh (n-1 r)
(z/assert `(= (- ,n 1) ,n-1))
(z/assert `(= (* ,n ,r) ,out))
(facto n-1 r)))))))
(run* (q)
(facto q 2)))
'(2))
(test "facto-backwards-720"
(letrec ((facto (tabled (n out)
(conde
((z/assert `(= ,n 0))
(z/assert `(= ,out 1)))
((z/assert `(not (= ,n 0)))
(fresh (n-1 r)
(z/assert `(= (- ,n 1) ,n-1))
(z/assert `(= (* ,n ,r) ,out))
(facto n-1 r)))))))
(run* (q)
(facto q 720)))
'(6))
(test "fibo-1-non-tabled"
(letrec ((fibo (lambda (n out)
(conde
((z/assert `(= ,n 0))
(z/assert `(= ,out 0)))
((z/assert `(= ,n 1))
(z/assert `(= ,out 1)))
((z/assert `(> ,n 1))
(fresh (n-1 n-2 r1 r2)
(z/assert `(= (- ,n 1) ,n-1))
(z/assert `(= (- ,n 2) ,n-2))
(z/assert `(= (+ ,r1 ,r2) ,out))
(fibo n-1 r1)
(fibo n-2 r2)))))))
(run 7 (q)
(fresh (n out)
(fibo n out)
(== q `(,n ,out)))))
'((0 0) (1 1) (2 1) (3 2) (4 3) (5 5) (6 8)))
(test "fibo-1-tabled"
(letrec ((fibo (tabled (n out)
(conde
((z/assert `(= ,n 0))
(z/assert `(= ,out 0)))
((z/assert `(= ,n 1))
(z/assert `(= ,out 1)))
((z/assert `(> ,n 1))
(fresh (n-1 n-2 r1 r2)
(z/assert `(= (- ,n 1) ,n-1))
(z/assert `(= (- ,n 2) ,n-2))
(fibo n-1 r1)
(fibo n-2 r2)
(z/assert `(= (+ ,r1 ,r2) ,out))))))))
(run 7 (q)
(fresh (n out)
(fibo n out)
(== q `(,n ,out)))))
'((0 0) (1 1) (2 1) (3 2) (4 3) (5 5) (6 8)))