% ----------------------------------------------------------------------
% $Id: clnf.red,v 1.15 2003/05/31 14:40:58 lasaruk Exp $
% ----------------------------------------------------------------------
% Copyright (c) 1995-1999 Andreas Dolzmann and Thomas Sturm
% ----------------------------------------------------------------------
% $Log: clnf.red,v $
% Revision 1.15 2003/05/31 14:40:58 lasaruk
% cl_renamevars modified to work with bounded quantifiers.
%
% Revision 1.14 2003/04/15 14:07:41 seidl
% Checked Lasaruk's changes, fixed issue in rl_nnf1 (don't negate bounds).
%
% Revision 1.13 2003/04/14 10:13:38 lasaruk
% Negation normal form, cl_flip and cl_apply2ats changed to work with
% new introduced bounded quantifiers. All changes are bracketed by %
% /LASARUK and % /END_LASARUK. Any other changes in code should be dismissed.
%
% Revision 1.12 2002/08/23 08:44:18 dolzmann
% Minor code cosmetic.
%
% Revision 1.11 1999/04/13 13:10:58 sturm
% Updated comments for exported procedures.
%
% Revision 1.10 1999/03/22 17:08:07 dolzmann
% Changed copyright information.
%
% Revision 1.9 1999/03/19 16:07:17 dolzmann
% Fixed a bug in cl_tnf: cl_tnff and cl_tnft call rl_t2cdl instead of
% ofsf_t2cdl.
%
% Revision 1.8 1997/08/14 10:09:16 sturm
% Added documentation for cl_rename!-vars.
%
% Revision 1.7 1996/10/17 13:51:54 sturm
% Introduced services rlvarl, rlfvarl, and rlbvarl. Renamed cl_varl to
% cl_varl1 for this.
%
% Revision 1.6 1996/10/07 11:45:51 sturm
% Added fluids for CVS and copyright information.
%
% Revision 1.5 1996/10/02 10:24:06 dolzmann
% Fixed a bug in cl_tnft.
%
% Revision 1.4 1996/10/01 10:24:54 reiske
% Introduced new service rltnf and related code.
%
% Revision 1.3 1996/07/07 14:35:37 sturm
% Turned some cl calls into service calls.
% Introduced new service rl_nnfnot.
%
% Revision 1.2 1996/06/05 15:06:40 sturm
% Added procedure cl_varl as an entry point for cl_varl1.
%
% Revision 1.1 1996/03/22 10:31:30 sturm
% Moved and split.
%
% ----------------------------------------------------------------------
lisp <<
fluid '(cl_nf_rcsid!* cl_nf_copyright!*);
cl_nf_rcsid!* := "$Id: clnf.red,v 1.15 2003/05/31 14:40:58 lasaruk Exp $";
cl_nf_copyright!* := "(c) 1995-1999 by A. Dolzmann and T. Sturm"
>>;
module clnf;
% Common logic normal forms. Submodule of [cl].
procedure cl_expand!-extbool(f);
% Common logic expand extended boolean operators. [f] is a formula.
% Returns a formula equivalent to [f] that does not contain any
% extended boolean operator.
begin scalar op;
op := rl_op f;
if rl_quap op then
return rl_mkq(op,rl_var f,cl_expand!-extbool(
rl_mat f));
if rl_basbp op then
return rl_mkn(op,for each subf in rl_argn f collect
cl_expand!-extbool(subf));
if op eq 'impl then
return cl_expand!-extbool(rl_mk2('or,
rl_mk1('not,rl_arg2l f),rl_arg2r f));
if op eq 'repl then
return cl_expand!-extbool(rl_mk2('or,
rl_arg2l f,rl_mk1('not,rl_arg2r f)));
if op eq 'equiv then
return cl_expand!-extbool(rl_mkn('and,{
rl_mk2('impl,rl_arg2l f,rl_arg2r f),
rl_mk2('repl,rl_arg2l f,rl_arg2r
f)}));
return f;
end;
procedure cl_nnf(f);
% Common logic negation normal form. [f] is a formula. Returns a
% formula equivalent to [f] that does not contain the operator
% [not].
cl_nnf1(f,T);
procedure cl_nnfnot(f);
% Common logic negation normal form not. [f] is a formula. Returns
% a formula equivalent to $\lnot [f]$ that does not contain the
% operator [not].
cl_nnf1(f,nil);
procedure cl_nnf1(f,flag);
% Common logic negation normal form. [f] is a formula; [flag] is
% bool. Returns a formula $\phi$ that does not contain the operator
% [not]. In case $[flag]$ is non-[nil] we have $\phi$ equivalent to
% [f], else we have $\phi$ equivalent to $\lnot [f]$.
begin scalar op;
op := rl_op f;
if op eq 'not then
return cl_nnf1(rl_arg1 f,not flag);
if op eq 'impl then
return rl_mkn(cl_cflip('or,flag),
{cl_nnf1(rl_arg2l f,not flag),cl_nnf1(rl_arg2r f,flag)});
if op eq 'repl then
return rl_mkn(cl_cflip('or,flag),
{cl_nnf1(rl_arg2l f,flag),cl_nnf1(rl_arg2r f,not flag)});
if op eq 'equiv then
return rl_mkn(cl_cflip('or,flag),{
rl_mkn(cl_cflip('and,flag),{
cl_nnf1(rl_arg2l f,flag),cl_nnf1(rl_arg2r f,flag)}),
rl_mkn(cl_cflip('and,flag),{
cl_nnf1(rl_arg2l f,not flag),cl_nnf1(rl_arg2r f,not flag)})});
if rl_tvalp op then
return cl_cflip(f,flag);
if rl_quap op then
return rl_mkq(cl_cflip(op,flag),rl_var f,cl_nnf1(rl_mat f,flag));
if rl_bquap op then % don't flip within bound
return rl_mkbq(cl_cflip(op,flag),rl_var f,cl_nnf1(rl_b f,t),
cl_nnf1(rl_mat f,flag));
if rl_junctp op then
return rl_mkn(
cl_cflip(op,flag),for each subf in rl_argn f collect
cl_nnf1(subf,flag));
return if flag then f else rl_negateat f
end;
procedure cl_pnf(phi);
% Common logic prenex normal form. [phi] is a formula. Returns a
% prenex formula equivalent to [phi]. The number of quantifier
% changes in the result is minimal among all formulas that can be
% obtained from [phi] by moving quantifiers to the outside.
cl_pnf1 rl_nnf phi;
procedure cl_pnf1(phi);
% Common logic prenex normal form subroutine. [phi] is a positive
% formula that does not contain any extended boolean operator.
% Returns a prenex formula equivalent to [phi]. The number of
% quantifier changes in the result is minimal among all formulas
% that can be obtained from [phi] by moving quantifiers to the
% outside.
<<
if null cdr erg or cl_qb car erg < cl_qb cadr erg then
car erg
else
cadr erg
>> where erg=cl_pnf2(cl_rename!-vars(phi));
procedure cl_pnf2(phi);
begin scalar op;
op := rl_op phi;
if rl_quap op then
return cl_pnf2!-quantifier(phi);
if rl_junctp op then
return cl_pnf2!-junctor(phi);
if rl_tvalp op then
return {phi};
if rl_cxp op then
rederr{"cl_pnf2():",op,"invalid as operator"};
return {phi}
end;
procedure cl_pnf2!-quantifier(phi);
<<
if (null cdr e) or (rl_op phi eq rl_op car e) then
{rl_mkq(rl_op phi,rl_var phi,car e)}
else
{rl_mkq(rl_op phi,rl_var phi,cadr e)}
>> where e=cl_pnf2 rl_mat phi;
procedure cl_pnf2!-junctor(phi);
begin scalar junctor,e,l1,l2,onlyex,onlyall,phi1,phi2; integer m,qb;
junctor := rl_op phi;
e := for each f in rl_argn phi collect cl_pnf2(f);
onlyex := T; onlyall := T;
for each ej in e do <<
qb := cl_qb car ej;
if qb > m then <<
m := qb; onlyex := T; onlyall := T
>>;
if cdr ej then <<
l1 := (car ej) . l1;
l2 := (cadr ej) . l2
>> else <<
l1 := (car ej) . l1;
l2 := (car ej) . l2
>>;
if eqn(m,qb) then <<
if rl_op car l1 eq 'all then onlyex := nil;
if rl_op car l2 eq 'ex then onlyall := nil
>>;
>>;
l1 := reversip l1;
l2 := reversip l2;
if eqn(m,0) then return {phi};
if onlyex neq onlyall then
if onlyex then
return {cl_interchange(l1,junctor,'ex)}
else % [onlyall]
return {cl_interchange(l2,junctor,'all)};
phi1 := cl_interchange(l1,junctor,'ex);
phi2 := cl_interchange(l2,junctor,'all);
if car phi1 eq car phi2 then
return {phi1}
else
return {phi1,phi2}
end;
procedure cl_qb(phi);
begin scalar q,scan!-q; integer qb;
while rl_quap(scan!-q := rl_op phi) do <<
if scan!-q neq q then <<
qb := qb + 1;
q := scan!-q
>>;
phi := rl_mat phi
>>;
return qb
end;
procedure cl_interchange(l,junctor,a);
begin scalar ql,b,result;
while cl_contains!-quantifier(l) do <<
l := for each f in l collect <<
while rl_op f eq a do <<
b := (rl_var f) . b;
f := rl_mat f
>>;
f
>>;
ql := b . ql;
b := nil;
a := cl_flip a
>>;
a := cl_flip a;
result := rl_mkn(junctor,l);
for each b in ql do <<
for each v in b do result := rl_mkq(a,v,result);
a := cl_flip a
>>;
return result
end;
procedure cl_contains!-quantifier(l);
l and (rl_quap rl_op car l or cl_contains!-quantifier(cdr l));
procedure cl_rename!-vars(f);
% Common logic rename variables. [f] is a formula. Returns an
% equivalent formula in which each quantified variable is unique,
% i.e., occurs neither boundly or freely elsewhere in [f].
car cl_rename!-vars1(f,cl_replace!-varl f);
procedure cl_replace!-varl(f);
begin scalar a,d,all,replace;
<< a := car vl1; d := cdr vl1 >>
where vl1=cl_varl1 f;
all := a;
for each x on d do <<
if car x memq cdr x or car x memq a then
replace := lto_insert((car x) . 0,replace);
all := lto_insert(car x,all)
>>;
return all . replace
end;
procedure cl_fvarl(f);
% Common logic free variable list. [f] is a formula. Returns the
% list of variables occurring freely in [f] sorted wrt. [ordp].
sort(cl_fvarl1 f,'ordp);
procedure cl_fvarl1(f);
% Common logic free variable list subroutine. [f] is a formula.
% Returns the list of variables occurring freely in [f].
car cl_varl1 f;
procedure cl_bvarl(f);
% Common logic bound variable list. [f] is a formula. Returns the
% list of variables occurring boundly in [f] sorted wrt. [ordp].
sort(cl_bvarl1 f,'ordp);
procedure cl_bvarl1(f);
% Common logic bound variable list subroutine. [f] is a formula.
% Returns the list of variables occurring boundly in [f].
cdr cl_varl1 f;
procedure cl_varl(f);
% Common logic variable lists. [f] is a formula. Returns a pair
% $(V_f . V_b)$ of variable lists. $V_f$ contains the variables
% occurring freely in [f], and $V_b$ contains the variables
% occurring boundly in [f]. Both lists are sorted wrt. the current
% kernel order [ordp].
(sort(car w,'ordp) . sort(cdr w,'ordp)) where w = cl_varl1 f;
procedure cl_varl1(f);
% Common logic variable lists. [f] is a formula. Returns a pair
% $(V_f . V_b)$ of variable lists. $V_f$ contains the variables
% occurring freely in [f], and $V_b$ contains the variables
% occurring boundly in [f].
cl_varl2(f,nil,nil,nil);
procedure cl_varl2(f,freevl,cboundvl,boundvl);
begin scalar op;
op := rl_op f;
if rl_tvalp op then
return freevl . boundvl;
if rl_boolp op then <<
for each s in rl_argn f do <<
freevl := car vl;
boundvl := cdr vl
>> where vl=cl_varl2(s,freevl,cboundvl,boundvl);
return freevl . boundvl
>>;
if rl_quap op then
return cl_varl2(rl_mat f,freevl,
lto_insertq(rl_var f,cboundvl),rl_var f . boundvl);
% /LASARUK
if rl_bquap op then
return cl_varl2(rl_mat f,freevl,
lto_insertq(rl_var f,cboundvl),rl_var f . boundvl);
% /LASARUK
% [f] is an atomic formula.
for each v in rl_varlat f do
if not (v memq cboundvl) then freevl := lto_insertq(v,freevl);
return freevl . boundvl
end;
procedure cl_rename!-vars1(f,vl);
begin scalar op,h,w,newid;
op := rl_op f;
if rl_boolp op then
return rl_mkn(op,for each x in cdr f collect <<
vl := cdr rnv;
car rnv
>> where rnv=cl_rename!-vars1(x,vl)) . vl;
if rl_quap op then <<
<< h := car rnv; vl := cdr rnv >>
where rnv=cl_rename!-vars1(rl_mat f,vl);
if (w := assoc(cadr f,cdr vl)) then <<
repeat <<
newid := mkid(car w,cdr w);
cdr w := cdr w + 1
>> until not (newid memq car vl or get(newid,'avalue));
car vl := lto_insertq(newid,car vl);
return rl_mkq(op,newid,cl_apply2ats1(
h,'rl_varsubstat,{newid,car w})) . vl
>>;
return rl_mkq(op,rl_var f,h) . vl
>>;
% /LASARUK
if rl_bquap op then <<
<< h := car rnv; vl := cdr rnv >>
where rnv=cl_rename!-vars1(rl_mat f,vl);
if (w := assoc(rl_var f,cdr vl)) then <<
repeat <<
newid := mkid(car w,cdr w);
cdr w := cdr w + 1
>> until not (newid memq car vl or get(newid,'avalue));
car vl := lto_insertq(newid,car vl);
return rl_mkbq(op, newid,
cl_apply2ats1(rl_b f, 'rl_varsubstat, {newid, car w}),
cl_apply2ats1(h,'rl_varsubstat, {newid, car w})) . vl
>>;
return rl_mkbq(op,rl_var f,rl_b f, h) . vl
>>;
% /LASARUK
% [f] is a truth value or an atomic formula.
return f . vl;
end;
procedure cl_apnf(phi);
% Common logic anti-prenex normal form. [phi] is a positive
% formula. Returns a positive formula equivalent to [phi], where
% all quantifiers are moved to the inside as far as possible.
begin scalar op;
op := rl_op phi;
if op eq 'ex then
return cl_apnf1(rl_var phi,cl_apnf rl_mat phi);
if op eq 'all then
return rl_nnfnot cl_apnf1(rl_var phi,cl_apnf rl_mat rl_nnfnot phi);
if rl_junctp op then
return rl_mkn(op,for each subf in rl_argn phi collect cl_apnf subf);
% [phi] is atomic.
return phi
end;
procedure cl_apnf1(var,phi);
% Common logic anti-prenex normal form subroutine. [var] is a
% variable. [phi] is a positive formula with all quantifiers
% already moved to the inside as far as possible. Returns a
% positive formula equivalent to [phi] with the existentially
% quantified [var] moved to the inside as far as possible.
begin scalar op,nf,occurl,noccurl;
op := rl_op phi;
if rl_tvalp op then
return phi;
if op eq 'ex then
return rl_mkq('ex,rl_var phi,cl_apnf1(var,rl_mat phi));
if op eq 'all then
return if cl_freevp(var,phi) then
rl_mkq('ex,var,phi)
else
phi;
if op eq 'or then <<
nf := for each subf in rl_argn phi collect cl_apnf1(var,subf);
return rl_mkn('or,nf)
>>;
if op eq 'and then <<
for each subf in rl_argn phi do
if cl_freevp(var,subf) then
occurl := subf . occurl
else
noccurl := subf . noccurl;
if occurl then <<
nf := if cdr occurl then
rl_mkq('ex,var,rl_mkn('and,reversip occurl))
else
cl_apnf1(var,car occurl);
noccurl := nf . noccurl
>>;
return rl_smkn('and,reversip noccurl)
>>;
% [phi] is atomic.
if var memq rl_varlat phi then
return rl_mkq('ex,var,phi);
return phi
end;
procedure cl_freevp(var,phi);
% Common logic free variable predicate. [var] is a variable, [phi]
% is a formula. Returns non-[nil] iff [var] occurs freely in [phi].
begin scalar argl,flag;
if rl_quap rl_op phi then <<
if var eq rl_var phi then
return nil;
return cl_freevp(var,rl_mat phi)
>>;
if cl_atfp phi then
return var memq rl_varlat phi;
argl := rl_argn phi;
while argl do
if cl_freevp(var,car argl) then <<
flag := T;
argl := nil
>> else
argl := cdr argl;
return flag
end;
procedure cl_tnf(f,terml);
% Common logic tree normal form. [f] is a formula, [terml] is a
% list of terms. Returns a big formula. Depends on the switch
% [rltnft].
if !*rltnft then cl_tnft(f,terml) else cl_tnff(f,terml);
procedure cl_tnff(f,terml);
% Common logic tree normal form flat. [f] is a formula, [terml] is
% a list of terms. Returns a big formula.
begin scalar w,theol,resl,dpth;
theol := cl_bnf!-cartprod for each term in terml collect
rl_t2cdl term;
if !*rlverbose then dpth := length theol;
for each theo in theol do <<
if !*rlverbose then <<
ioto_prin2 {"[",dpth};
dpth := dpth - 1
>>;
w := rl_simpl(f,theo,-1);
if w eq 'true then <<
resl := rl_smkn('and,theo) . resl;
if !*rlverbose then ioto_prin2 "+] "
>> else if w eq 'inctheo then
(if !*rlverbose then ioto_prin2 "!] ")
else if w neq 'false then <<
resl := rl_smkn('and,w . theo) . resl;
if !*rlverbose then ioto_prin2 ".] "
>> else if !*rlverbose then
ioto_prin2 "-] "
>>;
return rl_smkn('or,resl)
end;
procedure cl_tnft(f,terml);
% Common logic tree normal form tree. [f] is a formula, [terml] is
% a list of terms. Returns a big formula.
begin scalar w,cdl,cd,rvl;
if null terml then return f;
cdl := rl_t2cdl car terml;
while cdl do <<
cd := car cdl;
cdl := cdr cdl;
w := rl_simpl(rl_mk2('and,cd,f),nil,-1);
if w eq 'true then <<
rvl := '(true);
cdl := nil
>> else if w neq 'false then
rvl := cl_tnft(w,cdr terml) . rvl
>>;
return rl_simpl(rl_smkn('or,rvl),nil,-1)
end;
endmodule; % [clnf]
end; % of file