Artifact 762b929e07d569b6f38b870139be9ff47c93f2d8e79e709f2c3ca75dd962e89b:
- Executable file
r37/packages/redlog/ofsfbnf.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: 7917) [annotate] [blame] [check-ins using] [more...]
% ---------------------------------------------------------------------- % $Id: ofsfbnf.red,v 1.4 1999/03/23 07:41:37 dolzmann Exp $ % ---------------------------------------------------------------------- % Copyright (c) 1995-1999 Andreas Dolzmann and Thomas Sturm % ---------------------------------------------------------------------- % $Log: ofsfbnf.red,v $ % Revision 1.4 1999/03/23 07:41:37 dolzmann % Changed copyright information. % % Revision 1.3 1999/03/21 13:38:04 dolzmann % Removed procedure acfsf_bnfsimpl which was identical to cl_bnfsimpl. % % Revision 1.2 1996/10/07 12:03:22 sturm % Added fluids for CVS and copyright information. % % Revision 1.1 1996/03/22 12:14:02 sturm % Moved and split. % % ---------------------------------------------------------------------- lisp << fluid '(ofsf_bnf_rcsid!* ofsf_bnf_copyright!*); ofsf_bnf_rcsid!* := "$Id: ofsfbnf.red,v 1.4 1999/03/23 07:41:37 dolzmann Exp $"; ofsf_bnf_copyright!* := "Copyright (c) 1995-1999 by A. Dolzmann and T. Sturm" >>; module ofsfbnf; % Ordered field standard form boolean normal forms. Submodule of [ofsf]. procedure ofsf_dnf(f); % Ordered field standard form conjunctive normal form. [f] is a % formula. Returns a DNF of [f]. if !*rlbnfsac then (cl_dnf f) where !*rlsiso=T else cl_dnf f; procedure ofsf_cnf(f); % Ordered field standard form conjunctive normal form. [f] is a % formula. Returns a CNF of [f]. if !*rlbnfsac then (cl_cnf f) where !*rlsiso=T else cl_cnf f; procedure ofsf_subsumption(l1,l2,gor); % Ordered field standard form subsume. [l1] and [l2] are lists of % atomic formulas. Returns one of [imp], [rep], [nil]. if gor eq 'or then ( if ofsf_subsumep!-and(l1,l2) then 'keep2 else if ofsf_subsumep!-and(l2,l1) then 'keep1 ) else % [gor eq 'and] if ofsf_subsumep!-or(l1,l2) then 'keep1 else if ofsf_subsumep!-or(l2,l1) then 'keep2; procedure ofsf_subsumep!-and(l1,l2); % Ordered field standard form subsume [and] case. [l1] and [l2] are % lists of atomic formulas. begin scalar a; while l2 do << a := car l2; l2 := cdr l2; if cl_simpl(a,l1,-1) neq 'true then a := l2 := nil >>; return a end; procedure ofsf_subsumep!-or(l1,l2); % Ordered field standard form subsume [or] case. [l1] and [l2] are % lists of atomic formulas. begin scalar a; while l1 do << a := car l1; l1 := cdr l1; if cl_simpl(rl_smkn('or,l2),{a},-1) neq 'true then a := l1 := nil >>; return a end; procedure ofsf_sacatlp(a,l); % Ordered field standard form subsume and cut atomic formula list % predicate. [a] is an atomic formula; [l] is a list of atomic % formulas. [T] is returned if a subsumption or cut beween [a] and % an element of [l] is possible. not ((ofsf_arg2l a neq ofsf_arg2l w) and ordp(ofsf_arg2l a,ofsf_arg2l w)) where w=car l; procedure ofsf_sacat(a1,a2,gor); % Ordered field standard form subsume and cut atomic formula. [a1] % and [a2] are atomic formulas; [gor] is one of [or], [and]. % Returns [nil], ['keep], ['keep2], ['keep1], ['drop], or an atomic % formula. If [nil] is returned then neither a cut nor a % subsumption can be applied, if [keep] is returned then the atomic % formuas are identical, in the case of [keep1] or [keep2] the % respective atomic formula must be kept but the other can be % dropped. If an atomic formula $a$ is returned then it is the % result of the cut beween [a1] and [a2], if ['drop] is returned, a % cut with result ['true] or ['false] can be performed. begin scalar w; if ofsf_arg2l a1 neq ofsf_arg2l a2 then return nil; w := ofsf_sacrel(ofsf_op a1, ofsf_op a2,gor); if w memq '(drop keep keep1 keep2) then return w; return ofsf_0mk2(w,ofsf_arg2l a1) end; procedure ofsf_sacrel(r1,r2,gor); % Ordered field standard form subsume and cut relation. [r1] and % [r2] are relations; [gor] is one of [or], [and]. Returns ['keep], % ['keep2], ['keep1], ['drop], or a relation. [r1] and [r2] are % considered as relations of atomic formulas $[r1](t,0)$ and % $[r2](t,0)$. If [keep] is returned then the atomic formulas are % identical, in the case of [keep1] or [keep2] the respective % atomic formula must be kept but the other can be dropped, if a % relation $\rho$ is returned a cut with result $t\rho 0$ can be % performed, where $t$ is the left hand side of [a1] and [a2], if % ['drop] is returned, a cut with result ['true] or ['false] can be % performed. if gor eq 'or then ofsf_sacrel!-or(r1,r2) else ofsf_sacrel!-and(r1,r2); procedure ofsf_sacrel!-or(r1,r2); % Ordered field standard form subsume and cut relation or. [r1] and % [r2] are relations. ['keep], ['keep2], ['keep1], ['drop], or a % relation is returned. [r1] and [r2] are considered as relations % of atomic formulas $[r1](t,0)$ and $[r2](t,0)$. If [keep] is % returned then the atomic formulas are identical, in the case of % [keep1] or [keep2] the respective atomic formula must be kept but % the other can be dropped, if a relation $\rho$ is returned a cut % with result $t\rho 0$ can be performed, where $t$ is the left % hand side of [a1] and [a2], if ['drop] is returned a cut with % result ['true] can be performed. begin scalar w; w:= '( (lessp . ( (lessp . keep) (leq . keep1) (equal . leq) (neq . keep1) (geq . drop) (greaterp . neq))) (leq . ( (lessp . keep2) (leq . keep) (equal . keep2) (neq . drop) (geq . drop) (greaterp . drop))) (equal . ( (lessp . leq) (leq . keep1) (equal . keep) (neq . drop) (geq . keep1) (greaterp . geq))) (neq . ( (lessp . keep2) (leq . drop) (equal . drop) (neq . keep) (geq . drop) (greaterp . keep2))) (geq . ( (lessp . drop) (leq . drop) (equal . keep2) (neq . drop) (geq . keep) (greaterp . keep2))) (greaterp . ( (lessp . neq) (leq . drop) (equal . geq) (neq . keep1) (geq . keep1) (greaterp . keep)))); return cdr atsoc(r1,cdr atsoc(r2,w)); end; procedure ofsf_sacrel!-and(r1,r2); % Ordered field standard form subsume and cut relation and. [r1] and % [r2] are relations. ['keep], ['keep2], ['keep1], ['drop], or a % relation is returned. [r1] and [r2] are considered as relations % of atomic formulas $[r1](t,0)$ and $[r2](t,0)$. If [keep] is % returned then the atomic formulas are identical, in the case of % [keep1] or [keep2] the respective atomic formula must be kept but % the other can be dropped, if a relation $\rho$ is returned a cut % with result $t\rho 0$ can be performed, where $t$ is the left % hand side of [a1] and [a2], if ['drop] is returned a cut with % result ['false] can be performed. begin scalar w; w:= '( (lessp . ( (lessp . keep) (leq . keep2) (equal . drop) (neq . keep2) (geq . drop) (greaterp . drop))) (leq . ( (lessp . keep1) (leq . keep) (equal . keep1) (neq . lessp) (geq . equal) (greaterp . drop))) (equal . ( (lessp . drop) (leq . keep2) (equal . keep) (neq . drop) (geq . keep2) (greaterp . drop))) (neq . ( (lessp . keep1) (leq . lessp) (equal . drop) (neq . keep) (geq . greaterp) (greaterp . keep1))) (geq . ( (lessp . drop) (leq . equal) (equal . keep1) (neq . greaterp) (geq . keep) (greaterp . keep1))) (greaterp . ( (lessp . drop) (leq . drop) (equal . drop) (neq . keep2) (geq . keep2) (greaterp . keep)))); return cdr atsoc(r1,cdr atsoc(r2,w)); end; endmodule; % [ofsfbnf] end; % of file