/usr/share/Yap/cnf.pl is in yap 6.2.2-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 | %%============================================================================
%% CNF.pl
%% Convertor of Boolean formulae to CNF
%% Copyright (c) 2006, Michael Codish, Vitaly Lagoon, and Peter J. Stuckey
%%
%% Permission is hereby granted, free of charge, to any person obtaining a
%% copy of this software and associated documentation files (the
%% "Software"), to deal in the Software without restriction, including
%% without limitation the rights to use, copy, modify, merge, publish,
%% distribute, sublicense, and/or sell copies of the Software, and to
%% permit persons to whom the Software is furnished to do so, subject to
%% the following conditions:
%%
%% The above copyright notice and this permission notice shall be included
%% in all copies or substantial portions of the Software.
%%
%% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
%% OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
%% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
%% NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
%% LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
%% OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
%% WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
:- module(cnf,[cnf/2,cnf_dl/2]).
cnf(F,Cnf) :- cnf_dl(F,Cnf-[]).
cnf_dl(F,[[B]|Cnf1]-Cnf2) :- iff(F,+,B,Cnf2,Cnf1).
iff(V,_,B,Acc,Cnf) :- var(V), !, V=B, Cnf=Acc.
iff(1,_,B,Acc,Cnf) :- !, B=1, Cnf=Acc.
iff(0,_,B,Acc,Cnf) :- !, B=0, Cnf=Acc.
iff(-X,+,B,Acc,Cnf) :- !, iff(X,-,BX,Acc,Cnf), neglit(BX,B).
iff(-X,-,B,Acc,Cnf) :- !, iff(X,+,BX,Acc,Cnf), neglit(BX,B).
iff(-X,*,B,Acc,Cnf) :- !, iff(X,*,BX,Acc,Cnf), neglit(BX,B).
iff((X+Y),Polarity,B,Acc,Cnf) :- !,
iff(X,Polarity,BX,Acc,AccX),
iff(Y,Polarity,BY,AccX,AccXY),
(
Polarity == + -> Cnf = [[-B,BX,BY]|AccXY]
;
Polarity == - -> Cnf = [[B,-BX],[B,-BY]|AccXY]
;
Cnf = [[-B,BX,BY], [B,-BX], [B,-BY] | AccXY]
).
iff((X*Y),Polarity,B,Acc,Cnf) :- !,
iff(X,Polarity,BX,Acc,AccX),
iff(Y,Polarity,BY,AccX,AccXY),
(
Polarity == + -> Cnf = [[-B,BX],[-B,BY]|AccXY]
;
Polarity == - -> Cnf = [[B,-BX,-BY]|AccXY]
;
Cnf = [[B,-BX,-BY], [-B,BX], [-B,BY] | AccXY]
).
iff((X==Y),Polarity,B,Acc,Cnf) :- !,
iff(X,*,BX,Acc,AccX),
iff(Y,*,BY,AccX,AccXY),
(
Polarity == + -> Cnf = [[-BX,BY,-B],[BX,-BY,-B] | AccXY]
;
Polarity == - -> Cnf = [[-BX,-BY,B],[BX,BY,B] | AccXY]
;
Cnf = [[-BX,BY,-B],[BX,-BY,-B],[-BX,-BY,B],[BX,BY,B] | AccXY]
).
iff((X xor Y),Polarity,B,Acc,Cnf) :- !,
iff(X,*,BX,Acc,AccX),
iff(Y,*,BY,AccX,AccXY),
(
Polarity == + -> Cnf = [[-BX,-BY,-B],[BX,BY,-B] | AccXY]
;
Polarity == - -> Cnf = [[-BX,BY,B],[BX,-BY,B] | AccXY]
;
Cnf = [[-BX,BY,B],[BX,-BY,B],[-BX,-BY,-B],[BX,BY,-B] | AccXY]
).
iff((X->Y;Z),Polarity,B,Acc,Cnf) :- !,
iff(X,*,BX,Acc,AccX),
iff(Y,Polarity,BY,AccX,AccXY),
iff(Z,Polarity,BZ,AccXY,AccXYZ),
(
Polarity == + -> Cnf = [[-BX,BY,-B],[BX,BZ,-B],[BY,BZ,-B]|AccXYZ]
;
Polarity == - -> Cnf = [[-BX,-BY,B],[BX,-BZ,B],[-BY,-BZ,B]|AccXYZ]
;
Cnf = [[-BX,BY,-B], [BX,BZ,-B], [BY,BZ,-B],
[-BX,-BY,B], [BX,-BZ,B], [-BY,-BZ,B] | AccXYZ]
).
neglit(V,-V) :- var(V), !.
neglit(-V,V).
neglit(0,1).
neglit(1,0).
|