1:- module(seq, []). 2
3:- use_module(library(apply)). 4:- use_module(library(apply_macros)). 5:- use_module(pac(basic)). 6:- use_module(pac(meta)). 7:- use_module(util(misc)). 8:- use_module(zdd('zdd-array')). 9:- use_module(zdd(zdd)). 10:- use_module(pac(op)). 11
12:-op(1150, fy, seq_zdd). 13
14:-meta_predicate seq_zdd(:). 15seq_zdd(X):- zdd((set_compare(seq:seq_compare), seq:X)).
16
23
31
37
43
44seq_prove(X):- fetch_state(S),
45 set_compare(seq:seq_compare, S),
46 zdd_singleton(-X, X0, S),
47 resolve(X0, S).
48
50formula(I, I, I==J):-!, J is I+1.
51formula(I, J, I==P):- K is I + 1, formula(K, J, P).
52
55conj(I, I, I):-!.
56conj(I, J, I*P):- I0 is I + 1, conj(I0, J, P).
57
59seq_compare(=, X, X):-!.
60seq_compare(C, ==(X, Y), ==(U, V)):-!, seq_compare(C, X, Y, U, V).
61seq_compare(C, ->(X, Y), ->(U, V)):-!, seq_compare(C, X, Y, U, V).
62seq_compare(C, +(X, Y), +(U, V)):-!, seq_compare(C, X, Y, U, V).
63seq_compare(C, *(X, Y), *(U, V)):-!, seq_compare(C, X, Y, U, V).
64seq_compare(C, xor(X, Y), xor(U, V)):-!, seq_compare(C, X, Y, U, V).
65seq_compare(<, ==(_, _), _):-!.
66seq_compare(>, _, ==(_, _)):-!.
67seq_compare(<, ->(_, _), _):-!.
68seq_compare(>, _, ->(_, _)):-!.
69seq_compare(<, xor(_, _), _):-!.
70seq_compare(>, _, xor(_, _)):-!.
71seq_compare(<, *(_, _), _) :-!.
72seq_compare(>, _, *(_, _)) :-!.
73seq_compare(<, +(_, _), _) :-!.
74seq_compare(>, _, +(_, _)) :-!.
75seq_compare(C, -(X), -(Y)) :-!, seq_compare(C, X, Y).
76seq_compare(C, X, -(Y)) :-!,
77 ( X = Y -> C = (<)
78 ; seq_compare(C, X, Y)
79 ).
80seq_compare(C, -(X), Y):-!,
81 ( X = Y -> C = (>)
82 ; seq_compare(C, X, Y)
83 ).
84seq_compare(C, X, Y):- compare(C, X, Y).
85
87seq_compare(C, X, Y, U, V):-
88 seq_compare(C0, X, U),
89 ( C0 = (=) -> seq_compare(C, Y, V)
90 ; C = C0
91 ).
92
93 96
97resolve(X, S):- zdd_has_1(X, S), !. 98resolve(X, S):- X > 1,
99 cofact(X, t(A, L, R), S),
100 resolve(A, L, R, X0, S),
101 resolve(X0, S).
102
106resolve(-(-A), L, R, X0, S):-!, resolve(A, L, R, X0, S).
107resolve(A, L, R, X0, S):- L>1,
108 cofact(L, t(B, L0, R0), S),
109 B = -A,
110 !,
111 ltr_merge(R, R0, R1, S),
112 ltr_join(L0, R1, X0, S).
113resolve(A0 == A1, L, R, X0, S):-!, resolve((A0->A1)*(A1->A0), L, R, X0, S).
118resolve(A0 -> A1, L, R, X0, S):-!, resolve(-A0+A1, L, R, X0, S).
122
123resolve(A0 + A1, L, R, X0, S):-!,
124 zdd_insert_atoms([A0, A1], R, R0, S),
125 ltr_join(L, R0, X0, S).
126resolve(A0 * A1, L, R, X0, S):-!,
127 ltr_insert(A0, R, R0, S),
128 ltr_insert(A1, R, R1, S),
129 ltr_join_list([R0, R1], L, X0, S).
130resolve(xor(A0, A1), L, R, X0, S):-!, resolve(-A0*A1 + A0*(-A1), L, R, X0, S).
131resolve(-(A), L, R, X0, S):- deMorgan(A, M), !,
132 resolve(M, L, R, X0, S).
133resolve(-(_), L, _, L, _):-!. 134resolve(_, 0, _, 0, _):-!. 135resolve(A, L, R, X0, S):- 136 cofact(L, t(B, U, V), S),
137 ( B = -(A) ->
138 ltr_merge(V, R, M, S), 139 ltr_join(U, M, X0, S) 140 ; X0 = L 141 ).
143deMorgan(A0 == A1, -A0*A1 + A0 * -A1).
144deMorgan(A0 -> A1, A0 * -A1).
145deMorgan(A0 + A1, -A0 * -A1).
146deMorgan(A0 * A1, -A0 + -A1)