Artifact 58e967d136a43cfc53e80e44b5d0bb93bee0219818ed26ee140179a49ae75a5a:
- Executable file
r38/packages/redlog/clnf.red
— part of check-in
[f2fda60abd]
at
2011-09-02 18:13:33
on branch master
— Some historical releases purely for archival purposes
git-svn-id: https://svn.code.sf.net/p/reduce-algebra/code/trunk/historical@1375 2bfe0521-f11c-4a00-b80e-6202646ff360 (user: arthurcnorman@users.sourceforge.net, size: 17439) [annotate] [blame] [check-ins using] [more...]
% ---------------------------------------------------------------------- % $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