e5f4633c39
which included commits to RCS files with non-trunk default branches. git-svn-id: https://yap.svn.sf.net/svnroot/yap/trunk@5 b08c6af1-5177-4d33-ba66-4b1c6b8b522a
176 lines
4.9 KiB
Plaintext
176 lines
4.9 KiB
Plaintext
|
|
/*
|
|
**********************************************************************
|
|
*
|
|
* CLP(R) Version 2.0 (Example Programs Release)
|
|
* (C) Copyright, March 1986, Monash University
|
|
*
|
|
**********************************************************************
|
|
*/
|
|
|
|
%
|
|
% Convert a propositional formula into disjunctive normal form.
|
|
% There are 15 goals ?- go1 to ?- go 15.
|
|
% The goal ?- go5 is the most substantial.
|
|
%
|
|
|
|
literal(z0).
|
|
literal(z1).
|
|
literal(z2).
|
|
literal(z3).
|
|
literal(z4).
|
|
literal(z5).
|
|
literal(z6).
|
|
literal(z7).
|
|
literal(z8).
|
|
literal(z9).
|
|
literal(n(X)) :- literal(X).
|
|
|
|
/*---------------------------------------------- base cases ------------------*/
|
|
|
|
norm(X, X) :- literal(X).
|
|
norm(o(X, Y), o(X, Y)) :- literal(X), literal(Y).
|
|
norm(a(X, Y), a(X, Y)) :- literal(X), literal(Y).
|
|
|
|
/*---------------------------------------------- OR cases --------------------*/
|
|
|
|
norm(o(X, Y), o(X1, Y)) :-
|
|
literal(Y),
|
|
norm(X, X1).
|
|
norm(o(X, o(Y, Z)), W) :-
|
|
norm(o(o(X, Y), Z), W).
|
|
norm(o(X, a(Y1, Y2)), o(X1, Y12)) :-
|
|
norm(X, X1),
|
|
norm(a(Y1, Y2), Y12).
|
|
|
|
/*---------------------------------------------- AND cases -------------------*/
|
|
|
|
norm(a(X, Y), a(X1, Y)) :-
|
|
literal(Y),
|
|
norm(X, X1).
|
|
norm(a(X, a(Y, Z)), W) :-
|
|
norm(a(a(X, Y), Z), W).
|
|
norm(a(X, o(Y1, Y2)), a(X1, Y12)) :-
|
|
norm(X, X1),
|
|
norm(o(Y1, Y2), Y12).
|
|
|
|
/*----------------------------------------------------------------------------*/
|
|
/*----------------------------------------------------------------------------*/
|
|
/*---------------------------------------------- base cases ------------------*/
|
|
|
|
dnf(X, X) :- literal(X).
|
|
dnf(o(X, Y), o(X, Y)) :- literal(X), literal(Y).
|
|
dnf(a(X, Y), a(X, Y)) :- literal(X), literal(Y).
|
|
|
|
/*---------------------------------------------- compaction ------------------*/
|
|
|
|
dnf(n(n(X)), W) :- dnf(X, W).
|
|
dnf(n(o(X, Y)), W) :- dnf(a(n(X), n(Y)), W).
|
|
dnf(n(a(X, Y)), W) :- dnf(o(n(X), n(Y)), W).
|
|
|
|
/*----------------------------------------------------------------------------*/
|
|
|
|
dnf(o(X, Y), W) :-
|
|
dnf(X, X1),
|
|
dnf(Y, Y1),
|
|
norm(o(X1, Y1), W).
|
|
dnf(a(X, Y), a(a(X1, X2), Y)) :-
|
|
literal(Y),
|
|
dnf(X, a(X1, X2)).
|
|
dnf(a(X, Y), a(a(Y1, Y2), X)) :-
|
|
literal(X),
|
|
dnf(Y, a(Y1, Y2)).
|
|
dnf(a(X, Y), W) :-
|
|
dnf(X, a(X1, X2)),
|
|
dnf(Y, a(Y1, Y2)),
|
|
norm(a(a(X1, X2), a(Y1, Y2)), W).
|
|
dnf(a(X, Y), W) :-
|
|
dnf(X, o(X1, X2)),
|
|
dnf(Y, Y1),
|
|
dnf(o(a(X1, Y1), a(X2, Y1)), W).
|
|
dnf(a(X, Y), W) :-
|
|
dnf(X, X1),
|
|
dnf(Y, o(Y1, Y2)),
|
|
dnf(o(a(X1, Y1), a(X1, Y2)), W).
|
|
|
|
go1:- dnf(a(z1, a(z2, o(z3, a(z4, a(z5, z6))))), X),
|
|
printf("%\n", [X]).
|
|
go2:- dnf(o(o(z1,o(z2,o(z3,z4))),o(z5,o(z6,o(z7,z8)))),X),
|
|
printf("%\n", [X]).
|
|
go3:- dnf(o(o(a(z1,z2),z3),o(a(z4,a(a(z5,z6),z7)),o(z8,z9))),X),
|
|
printf("%\n", [X]).
|
|
go4:- dnf(a(a(z1,a(o(z2,z3),z4)),a(z5,o(z6,z7))),X),
|
|
printf("%\n", [X]).
|
|
go5:- dnf(n(o(a(n(o(z1,z2)),n(a(z3,z4))),a(n(z5),o(a(z6,a(z7,z8)),z9)))),X),
|
|
dnf(n(o(a(n(o(z1,z2)),n(a(z3,z4))),a(n(z5),o(a(z6,a(z7,z8)),z9)))),X),
|
|
printf("%\n", [X]).
|
|
go6:- dnf(n(a(z1,a(z2,z3))),X),
|
|
printf("%\n", [X]).
|
|
go7:- dnf(a(a(o(z1,z2),z3),z4),X),
|
|
printf("%\n", [X]).
|
|
go8:- dnf(o(a(z1,z2),a(z3,z4)),X),
|
|
printf("%\n", [X]).
|
|
go9:- dnf(a(o(z1,z2),o(z3,z4)),X),
|
|
printf("%\n", [X]).
|
|
go10:- dnf(o(a(o(z1,z2),a(z3,z4)),z5),X),
|
|
printf("%\n", [X]).
|
|
go11:- dnf(o(o(z1,o(z3,o(z4,a(z4,z5)))),z5),X),
|
|
printf("%\n", [X]).
|
|
go12:- dnf(o(z1,o(z2,o(z3,z4))),X),
|
|
printf("%\n", [X]).
|
|
go13:- dnf(o(a(z1,z2),n(o(z2,a(z3,z4)))),X),
|
|
printf("%\n", [X]).
|
|
go14:- dnf(o(a(n(z0),n(z1)),a(n(z0),n(z2))),X),
|
|
printf("%\n", [X]).
|
|
go15:- dnf(o(n(a(z1,z2)),a(o(a(o(z1,z2),z3),z4),z5)),X),
|
|
printf("%\n", [X]).
|
|
|
|
% Answers:
|
|
% 1 ?- go1.
|
|
% o(a(a(z2, z3), z1), a(a(a(a(z5, z6), z4), z2), z1))
|
|
%
|
|
% 2 ?- go2.
|
|
% o(o(o(o(o(o(o(z1, z2), z3), z4), z5), z6), z7), z8)
|
|
%
|
|
% 3 ?- go3.
|
|
% o(o(o(o(a(z1, z2), z3), a(a(a(z5, z6), z7), z4)), z8), z9)
|
|
%
|
|
% 4 ?- go4.
|
|
% o(o(o(a(a(a(a(z2, z4), z1), z5), z6), a(a(a(a(z2, z4), z1), z5), z7)), a(a(a(a(z3, z4), z1), z5), z6)), a(a(a(a(z3, z4), z1), z5), z7))
|
|
%
|
|
% 5 ?- go5.
|
|
% o(o(o(o(o(o(o(o(o(o(o(a(z1, n(n(z5))), a(a(n(z6), n(z9)), z1)), a(a(n(z7), n(z9)), z1)), a(a(n(z8), n(z9)), z1)), a(z2, n(n(z5)))), a(a(n(z6), n(z9)), z2)), a(a(n(z7), n(z9)), z2)), a(a(n(z8), n(z9)), z2)), a(a(z3, z4), n(n(z5)))), a(a(a(z3, z4), n(z6)), n(z9))), a(a(a(z3, z4), n(z7)), n(z9))), a(a(a(z3, z4), n(z8)), n(z9)))
|
|
%
|
|
% 6 ?- go6.
|
|
% o(o(n(z1), n(z2)), n(z3))
|
|
%
|
|
% 7 ?- go7.
|
|
% o(a(a(z1, z3), z4), a(a(z2, z3), z4))
|
|
%
|
|
% 8 ?- go8.
|
|
% o(a(z1, z2), a(z3, z4))
|
|
%
|
|
% 9 ?- go9.
|
|
% o(o(o(a(z1, z3), a(z1, z4)), a(z2, z3)), a(z2, z4))
|
|
%
|
|
% 10 ?- go10.
|
|
% o(o(a(a(z3, z4), z1), a(a(z3, z4), z2)), z5)
|
|
%
|
|
% 11 ?- go11.
|
|
% o(o(o(o(z1, z3), z4), a(z4, z5)), z5)
|
|
%
|
|
% 12 ?- go12.
|
|
% o(o(o(z1, z2), z3), z4)
|
|
%
|
|
% 13 ?- go13.
|
|
% o(o(a(z1, z2), a(n(z2), n(z3))), a(n(z2), n(z4)))
|
|
%
|
|
% 14 ?- go14.
|
|
% o(a(n(z0), n(z1)), a(n(z0), n(z2)))
|
|
%
|
|
% 15 ?- go15.
|
|
% o(o(o(o(n(z1), n(z2)), a(a(z1, z3), z5)), a(a(z2, z3), z5)), a(z4, z5))
|
|
%
|
|
|
|
?- printf("\n>>> Sample goals: go1/0, ..., go15/0\n", []).
|