This file is indexed.

/usr/share/Yap/cnf.pl is in yap 6.2.2-6+b2.

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).