% ----------------------------------------------------------------------
% $Id: clbnf.red,v 1.20 2003/12/08 15:30:00 dolzmann Exp $
% ----------------------------------------------------------------------
% Copyright (c) 1995-2003 A. Dolzmann, A. Seidl, and T. Sturm
% ----------------------------------------------------------------------
% $Log: clbnf.red,v $
% Revision 1.20 2003/12/08 15:30:00 dolzmann
% Renamed variable state to kstate, because hephys/physop.red defines
% state as an stat function. This causes errors reading clbnf provided
% physop is loaded.
%
% Revision 1.19 2003/06/11 08:45:23 dolzmann
% Rewritten Quine simplification such that rl_simpl is not called by
% default. Calling rl_simpl can cause male function due to unwanted
% algebraic simplifications.
% Added procedure for converting a bnf into set representation wrt. a
% given operator.
% Added black boxes rl_qssimpl and rl_qssiadd.
% Added black box implementations cl_qssimpl and cl_qssibysimpl.
%
% Revision 1.18 2003/06/06 08:06:14 dolzmann
% Added power set computation by enumeration.
%
% Revision 1.17 2003/06/04 07:23:04 dolzmann
% Added CNF support to cl_quine by computing the minimal DNF of the negated
% input formula.
%
% Revision 1.16 2003/06/04 06:08:09 dolzmann
% Added procedure cl_qssusubytab as a generic implementation for
% blackbox rl_qssubsumtion. It requires rl_qssusuat.
% Improved procedure cl_qsimpltestccl.
%
% Revision 1.15 2003/06/03 16:09:40 dolzmann
% Fixed a bug in cl_qsnconsens1: The return value nil of rl_qstrycons
% entered the list of consensus.
% Fixed a bug in cl_qssusubyit: The eq test to 'true was missing.
%
% Revision 1.14 2003/06/03 11:18:10 dolzmann
% Completely overworked quine simplification. In particular: Removed
% bugs during prime implicant computation. Added missing tautology test
% for implication test. Added comments on use of black boxes. Moved and
% sorted procedure definitions.
%
% Revision 1.13 2003/05/27 08:19:54 dolzmann
% Procedure cl_qsconsens now returns a list of consensus. Adapted
% procedure cl_qscpi accordingly.
%
% Revision 1.12 2003/05/27 07:27:51 dolzmann
% Use cl_qssub instead of rl_subfof;
% Added black box rl_qssubat.
% Added default implementation cl_qssubat for black box rl_qssubat.
% Added procedure cl_qssimplc as a future replacement for rl_simpl.
% Changed cl_bnf2set. cl_quine can now deal with BNFs containing
% identical clauses.
%
% Revision 1.11 2003/05/23 16:01:01 dolzmann
% Added selection from all prime implicants as descibed in Quine 1955.
% Fixed a bug in consensus computation: nil as an legal conses was not
% recognized.
%
% Revision 1.10 2003/05/21 09:03:27 dolzmann
% Added first experimental implementation of service rlquine for
% simplifying Boolean normal forms in the style of W. V. Quine.
%
% Revision 1.9 2003/05/20 11:35:46 dolzmann
% Moved procedures.
%
% Revision 1.8 1999/04/13 13:10:55 sturm
% Updated comments for exported procedures.
%
% Revision 1.7 1999/04/01 11:26:47 dolzmann
% Reformatted one procedure.
%
% Revision 1.6 1999/03/22 17:07:12 dolzmann
% Changed copyright information.
% Reformatted comments.
%
% Revision 1.5 1999/03/21 13:34:06 dolzmann
% Corrected comments.
%
% Revision 1.4 1996/10/07 11:45:47 sturm
% Added fluids for CVS and copyright information.
%
% Revision 1.3 1996/07/13 10:53:07 dolzmann
% Added black box implementations cl_bnfsimpl, cl_sacatlp, and cl_sacat.
%
% Revision 1.2 1996/07/07 14:34:19 sturm
% Turned some cl calls into service calls.
%
% Revision 1.1 1996/03/22 10:31:27 sturm
% Moved and split.
%
% ----------------------------------------------------------------------
lisp <<
fluid '(cl_bnf_rcsid!* cl_bnf_copyright!*);
cl_bnf_rcsid!* := "$Id: clbnf.red,v 1.20 2003/12/08 15:30:00 dolzmann Exp $";
cl_bnf_copyright!* := "(c) 1995-2003 by A. Dolzmann, A. Seidl, and T. Sturm"
>>;
module clbnf;
% Common logic boolean normal forms. Submodule of [cl]. This module
% provides CNF and DNF computation.
%DS
% <SG-DNF> ::= <GOR> . <SGCL>
% <SGCL> ::= (<SGCONJ>,...)
% <SGCONJ> ::= <GAND> . <SATOTVL>
% <GOR> ::= ['or] | ['and]
% <GAND> ::= ['and] | ['or] "opposite to <GOR>"
% <SATOTVL> ::= (<TRUTH VALUE>) | (<ATOMIC FORMULA>, ...)
procedure cl_dnf(f);
% Common logic disjunctive normal form. [f] is a formula. Returns a
% DNF of [f].
rl_simpl(cl_gdnf(f,'or),nil,-1);
procedure cl_cnf(f);
% Common logic conjunctive normal form. [f] is a formula. Returns a
% CNF of [f].
rl_simpl(cl_gdnf(f,'and),nil,-1);
procedure cl_gdnf(f,gor);
% Common logic generic disjunctive normal form. [f] is a formula;
% [gor] is one of [and], [or]. Returns a G-DNF of [f].
begin scalar strictgdnf,gdnf,svrlsiexpla;
f := rl_simpl(rl_nnf f,nil,-1);
svrlsiexpla := !*rlsiexpla;
!*rlsiexpla := nil;
(strictgdnf := cl_strict!-gdnf(f,gor)) where !*rlbnfsm=nil;
if !*rlbnfsm then
strictgdnf := gor . cl_subsume(rl_argn strictgdnf,gor);
!*rlsiexpla := svrlsiexpla;
gdnf := cl_unstrict(strictgdnf,gor);
return gdnf
end;
procedure cl_strict!-gdnf(f,gor);
% Common logic strict generic disjunctive normal form. [f] is a
% formula; [gor] is one of [and], [or]. Returns a strict g-DNF,
% i.e. a formula upto unary [and]'s and [or]'s, which is in g-DNF.
begin scalar w;
w := cl_mkstrict(rl_simpl(cl_strict!-gdnf1(f,gor),nil,-1),gor);
return rl_bnfsimpl(w,gor)
end;
procedure cl_subsume(gcl,gor);
% Common logic subsume. [gcl] is a generic conjunction list; [gor]
% is one of [and], [or]. Returns a generic conjunction list
% equivalent to [gcl]. Performs simplification by subsumption.
begin scalar w;
if null gcl or null cdr gcl then return gcl;
w := cl_subsume1(gcl,gor);
if car w then <<
cddr w := cl_subsume(cddr w,gor);
return cdr w
>>;
return cl_subsume(cdr w,gor)
end;
procedure cl_subsume1(gcl,gor);
% Common logic subsume 1. [gcl] is a generic conjunction list;
% [gor] is one of [and], [or]. A pair $(c,l)$ is returned, where
% $c$ is [nil] or a list of atomic formulas and $l$ is a generic
% conjunction list. [gcl] is modified. The subsumption relation
% beween [car gcl] and all elements of [cdr gcl] is tested. If $c$
% is nil, [car gcl] was suberflous. $l$ is the modified [gcl] in
% which all superflous conjunctions are deleted. If $c$ is non-nil,
% it is [car gcl] and [car gcl] cannot be dropped. If [cl_setrel]
% is used this requires, that [!*rlsiso] and [!*rlidentify] are on.
begin scalar a,w,x,scgcl,oscgcl;
x := cdar gcl;
oscgcl := gcl;
scgcl := cdr gcl;
while scgcl do <<
a := car scgcl; scgcl := cdr scgcl;
w := if !*rlbnfsm then
rl_subsumption(x,cdr a,gor)
else
cl_setrel(x,cdr a,gor);
if w eq 'keep1 then
cdr oscgcl := scgcl
else if w eq 'keep2 then
x := scgcl := nil
else
oscgcl := cdr oscgcl
>>;
if null x then gcl := cdr gcl;
return x . gcl
end;
procedure cl_setrel(l1,l2,gor);
% Common logic set relation. [l1] and [l2] are list of atomic
% formulas. [gor] is one of [and], [or]. Returns [nil], [keep1], or
% [keep2]. If [l1] is a subset of [l2] [keep1] is returned; if [l2]
% is a subset of [l1] [keep2] is returned otherwise [nil] is
% returned.
begin scalar kstate,a1,hlp;
while l1 and l2 and car l1 eq car l2 do <<
l1 := cdr l1;
l2 := cdr l2
>>;
if null (l1 and l2) then <<
if null (l1 or l2) then return 'keep1; % both equal.
return l2 and 'keep1 or 'keep2
>>;
kstate := 'keep1;
if rl_ordatp(car l1,car l2) then <<
hlp := l1; l1 := l2; l2 := hlp;
kstate := 'keep2
>>;
repeat <<
a1 := car l1; l1 := cdr l1;
l2 := memq(a1,l2);
if null l2 then a1 := l1 := nil
>> until null l1;
return a1 and kstate
end;
procedure cl_strict!-gdnf1(f,gor);
% Common logic disjunctive normal form in strict representation.
% [f] is a formula containing no first-order operators but $\land$
% and $\lor$; [gor] is one of ['and], ['or]. Returns a strict g-DNF
% of [f], i.e. a g-disjunction of g-conjunctions of atomic formulas
% including unary $\lor$ and $\land$ if necessary.
begin scalar gand,op,subgdnfl,noop,noopgdnf;
gand := if gor eq 'or then 'and else 'or;
op := rl_op f;
if op eq gor then
return rl_mkn(gor,for each subf in rl_argn(f) join
rl_argn(cl_strict!-gdnf(subf,gor)));
if op eq gand then <<
subgdnfl := for each subf in rl_argn(f) collect
cl_strict!-gdnf(subf,gor);
% Switch to noop form.
noop := for each subf in subgdnfl collect
for each gconj in rl_argn subf collect rl_argn gconj;
% Computing the cartesian product of the conjunctive lists is
% now equivalent to an application of the law of
% distributivity, though the result is not flat yet.
noopgdnf := cl_bnf!-cartprod noop;
% Switch back to our normal representation.
return rl_mkn(gor,for each gconj in noopgdnf collect
rl_mkn(gand,for each x in gconj join append(x,nil)))
>>;
if rl_cxp op and not rl_tvalp op then
rederr {"cl_strict!-gdnf: illegal operator",op,"in BNF computation"};
return rl_mkn(gor,{rl_mkn(gand,{f})})
end;
procedure cl_mkstrict(f,gor);
% Common logic make strict. [f] is a g-DNF. Returns a strict g-DNF,
% possibly including one truth value.
begin scalar op,gand;
gand := cl_flip gor;
op := rl_op f;
if not rl_cxp op or rl_tvalp op then
return rl_mkn(gor,{rl_mkn(gand,{f})});
if op eq gand then
return rl_mkn(gor,{f});
if op neq gor then
rederr {"BUG IN cl_mkstrict"};
return rl_mkn(gor,for each subf in rl_argn f collect
if rl_op subf eq gand then subf else rl_mkn(gand,{subf}))
end;
procedure cl_unstrict(sgdnf,gor);
% Common logic unstrict, [sdnf] is a sg-DNF; [gor] is one of [and],
% [or]. Returns a g-DNF.
rl_smkn(gor,for each conj in rl_argn sgdnf collect
% A unary g-and does not have a cddr, ignore it.
if cdr rl_argn conj then conj else car rl_argn conj);
procedure cl_bnf!-cartprod(s);
% Common logic boolean normal form cartesian product. [s] is a list
% $(s_1,...,s_n)$ of lists. Returns $s_1 \times ... \times s_n$ as
% a list of $n$-element lists. The empty set and singletons are
% their own cartesian product.
if null s or null cdr s then s else cl_bnf!-cartprod1 s;
procedure cl_bnf!-cartprod1(s);
% Common logic boolean normal form cartesian product. [s] is a list
% $(s_1,...,s_n)$ of lists with $n \geq 2$. Returns $s_1 \times ...
% \times s_n$ as a list of $n$-element lists.
begin scalar w;
if null cdr s then
return for each m in car s collect {m};
w := cl_bnf!-cartprod1 cdr s;
return for each m in car s join
for each y in w collect m . y
end;
procedure cl_bnfsimpl(sgdnf,gor);
% Common logic boolean normal form simplification. [sgdnf] is an
% SG-DNF; [gor] is one of the operators [and], [or]. Returns an
% SG-DNF equivalent to [sgdnf]. Performs simplification of [gcl].
% Accesses switch [rlbnfsac].
if !*rlbnfsac then cl_sac(sgdnf,gor) else sgdnf;
procedure cl_sac(sgdnf,gor);
% Common logic subsumption and cut. [sgdnf] is a sg-DNF; [gor] is
% one of [or], [and]. Returns a sg-DNF equivalent to [sgdnf]. This
% procedures performs simplifications based on order theoretical
% subsumption and cut. There are no possible applications of order
% theoretical subsumption and cut between subformulas of the
% returned sg-DNF.
begin scalar w,gand;
if rl_tvalp car rl_argn car rl_argn sgdnf then return sgdnf;
gand := cl_flip(gor);
% switch to noop form
w := for each x in rl_argn sgdnf collect
rl_argn x;
w := cl_applysac(w,gor);
if w eq 'break then
return rl_mkn(gor,{rl_mkn(gand,{cl_cflip('true,gor eq 'or)})});
w := for each x in w join
if x then
{rl_mkn(gand,x)}
else
nil;
if null w then
return rl_mkn(gor,{rl_mkn(gand,{cl_cflip('true,gor eq 'or)})});
return gor . w
end;
procedure cl_applysac(l,gor);
% Common logic apply subsumption and cut. [l] is a list of lists of
% atomic formulas; [gor] is one of [or], [and]. Returns ['break] or
% a list $k$ of list of atomic formulas. If ['break] is returned
% [l] is as a g-DNF equivalent to ['true] in case of ['gor eq 'or]
% and equivalent to ['false] in case ['gor eq 'and]. The lists are
% considered as generic disjunctive normal forms and are in this
% sense equivalent. There is no possible application of order
% theoretical subsumption or cut between elements of $k$.
begin scalar w,ll,res;
ll := l;
while ll do <<
w := cl_applysac1(car ll,res,gor);
if w eq 'break then <<
ll := nil;
res := 'break
>> else <<
ll := cdr ll;
if car w then
res := cdar w . cdr w
else
res := cdr w
>>
>>;
return res
end;
procedure cl_applysac1(c,l,gor);
% Common logic apply subsumption and cut 1. [c] is a list of atomic
% formulas; [l] is a list of list of atomic formulas; [gor] is one
% of [or], [and]. Returns ['break] or a pair $(c' . \lambda)$. If
% ['break] is returned [l] is as a g-DNF equivalent to ['true] in
% case of ['gor eq 'or] and equivalent to ['false] in case ['gor eq
% 'and]. $c'$ is either [nil] or a pair $(\tau . \gamma)$, where
% $\tau$ is one of [T] and [nil] and $\gamma$ is a list of atomic
% formulas. $\lambda$ is a list of list of atomic formulas. If $c'$
% is [nil] then the conjunction over [c] is implied by a
% conjunction over an element in [l]. If $\tau$ is [T] then
% $\gamma$ is equal to $c$, otherwise $\gamma$ is the result of a
% cut between $c$ and an element of $l$. In all cases there is no
% possible application of subsumption or cut between $\gamma$ and
% an arbitrary element of $\lambda$. [l] is modified.
begin scalar w,flg;
flg:=T;
repeat <<
w := cl_applysac2(c,l,gor);
if w eq 'break then <<
w := '(nil); % leave the loop
flg := 'break
>>;
if car w and null caar w then <<
flg:=nil;
c := cdar w;
l := cdr w
>>;
>> until null car w or caar w;
if flg eq 'break then
return 'break;
if null car w then
return w;
return (flg . cdar w) . cdr w
end;
procedure cl_applysac2(c,l,gor);
% Common logic apply subsumption and cut 1. [c] is a list of atomic
% formulas; [l] is a list of list of atomic formulas; [gor] is one
% of [or], [and]. Returns ['break] or a pair ($c'$ . $\lambda$). If
% ['break] is returned [l] is as a g-DNF equivalent to ['true] in
% case of ['gor eq 'or] and equivalent to ['false] in case ['gor eq
% 'and]. $c'$ is either [nil] or a pair $(\tau . \gamma)$, where
% $\tau$ is one of [T] and [nil] and $\gamma$ is a list of atomic
% formulas. $\lambda$ is a list of list of atomic formulas. If $c'$
% is [nil] then the conjunction over [c] is implied by a
% conjunction over an element in [l]. If $\tau$ is [T] then
% $\gamma$ is equal to $c$, otherwise $\gamma$ is the result of a
% cut between $c$ and an element of $l$. [l] is modified. If
% ['break] is returned then the formula $['gor]([c],\phi)$ is
% equivalent to ['true] in the case ['gor eq 'or] or to ['false] in
% the case ['gor eq 'and].
begin scalar w,ll;
if null l then return ( (T . c) . nil);
ll := l;
while ll and ((w := cl_subandcut(c, car ll,gor)) eq 'keep1) do
ll := cdr ll;
if null w then return 'break;
if null ll then return ((T . c) . nil);
if w eq 'keep2 then return (nil . ll);
if w neq 'failed then % [w] is the result of the cut
% between [c] and [car ll].
return (nil . w) . cdr ll;
% We know, that there is no interaction between [c] and [car ll]
w := cl_applysac2(c,cdr ll,gor);
if w eq 'break then
return 'break;
cdr ll := cdr w;
return car w . ll;
end;
procedure cl_subandcut(l1,l2,gor);
% Common logic subsumption and cut. [l1] and [l2] are sorted lists
% of atomic formulas; [gor] is one of ['or], ['and]. Returns
% ['failed], ['keep1], ['keep2] or a list of atomic formulas. Both
% [l1] and [l2] are considered as conjunctions. ['keep1] is
% returned if [l2] subsumes [l1]; ['keep2] is returned if [l1]
% subsumes [l2]. If a list [l] of atomic formulas is returned then
% [l] is the result of a cut between [l1] and [l2]. Both
% subsumption and cut means order theoretical generalizations of
% the respective notions of the propositional calculus.
begin scalar kstate,w,x; integer c;
x := l1; % Save one of [l1] and [l2] for computing a cut.
% Determing the maximal common prefix of [l1] and [l2] and its length.
while l1 and l2 and (car l1 equal car l2) do <<
c := c+1;
l1 := cdr l1; l2 := cdr l2
>>;
if null (l1 and l2) then << % on of [l1] and [l2] are empty
if null (l1 or l2) then return 'keep1; % both equal.
% [l1] is a ``subset'' of [l2] or vice versa.
return (l2 and 'keep1) or 'keep2
>>;
% We have [l1 and l2] and [car l1 neq car l2].
kstate := 'keep1;
w := rl_sacat(car l1,car l2,gor); % [w neq 'keep]
if w eq 'keep2 then <<
kstate := 'keep2;
% swap [l1] and [l2] upto the first element.
w := cdr l1; l1 := cdr l2; l2 := w
>> else if w eq 'keep1 then <<
l1 := cdr l1; l2 := cdr l2
>> else if w then
return cl_trycut(x,c,w,cdr l1,cdr l2)
else if rl_ordatp(car l1,car l2) then << % [car l1 neq car l2]
kstate := 'keep2;
w := l1; l1 := l2; l2 := w
>>;
% Now [l1] is ``shorter'' than [l2]; no cuts are possible.
while l1 do <<
w := cl_sacatl(car l1, l2,gor);
l2 := cdr w; w := car w;
l1 := cdr l1;
if w neq 'keep1 then
l1 := nil % Leave the loop.
>>;
if w eq 'keep1 then return kstate;
return 'failed
end;
procedure cl_trycut(l,c,at,l1,l2);
% Common logic try cut. [l], [l1], and [l2] are lists of atomic
% formulas; [c] is an integer; [at] is an atomic formula or
% ['drop]. Returns ['failed] or a sorted list $\lambda$ of atomic
% formulas. If a cut beween [l1] and [l2] are possible then a list
% of atomic formulas is returned, otherwise [nil] is returned. [l]
% is a list $(a_1,...,a_n)$, [l1] is a list $(c_1,...,c_m)$.
% $lambda$ is a list $(a_1,...,a_c,b,c_1,...,c_m)$, where $b$ is
% the atomic formula [at] if [at] is not [drop], otherwise $b$ is
% ommitted.
begin scalar a;
if null l1 and null l2 then <<
l := for i := 1 : c collect <<
a := car l; l := cdr l; a
>>;
if at eq 'drop then
return sort(l,'rl_ordatp);
return sort(at . l,'rl_ordatp)
>>;
if l1 neq l2 then return 'failed;
% [l1] and [l2] are equal.
for i:=1:c do << l1 := car l . l1; l := cdr l >>;
if at neq 'drop then
l1 := at . l1;
return sort(l1,'rl_ordatp)
end;
% Generic black box implementations.
procedure cl_sacatl(a,l,gor);
% Common logic subsume and cut atomic formula list. [a] is an
% atomic formula; [l] is a sorted list of atomic formulas; [gor] is
% one of [or], [and]. Returns a pair $(\alpha . \lambda)$ where
% $\alpha$ is a relation, ['keep1], or [nil]; [l] is a possibly
% empty list of atomic formulas. $\alpha$ is [T] if [a] is implied
% by an atomic formula from [l]; if $\alpha$ is [nil] then neither
% [a] is implied by an atomic formula from [l] nor a cut between
% [a] and an atomic formula from [l] is possible, otherwise
% $\alpha$ is the result of such a cut. $\lambda$ is the rest of
% [l] not involved in the computation of $\alpha$.
begin scalar w;
if null l then
return '(nil . nil);
if not rl_sacatlp(a,l) then
return (nil . l);
w := rl_sacat(a,car l,gor);
if not w then
return cl_sacatl(a,cdr l,gor);
if w memq '(keep1 keep) then
return ('keep1 . cdr l);
if w eq 'keep2 then
return (nil . cdr l);
return (w . cdr l) % [w] is a relation or [drop]
end;
procedure cl_sacatlp(a,l);
% Common logic subsumption and cut atomic formula list predicate.
% [a] is an atomic formula; [l] is a list of atomic formulas.
% Returns [T] a subsumption or cut beween [a] and an element of [l]
% is possible.
T;
procedure cl_sacat(a1,a2,gor);
% Common logic subsumption and cut atomic formula. [a1] and [a2]
% are atomic formulas; [gor] is one of the operators [or], [and].
% Returns [nil], one of the identifiers [keep], [keep1], [keep2],
% [drop], or an atomic formula. The return value [nil] indicates
% that neither a cut nor a subsumption can be applied. If [keep] is
% returned, then the atomic formulas are identical. In the case of
% [keep1] or [keep2] the corresponding atomic formula can be kept,
% and the other one can be dropped. If an atomic formula $a$ is
% returned, then this atomic formula is the result of the cut
% beween [a1] and [a2]. If [drop] is returned, then a cut with
% result [true] or [false] can be performed.
if a1 = a2 then 'keep else nil;
% ----------------------------------------------------------------------
% Simplification of Boolean normal forms in the style of W. V. Quine.
% ----------------------------------------------------------------------
% The following services are required:
% * rl_simpl
% The following black boxes are required:
% * rl_qscsaat(at) Default: cl_qscsa
% * rl_qssubat(sl,at) Default: cl_qssubat (requires rl_negateat)
% * rl_qsconsens Default: cl_qs1consens (requires rl_qstrycons)
% Default; cl_qsnconsens (requires rl_qstrycons)
% * rl_qsimpltestccl Default: cl_qsimpltestccl (req. rl_qscsa,
% rl_qssubat, rl_qstautp
% rl_qssimpl)
% * rl_qstautp Default: cl_qstautp
% * rl_qssubsumep Default: cl_qssusubymem
% cl_qssusubysi
% cl_qssusubyit (requires rl_simpl)
% cl_qssusubytab (requires rl_qssusuat)
% * rl_qstrycons Default cl_qstrycons (requires rl_negateat)
% * rl_qssimpl Defualt cl_qssibysimpl
% Default cl_qssimpl (requires rl_qssiadd)
% * rl_qssiadd kein default
% Warning: The blackboxes rl_qscsaat and rl_qssubat belong to each
% other. They cannot be implemented independently.
% For rapid prototyping, using only the relation betwen $alpha$ and
% $\overline{\alpha}$ one can use the following assignment of generic
% implementations to black boxes. We use the service rl_simpl and the
% black boxes rl_negateat and rl_ordatp from the general context
% environment.
% * rl_qssubsumep -> cl_qssusubymem
% * rl_qsconsens -> cl_qsnconsens
% * rl_qstrycons -> cl_qstrycons
% * rl_qsimpltestccl -> cl_qsimpltestccl
% * rl_qscsaat -> cl_qscsaat
% * rl_qssubat -> cl_qssubat
% * rl_qstautp -> cl_qstautp
% To gain maximal use of algebraic dependencies between relations one
% have to implement at least the following black boxes in a context
% specific manner: rl_qssubsumep rl_qstrycons rl_qssubat
% TODO: Truth values in BNF
% TODO: List2set vermeiden -> adjoin
% TODO: CNF's
% TODO: rl_simpl beschraenken oder eigenes.
% TODO: Substituierende Simplifikation
procedure cl_quine(f);
% Common logic Quine simplification. [f] is a a formula in a BNF.
% Returns a formula in BNF.
begin scalar w,op,s;
w := cl_bnf2set f;
op := car w;
if not op then
return f;
if op eq 'and then
s := cl_qsnot cdr w
else
s := cdr w;
s := cl_qs(s,'or); % Non generic
if op eq 'and then
s := cl_qsnot s;
return cl_set2bnf(s,op)
end;
procedure cl_qsnot(s);
for each c in s collect cl_qsnot1 c;
procedure cl_qsnot1(c);
for each a in c collect rl_negateat a;
procedure cl_bnf2set(f);
cl_bnf2set1(f,nil);
procedure cl_bnf2set1(f,xop);
% Common logic bnf to set representation. [f] is a formula in bnf.
% Returns a pair $(\gamma,l)$ where $l$ is a list of list of atomic
% formulas and $\gamma$ is [nil] or an operator. if $\gamma$ is
% [or] then [f] is a DNF and $l$ is the set representation of $f$;
% if it is [and] then f is a CNF and again $f$ is a set
% representation of f; if $\gamma$ is [nil] then $l$ is identical
% to [f].
begin scalar op,w;
if rl_tvalp f then
return nil . f;
if not cl_cxfp f then
return nil . {{f}};
op := rl_op f;
if not(op memq '(and or)) then
rederr {"cl_bnf2set: not in bnf: ",f};
w := cl_bnf2set2(rl_argn f,op);
if not car w then % List of atomic formulas, translated to singletons
if op eq xop then
return op . w
else if cl_flip op eq xop then
return op . {rl_argn f}
else
return nil . f;
return op . cdr w
end;
procedure cl_bnf2set2(fl,op);
% Common logic bnf to set representation subroutine. [fl] is a list
% of atomic formulas or flat formulas not containing truth values.
% Returns a pair $(\gamma,l)$ where l is a list of list of atomic
% formulas; $\gamma$ is a flag. If it is [T] then fl contains a
% non-atomic formula.
begin scalar xop,flg,w;
xop := cl_flip op;
w := for each f in fl collect <<
if not cl_cxfp f then
{f}
else if rl_op f eq xop then <<
flg := T;
sort(list2set rl_argn f,'rl_ordatp)
>> else
rederr {"cl_bnf2set1: not in bnf: ",f}
>>;
return flg . list2set w
end;
procedure cl_set2bnf(ll,op);
begin scalar flop;
flop := cl_flip(op);
return rl_smkn(op,for each l in ll collect
rl_smkn(flop,l))
end;
procedure cl_qs(s,op);
% Common logic quine simplification. [s] is a set representation of
% a BNF. [op] is one of [and], [or]. Returns a set representation.
begin scalar w;
if !*rlverbose then
ioto_tprin2 {"[Quine: ",cl_qssize s,"/",length s};
w := cl_qscpi(s,op);
if w eq 'break then <<
ioto_prin2t {" -> 0/0]"};
return {{}} % True for DNF; False for CNF
>>;
if !*rlverbose then
ioto_prin2 {" -> ",cl_qssize w,"/",length w};
return cl_qsselect(w,op);
end;
procedure cl_qscpi(cl,op);
% Common logic quine simplification compute prime implicants. [s]
% is a set representation of a BNF. [op] is one of [and], [or].
% Returns a set representation.
begin scalar firstl,scfirstl,first,secondl,scsecondl,second,newl,w;
newl := cl;
while newl do <<
newl := cl_qssisu(newl,op);
firstl := cl_qssisutwo(firstl,newl,op);
secondl := newl;
newl := nil;
scfirstl := firstl;
while scfirstl do <<
first := car scfirstl;
scfirstl := cdr scfirstl;
scsecondl := secondl;
while scsecondl do <<
second := car scsecondl;
scsecondl := cdr scsecondl;
if not(second eq first) then <<
w := rl_qsconsens(first,second,op);
if w eq 'break then
newl := scsecondl := scfirstl := nil
else
foreach cs in w do
if cs and not(cl_qssubsumelp(cs,firstl,op)) and
not(cs member newl)
then
newl := cs . newl
>>
>> % while scsecondl
>> % while scfirstl
>>; % newl
if (w eq 'break) then
return 'break;
return firstl
end;
procedure cl_qssisu(l,op);
% Simplify by subsumtion. [l] is a list of clauses. Returns a list
% of clauses.
for each x in l join
if not(cl_qssubsumelp(x,delq(x,l),op)) then
{x};
procedure cl_qssisutwo(l1,l2,op);
% Neither to l1 nor to l2 subsumption can be applied. No clause of
% l2 subsumes a clause of l1.
begin scalar w;
w := for each x in l1 join
if not(cl_qssubsumelp(x,l2,op)) then
{x};
return nconc(w,l2)
end;
procedure cl_qssubsumelp(c,cl,op);
% Returns [T] if [c] subsumes one of the clauses in cl.
begin scalar r;
while (cl and not(r)) do <<
r := cl_qssubsumep(c,car cl,op);
cl := cdr cl;
>>;
return r
end;
procedure cl_qssubsumep(c1,c2,op);
if op eq 'or then
rl_qssubsumep(c1,c2,op)
else
rl_qssubsumep(c2,c1,op);
switch psen;
on1 'psen;
procedure cl_qsselect(s,op);
begin scalar w,core,dcs; integer csize,wsize,clen,wlen;
w := cl_qsspltcore(s,op);
core := car w;
dcs := cdr w;
if !*rlverbose then <<
csize := cl_qssize core;
clen := length core;
ioto_prin2 {" -> ",csize,"/",clen,"+",cl_qssize dcs,"/",length dcs}
>>;
dcs := cl_qsrmabsdisp(core,dcs,op);
if !*rlverbose then
ioto_prin2 {" -> ",csize,"/",clen,"+",cl_qssize dcs,"/",length dcs};
if !*psen then
w := cl_qsselect2(core,dcs,op)
else
w := cl_qsselect1(core,dcs,cl_subsets dcs,op);
if !*rlverbose then <<
wsize := cl_qssize w;
wlen := length w;
ioto_prin2t {" -> ",csize,"/",clen,"+",wsize,"/",wlen,
" = ",csize+wsize,"/",clen+wlen,"]"}
>>;
w := nconc(w,core);
return w;
end;
procedure cl_qsselect1(core,dcs,potdcs,op);
begin scalar r,w;
potdcs := cdr reversip potdcs;
while potdcs and not(r) do <<
w := setdiff(dcs,car potdcs);
if cl_qsimpltestclcl(car potdcs,append(core,w),op) then
r := w;
potdcs := cdr potdcs;
>>;
return r
end;
procedure cl_qsselect2(core,dcs,op);
begin scalar r,w,kstate,potdcs;
kstate := dcs . nil;
cl_ps kstate; % Remove leading nil;
while (potdcs:=cl_ps kstate) neq 'final and not(r) do <<
w := setdiff(dcs,potdcs);
if cl_qsimpltestclcl(w,append(core,potdcs),op) then
r := potdcs;
>>;
return r
end;
procedure cl_qsspltcore(s,op);
begin scalar core,dcs;
for each x in s do
if rl_qsimpltestccl(x,delq(x,s),op) then
dcs := x . dcs
else
core := x . core;
return core . dcs;
end;
procedure cl_qsrmabsdisp(core,dcs,op);
for each c in dcs join
if not(rl_qsimpltestccl(c,core,op)) then
{c};
procedure cl_qsimpltestclcl(pl,cl,op);
% quine simplification implication test clauses list clauses list.
% [pl] is the list of all premise clauses; [cl] is the list of all
% conclusion clauses; [op] is one of [and] or [or]. Returns [T] or
% [nil].
begin scalar r;
r := T;
while pl and r do <<
r := rl_qsimpltestccl(car pl,cl,op);
pl := cdr pl;
>>;
return r
end;
procedure cl_subsets(l);
sort(cl_subsets1 l,'cl_lengthp);
procedure cl_lengthp(l1,l2);
length l1 < length l2;
procedure cl_subsets1(l);
begin scalar w,r,x;
if null l then
return {nil};
w := cl_subsets1 cdr l;
x := car l;
for each y in w do
r := (x . y) . r;
return nconc(r,w)
end;
procedure cl_qssize(s);
for each x in s sum length x;
%------------------------------------------------------------------------
% Generic Implementations of rl_qssubsumep
%------------------------------------------------------------------------
procedure cl_qssusubysi(c1,c2,op);
% Subsumtion by Simplification.
rederr "Out of order -> ueber rl_simpl";
% cl_qssimplc1(c2,c1,op) eq 'true;
procedure cl_qssusubyit(c1,c2,op);
% Subsumtion by implication test.
cl_qsimpltestcc(c1,c2,op) eq 'true;
procedure cl_qssusubymem(c1,c2,op);
% Subsumtion by member. Returns [T] is [c1] g-subsumes [c2] and
% hence [c1] implies [c2].
begin scalar l1,l2;
l1 := length c1;
l2 := length c2;
if not(l1>=l2) then
return nil;
return cl_qssusubymem1(c1,c2)
end;
procedure cl_qssusubymem1(c1,c2);
begin scalar r;
r := T;
while c2 and r do <<
if not(car c2 member c1) then
r := nil;
c2 := cdr c2;
>>;
return r
end;
procedure cl_qssusubytab(c1,c2,op);
% Subsumtion by table. Returns [T] is [c1] g-subsumes [c2] and
% hence [c1] implies [c2].
begin scalar l1,l2;
l1 := length c1;
l2 := length c2;
if not(l1>=l2) then
return nil;
return cl_qssusubytab1(c1,c2,op)
end;
procedure cl_qssusubytab1(c1,c2,op);
% Subsumtion by table. Returns [T] is [c1] g-subsumes [c2] and
% hence [c1] implies [c2].
begin scalar r;
r := T;
while c2 and r do <<
r := cl_qssusubytab2(c1,car c2,op);
c2 := cdr c2
>>;
return r
end;
procedure cl_qssusubytab2(c1,a,op);
begin scalar r;
while c1 and not(r) do <<
r := rl_qssusuat(car c1,a,op);
c1 := cdr c1
>>;
return r
end;
%------------------------------------------------------------------------
% Generic implementations of rl_qssimpl
%------------------------------------------------------------------------
% Variant 1: Special simplifier
procedure cl_qssimpl(s,theo,op);
begin scalar r,a,w,ats;
while s and not(rl_tvalp r) do <<
a := car s;
w := cl_qssimplc(a,theo,op);
if w eq 'true then
r := 'true
else if w neq 'false then
r := w . r;
s := cdr s;
>>;
if r eq 'true then
'true;
w := nconc(ats,r);
return if null w then
'false
else w
end;
procedure cl_qssimplc(c,theo,op);
% simplification of one clause.
begin scalar r,a;
while c and r neq 'false do <<
a := car c;
if a eq 'false then
r := 'false
else if a neq 'true then
r := rl_qssiadd(a,r,theo,op);
c := cdr c;
>>;
return if null r then
'true
else
r
end;
% Variant 1: Using rl_simpl
procedure cl_qssibysimpl(s,theo,op);
begin scalar !*rlsiexpla,!*rlsiexpl,f,w;
f := rl_simpl(cl_set2bnf(s,op),nil,-1);
if rl_tvalp f then
return f;
w := cl_bnf2set1(f,'or);
return cdr w
end;
%------------------------------------------------------------------------
% Generic implementations of rl_qsimpltestccl
%------------------------------------------------------------------------
procedure cl_qsimpltestccl(cp,clc,op);
% .. clause clauses list.
begin scalar w,r,sl;
sl := cl_qscsa cp;
while clc and r neq 'true do <<
w := cl_qsimpltestcc1(sl,cp,car clc,op);
if w eq 'true then
r := 'true
else if w neq 'false then
r := w . r;
clc := cdr clc;
>>;
% w := cl_qssimplf(rl_smkn(op,r),nil);
% if not rl_tvalp w and cl_qe(rl_all(w,nil)) eq 'true then
% rederr {"cl_asimpltestcc: computed non-atomic formula:",w};
return rl_qstautp r
end;
procedure cl_qsimpltestcc(cp,cc,op);
cl_qsimpltestcc1(cl_qscsa cp,cp,cc,op);
procedure cl_qsimpltestcc1(sl,cp,cc,op); % TODO
begin scalar w;
w := rl_qssimpl({cl_qssubc(sl,cc)},nil,op); % Warnung: Clause -> Clause
return if rl_tvalp w then
w
else if cdr w then
rederr {"cl_qssimpltestcc1: Unexpected complex formula",w}
else
car w
end;
procedure cl_qstautp(f);
if f eq 'true then
T
else if f eq 'false then
nil
else
(cl_qscpi(f,'or)) eq 'break;
procedure cl_qscsa(c);
% Compute satisfying assignment.
for each a in c collect
rl_qscsaat a;
procedure cl_qssub(pl,s);
for each c in s collect
cl_qssubc(pl,c);
procedure cl_qssubc(pl,c);
for each a in c collect
rl_qssubat(pl,a);
%------------------------------------------------------------------------
% Generic Implementations of rl_qscsaat
%------------------------------------------------------------------------
procedure cl_qscsaat(a);
a;
%------------------------------------------------------------------------
% Generic Implementations of rl_qscsaat
%------------------------------------------------------------------------
procedure cl_qssubat(pl,a);
if a member pl then
'true
else if rl_negateat(a) member pl then
'false
else
a;
%------------------------------------------------------------------------
% Generic Implementations of rl_qsconsens
%------------------------------------------------------------------------
% First variant: Assume there is maximal one consens of two clauses.
procedure cl_qs1consens(c1,c2,op);
% consens computation of 1 consensus. [c1] and [c2] are clausels.
% Computes the unique determined consenus of [c1] and [c2] provided
% it exists.
begin scalar l1,l2,w;
l1 := length c1;
l2 := length c2;
w := if l1<l2 then
cl_qs1consens1(c1,c2,op)
else
cl_qs1consens1(c2,c1,op);
return if w eq 'break then 'break else {w};
end;
procedure cl_qs1consens1(c1,c2,op);
begin scalar w,sc1;
sc1 := c1;
while sc1 and not(w) do <<
w := rl_qstrycons(car sc1,c1,c2,op);
sc1 := cdr sc1
>>;
return w
end;
% Second variant: Multiple consensus of two claues allowed.
procedure cl_qsnconsens(c1,c2,op);
% consens computation of n consensus. [c1] and [c2] are clausels.
% Computes the unique determined consenus of [c1] and [c2] provided
% it exists.
begin scalar l1,l2;
l1 := length c1;
l2 := length c2;
return if l1<l2 then
cl_qsnconsens1(c1,c2,op)
else
cl_qsnconsens1(c2,c1,op)
end;
procedure cl_qsnconsens1(c1,c2,op);
begin scalar w,r,sc1;
sc1 := c1;
while sc1 and w neq 'break do <<
w := rl_qstrycons(car sc1,c1,c2,op);
if w then
r := w . r;
sc1 := cdr sc1;
>>;
return if w eq 'break then 'break else r
end;
%------------------------------------------------------------------------
% Generic Implementations of rl_qstrycons
%------------------------------------------------------------------------
procedure cl_qstrycons(a,c1,c2,op);
% quine simplification try consensus. [a] is an atomic formula,
% [c1] and [c2] are clauses, op is one of ['and], ['or]. Returns
% [T], [nil] or [break].
begin scalar na,sc1,r,cc1;
cc1 := delete(a,c1); % Copy... % TODO: delq or delete?
na := rl_negateat a;
if not(na member c2) then
return nil;
sc1 := cc1;
r := T;
while sc1 and r do <<
if rl_negateat car sc1 member c2 then
r := nil;
sc1 := cdr sc1;
>>;
if not r then
return nil;
r := sort(list2set append(cc1,delete(na,c2)),'rl_ordatp); %TODO: nconc
if null r then
return 'break;
return r
end;
% ------------------------------------------------------------------------
% Enumeration of power set
% ------------------------------------------------------------------------
%DS
% <STATE> ::= l . [z_1,...,z_n]
% Der pointer $v_n$ steht immer vor $v_n-1$
procedure cl_ps(s);
% [s] is a STATE. Returns an element of thepower set. Modifies [s].
begin scalar v,w,r; integer i,n;
v := cdr s;
if cdr s eq 'final then
return 'final;
if null cdr s then
v := cdr s := mkvect (length car s-1);
n := upbv v;
while i<=n and (w:=getv(v,i)) do <<
r := car w . r;
i:=i+1;
>>;
cl_psnext s;
return r
end;
procedure cl_psnext(s);
cl_psnext1(s,0);
procedure cl_psnext1(s,n);
begin scalar w,v;
v := cdr s;
if n > upbv v then
return cdr s := 'final; % Mark and return;
w := getv(v,n);
if null w then % Introduce pointer
return putv(v,n,car s);
w := cdr w; % Try to move
if w then % Success
return putv(v,n,w);
% Overflow occurs.
repeat <<
w := cl_psnext1(s,n+1);
if w neq 'final then
w := cdr getv(v,n+1);
>> until w;
if w eq 'final then
return 'final;
putv(v,n,w)
end;
endmodule; % [clbnf]
end; % of file