Artifact a4140a265735eb7b910eb8ff35a474e20491e00fecaf2619d532dbbc03f9f1b1:
- Executable file
r38/packages/redlog/ibalp.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: 31906) [annotate] [blame] [check-ins using] [more...]
% ---------------------------------------------------------------------- % $Id: ibalp.red,v 1.33 2003/09/25 07:47:58 sturm Exp $ % ---------------------------------------------------------------------- % Copyright (c) 2003 A. Dolzmann, A. Seidl, and T. Sturm % ---------------------------------------------------------------------- % $Log: ibalp.red,v $ % Revision 1.33 2003/09/25 07:47:58 sturm % Removed conflicts. Probably no change. % % Revision 1.32 2003/09/25 07:30:35 seidl % Pretty printing for TeXmacs. % % Revision 1.31 2003/07/11 17:16:06 sturm % New service rlqnum (number of quantifiers). % % Revision 1.30 2003/06/11 08:45:49 dolzmann % Added black box rl_qssimpl. % % Revision 1.29 2003/06/03 11:19:58 dolzmann % Removed unused variables from ibalp_simplat1. % Added black box definitions. % % Revision 1.28 2003/05/27 07:32:31 dolzmann % Added black block implementation for ibalp_qssubat. % % Revision 1.27 2003/05/23 16:01:31 dolzmann % Added implementation of black-box ibalp_qscsaat. % % Revision 1.26 2003/05/21 09:05:03 dolzmann % Added service rlquine. % % Revision 1.25 2003/05/03 20:47:36 sturm % Fixed a bug in ibalp_simpatom. % Fixed a bug in ibalp_varsel (and the same in ibalp_badvarsel). % % Revision 1.24 2003/05/03 18:29:42 sturm % Implemented an improved ibalp_qevarsel. % Fixed a bug in ibalp_varlt1 (could not cause wrong results). % % Revision 1.23 2003/05/03 16:03:26 sturm % Implemented procedure ibalp_prepterm. % Added definition for parameter rl_tordp!*, s.t. service rl_termml!* works. % % Revision 1.22 2003/05/03 14:51:53 sturm % Added development switch ibalpbadvarsel for dual strategy. % % Revision 1.21 2003/05/03 14:44:18 sturm % Added variable selection strategy. % Added verbose output for case that elimination set contains only one % variable. % % Revision 1.20 2003/05/03 12:33:28 sturm % Added tableaux methods. % % Revision 1.19 2003/05/03 12:07:30 sturm % Replaced parameter function cl_sacat by ibalp_sacat. % Made some fluid declarations. % % Revision 1.18 2003/05/01 18:56:54 sturm % Added substitution and Boolean normal forms. % % Revision 1.17 2003/05/01 17:22:45 sturm % Fixed a missing scalar declaration in ibalp_simpterm. This led to % semantic errors! % % Revision 1.16 2003/05/01 08:48:31 sturm % Rewritten ibalp_simpterm/ibalp_resimpterm. % % Revision 1.15 2003/04/25 11:57:17 seidl % Modified ibalp_simplat1 so it works with smart simplification. % % Revision 1.14 2003/04/24 17:20:47 sturm % Fixed procedures ibalp_simpterm, ibalp_resimpterm, etc. % Added procedure ibalp_opp. % Added procedure ibalp_ordatp. % % Revision 1.13 2003/04/24 16:32:07 seidl % Smart simplification now available, rlsism is on now by default. % Changed ibalp_ordatp; still we need a better predicate, one which % sorts in addition by variable name (this is needed for commutative % law). % % Revision 1.12 2003/04/23 11:02:40 sturm % Rewritten ibalp_negateat. % Provided rlqea. % % Revision 1.11 2003/04/17 16:52:47 seidl % Added ibalp_termmlat and declared various services. % % Revision 1.10 2003/04/17 15:22:31 sturm % Fixed bugs in QE code. % Added services rl_ex!* and rl_all!*. % % Revision 1.9 2003/04/17 14:48:02 seidl % Removed bug from ibalp_varlt1. % % Revision 1.8 2003/04/17 13:34:52 sturm % Quantifier elimination should work. % % Revision 1.7 2003/04/17 12:13:32 seidl % After simplification, atoms are of the form a=1 or a=0 now, and NNF works % as it should, i.e. there is no "not" in the result. % % Revision 1.6 2003/04/15 14:02:17 seidl % Simplified result has now always atoms of the form a=1. This is needed % for rlpcprint. % % Revision 1.5 2003/04/10 18:34:22 seidl % Changed <=>, =>, <= to <->, ->, <- to avoid conflict with lessequal. % Simplification (including term expansion) implemented. Modified % ibalp_negateat, added ibalb_flip01, ibalp_simplat1 ibalp_term2fo and % ibalp_ordatp. % % Revision 1.4 2003/03/27 13:12:03 sturm % Clean treatment of static case sensitivity. % % Revision 1.3 2003/03/27 12:53:10 sturm % Fixed a buig in ibalp_priequal. % % Revision 1.2 2003/03/27 12:38:41 sturm % Implemented printing for bnot. % Added procedures ibalp_upcase, ibalp_downcase, ibalp_uppercasep. % Added procedures ibalp_pcvar,ibalp_pcvarp. % Implemented rlpcvar, which is stat rlis, i.e., has sytax like e.g. "tr". % % Revision 1.1 2003/03/26 18:20:44 seidl % Initail check-in. Syntax works. % % ---------------------------------------------------------------------- lisp << fluid '(ibalp_rcsid!* ibalp_copyright!*); ibalp_rcsid!* := "$Id: ibalp.red,v 1.33 2003/09/25 07:47:58 sturm Exp $"; ibalp_copyright!* := "Copyright (c) 2003 A. Dolzmann, A. Seidl, and T. Sturm" >>; module ibalp; % Initial Boolean Algebra Lisp Prefix Form. Provides for % Propositional Logic as well. off raise; % static case sensitivity for compilation create!-package('(ibalp),nil); load!-package 'cl; load!-package 'rltools; imports rltools,cl; fluid '(!*rlverbose !*rlbnfsac !*rlpcprint !*rlsiso); flag('(ibalp),'rl_package); % Switches switch rlpcprint; % Parameters put('ibalp,'rl_params,'( (rl_tordp!* . ibalp_ordp) (rl_a2cdl!* . ibalp_a2cdl) (rl_subsumption!* . ibalp_subsumption) (rl_bnfsimpl!* . cl_bnfsimpl) (rl_sacatlp!* . cl_sacatlp) (rl_sacat!* . ibalp_sacat) (rl_subat!* . ibalp_subat) (rl_subalchk!* . ibalp_subalchk) (rl_eqnrhskernels!* . ibalp_eqnrhskernels) (rl_smupdknowl!* . cl_smupdknowl) (rl_smrmknowl!* . cl_smrmknowl) (rl_smcpknowl!* . cl_smcpknowl) (rl_smmkatl!* . cl_smmkatl) (rl_smsimpl!-impl!* . cl_smsimpl!-impl) (rl_smsimpl!-equiv1!* . cl_smsimpl!-equiv1) (rl_elimset!* . ibalp_elimset) (rl_translat!* . ibalp_translat) (rl_varsel!* . ibalp_varsel) (rl_transform!* . ibalp_transform) (rl_trygauss!* . ibalp_trygauss) (rl_specelim!* . ibalp_specelim) (rl_simplat1!* . ibalp_simplat1) (rl_ordatp!* . ibalp_ordatp) (rl_termmlat!* . ibalp_termmlat) (rl_op!* . ibalp_op) (rl_varsubstat!* . ibalp_substat) (rl_negateat!* . ibalp_negateat) (rl_qemkans!* . ibalp_qemkans) (rl_varlat!* . ibalp_varlat) (rl_qstrycons!* . cl_qstrycons) (rl_qscsaat!* . ibalp_qscsaat) (rl_qssubat!* . ibalp_qssubat) (rl_qsconsens!* . cl_qs1consens) (rl_qsimpltestccl!* . cl_qsimpltestccl) (rl_qssubsumep!* . cl_qssusubymem) (rl_qstautp!* . cl_qstautp) (rl_qssimpl!* . cl_qssibysimpl) )); % Services put('ibalp,'rl_services,'( (rl_tab!* . cl_tab) (rl_atab!* . ibalp_atab) (rl_itab!* . ibalp_itab) (rl_cnf!* . ibalp_cnf) (rl_dnf!* . ibalp_dnf) (rl_subfof!* . cl_subfof) (rl_identifyonoff!* . cl_identifyonoff) (rl_ex!* . cl_ex) (rl_all!* . cl_all) (rl_simpl!* . cl_simpl) (rl_atnum!* . cl_atnum) (rl_qnum!* . cl_qnum) (rl_matrix!* . cl_matrix) (rl_atl!* . cl_atl) (rl_atml!* . cl_atml) (rl_pnf!* . cl_pnf) (rl_nnf!* . cl_nnf) (rl_nnfnot!* . cl_nnfnot) % not available in algebraic mode (rl_termml!* . cl_termml) (rl_terml!* . cl_terml) (rl_varl!* . cl_varl) (rl_fvarl!* . cl_fvarl) (rl_bvarl!* . cl_bvarl) (rl_quine!* . cl_quine) (rl_qe!* . cl_qe) (rl_qea!* . cl_qea))); % Switches put('ibalp,'rl_cswitches,'( (rlsism . t) (raise . nil))); % Admin put('ibalp,'simpfnname,'ibalp_simpfn); put('ibalp,'rl_prepat,'ibalp_prepat); put('ibalp,'rl_resimpat,'ibalp_resimpat); put('ibalp,'rl_lengthat,'ibalp_lengthat); put('ibalp,'rl_prepterm,'ibalp_prepterm); put('ibalp,'rl_simpterm,'ibalp_simpterm); algebraic infix equal; put('equal,'prifn,'ibalp_priequal); put('equal,'fancy!-prifn,'ibalp_fancy!-priequal); put('equal,'ibalp_simpfn,'ibalp_simpat); put('equal,'fancy!-prifn,'ibalp_fancy!-priequal); put('equal,'number!-of!-args,2); procedure ibalp_priequal(f); % Print equal. [f] is of the form $([equal] s t)$. Returns in % identifier. Provided that switches [nat] and [rlpcprint] are on: % If $s$ is and identifier and the corresponding uppercase % identifier is $S$ is a PC variable, then print $S$. Else returns % ['failed] and leave printing to [maprin]. begin scalar w,rhs; f := reval f; if not !*nat or not !*rlpcprint then return 'failed; rhs := caddr f; if not eqn(rhs,1) and not eqn(rhs,0) then return 'failed; w := cadr f; if not idp w then return 'failed; w := ibalp_upcase w; if not ibalp_pcvarp w then return 'failed; if eqn(rhs,0) then prin2!* "not("; prin2!* w; if eqn(rhs,0) then prin2!* ")" end; procedure ibalp_fancy!-priequal(c); begin scalar w,rhs; c := reval c; rhs := caddr c; if not !*nat or not !*rlpcprint or not (eqn(rhs,1) or eqn(rhs,0)) then << maprin cadr c; fancy!-prin2 "="; maprin rhs; return ; >>; %if not eqn(rhs,1) and not eqn(rhs,0) then return 'failed; w := cadr c; if not idp w then return 'failed; w := ibalp_upcase w; if not ibalp_pcvarp w then return 'failed; if caddr c eq 0 then fancy!-prin2 "\overline{"; fancy!-prin2 w; if caddr c eq 0 then fancy!-prin2 "}" end; algebraic infix neq; put('neq,'ibalp_simpfn,'ibalp_simpat); put('neq,'number!-of!-args,2); put('neq,'rtypefn,'quotelog); newtok '((!< !>) neq); algebraic operator bnot; put('bnot,'number!-of!-args,1); put('bnot,'prifn,'ibalp_pribnot); put('bnot,'fancy!-prifn,'pasf_fancy!-pribnot); newtok '((!~) bnot); procedure ibalp_pribnot(u); << prin2!* " "; prin2!* get(car u,'prtch); prin2!* " "; if pairp cadr u and get(caadr u,'infix) then << prin2!* "("; maprin cadr u; prin2!* ")" >> else maprin cadr u >>; symbolic procedure pasf_fancy!-pribnot(u); << fancy!-prin2 "("; fancy!-prin2 "\~{}"; % \char126 maprin cadr u; fancy!-prin2 ")"; >>; algebraic infix bequiv; put('bequiv,'number!-of!-args,2); put('bequiv,'fancy!-prifn,'pasf_fancy!-pribequiv); newtok '((!< !- !>) bequiv); put('bequiv,'fancy!-infix!-symbol,"\leftrightarrow "); precedence bequiv,neq; symbolic procedure pasf_fancy!-pribequiv(u); << fancy!-prin2 "("; maprin cadr u; fancy!-prin2 "\leftrightarrow{}"; maprin caddr u; fancy!-prin2 ")"; >>; algebraic infix bimpl; put('bimpl,'number!-of!-args,2); put('bimpl,'fancy!-prifn,'pasf_fancy!-pribimpl); newtok '((!- !>) bimpl); put('bimpl,'fancy!-infix!-symbol,"\rightarrow "); precedence bimpl,bequiv; symbolic procedure pasf_fancy!-pribimpl(u); << fancy!-prin2 "("; maprin cadr u; fancy!-prin2 "\rightarrow{}"; maprin caddr u; fancy!-prin2 ")"; >>; algebraic infix brepl; put('brepl,'number!-of!-args,2); put('brepl,'fancy!-prifn,'pasf_fancy!-pribrepl); newtok '((!< !-) brepl); put('brepl,'fancy!-infix!-symbol,"\leftarrow"); precedence brepl,bimpl; symbolic procedure pasf_fancy!-pribrepl(u); << fancy!-prin2 "("; maprin cadr u; fancy!-prin2 "\leftarrow{}"; maprin caddr u; fancy!-prin2 ")"; >>; algebraic infix bor; flag('(bor),'nary); put('bor,'fancy!-prifn,'pasf_fancy!-pribor); newtok '((!|) bor); put('bor,'fancy!-infix!-symbol,"\|"); precedence bor,bimpl; symbolic procedure pasf_fancy!-pribor(u); begin scalar w; fancy!-prin2 "("; w := cdr u; % the arguments maprin car w; w := cdr w; while w do << fancy!-prin2 "|"; maprin car w; w := cdr w; >>; fancy!-prin2 ")"; end; algebraic infix band; flag('(band),'nary); put('band,'fancy!-prifn,'pasf_fancy!-priband); newtok '((!&) band); put('band,'fancy!-infix!-symbol,"\&"); precedence band,bor; symbolic procedure pasf_fancy!-priband(u); begin scalar w; fancy!-prin2 "("; w := cdr u; % the arguments maprin car w; w := cdr w; while w do << fancy!-prin2 "\&{}"; maprin car w; w := cdr w; >>; fancy!-prin2 ")"; end; flag('(band bor bimpl brepl bequiv equal neq),'spaced); flag('(ibalp_simpat),'full); flag('(ibalp_pcstat),'endstatfn); procedure ibalp_pcstat(); begin scalar x; x := cursym!*; scan(); return {x} end; procedure ibalp_pcform(form,an!-empty!-al,mode); if mode eq 'symbolic then mkquote intern car form % we mean the identifier then else % we know [mode eq 'algebraic] mkquote {'equal,ibalp_downcase car form,1}; put('rlpcvar,'stat,'rlis); put('rlpcvar,'formfn,'ibalp_pcvarform); procedure ibalp_pcvarform(vl,an!-empty!-al,mode); << ibalp_pcvar for each v in cdr vl join << if pairp v and ibalp_pcvarp car v then << lprim {"ignoring",car v,"- already declared pcvar"}; nil >> else if not ibalp_uppercasep v then << lprim{"ignoring",v,"- not an uppercase identifier"}; nil >> else {v} >>; mkquote nil >>; procedure ibalp_pcvar(vl); for each v in vl do << put(v,'stat,'ibalp_pcstat); put(v,'formfn,'ibalp_pcform) >>; procedure ibalp_uppercasep(id); id = ibalp_upcase id; procedure ibalp_pcvarp(id); get(id,'stat) eq 'ibalp_pcstat; procedure ibalp_upcase(id); intern compress for each c in explode id collect red!-char!-upcase c; procedure ibalp_downcase(id); intern compress for each c in explode id collect red!-char!-downcase c; ibalp_pcvar '(A B C D E F G H I J K L M N O P Q R S T U V W X Y Z); procedure ibalp_subat(al,at); ibalp_mk2(ibalp_op at, ibalp_subt(al,ibalp_arg2l at),ibalp_subt(al,ibalp_arg2r at)); procedure ibalp_subt(al,u); begin scalar w; if idp u and (w := atsoc(u,al)) then return cdr w; if atom u then return u; return car u . for each arg in cdr u collect ibalp_subt(al,arg) end; procedure ibalp_subalchk(al); ; procedure ibalp_eqnrhskernels(x); ibalp_varlt cdr x; procedure ibalp_simpterm(u); % Simplify term. [u] is Lisp Prefix. Returns the [u] as a IBALP % term. begin scalar op; if atom u then return ibalp_simpatom u; op := car u; if ibalp_boolfp op then return op . for each arg in cdr u collect ibalp_simpterm arg; u := reval u; if eqcar(u,op) then typerr(op,"Boolean function"); return ibalp_simpterm u % terminates because reval is idempotent end; procedure ibalp_simpatom(u); begin scalar w; if u = 0 or u = 1 then return u; if idp u then << if (w := rl_gettype u) then return ibalp_simpterm reval u; flag({u},'used!*); return u >>; if null u then typerr("nil","Boolean term"); if numberp u then typerr({"number",u},"Boolean term"); if stringp u then typerr({"string",u},"Boolean term") end; procedure ibalp_prepterm(u); u; procedure ibalp_boolfp(op); op memq '(bnot band bor bimpl brepl bequiv); procedure ibalp_resimpterm(u); ibalp_simpterm u; procedure ibalp_prepat(f); % Prep atomic formula. [f] is a IBALP atomic formula. Returns [f] % in Lisp prefix form. f; procedure ibalp_resimpat(f); % Resimp atomic formula. [f] is an IBALP atomic formula. Returns the % atomic formula [f] with resimplified terms. ibalp_mk2(ibalp_op f,ibalp_resimpterm ibalp_arg2l f, ibalp_resimpterm ibalp_arg2r f); procedure ibalp_lengthat(f); % Length of atomic formula. [f] is an % atomic formula. Returns a number, the length of [f]. length ibalp_argn f; procedure ibalp_simpat(u); % Simp atomic formula. [u] is Lisp prefix. Returns [u] as an atomic % formula. ibalp_mk2(car u,ibalp_simpterm cadr u,ibalp_simpterm caddr u); procedure ibalp_op(atf); % Get operator. [atf] is an atomic formula $(R,t_1,t_2)$. Returns % $R$ which is $=$. car atf; procedure ibalp_atfp(f); % Atomic formula predicate. [f] is a % formula. Returns t is and only if [f] is an atomic formula. ibalp_op f memq '(equal neq); procedure ibalp_arg1(atf); % Unary operator argument. [atf] is an atomic formula $R(t)$. % Returns $t$. cadr atf; procedure ibalp_arg2l(atf); % Binary operator left hand side argument. [atf] is an atomic % formula $R(t_1,t_2)$. Returns $t_1$. cadr atf; procedure ibalp_arg2r(atf); % Binary operator right hand side argument. [atf] is an atomic % formula $R(t_1,t_2)$. Returns $t_2$. caddr atf; procedure ibalp_argn(atf); % n-ary operator argument list. [atf] is an atomic formula % $(R,t_1,...,t_n)$. Returns the list $(t_1,...,t_n)$. cdr atf; procedure ibalp_mk2(op,lhs,rhs); % Make atomic formula for binary operator. [op] is one of the % operators [equal], [neq]; [lhs] and [rhs] are terms. Returns the % atomic formula $[op]([lhs],[rhs])$. {op,lhs,rhs}; procedure ibalp_1mk2(op,lhs); % Make zero right hand atomic formula for binary operator. [op] is % the operator [equal]. Returns the atomic formula $[op]([lhs],0)$. {op,lhs,1}; procedure ibalp_mkn(op,argl); % Make atomic formula for n-ary operator. [op] is one of the % operators [equal], [neq]; [argl] is a list $(t_1,t_2)$ of terms. % Returns the atomic formula $(op,t_1,t_2)$. op . argl; %%% --- this part might become ibalpbnf.red --- %%% procedure ibalp_dnf(f); % Disjunctive 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 ibalp_cnf(f); % 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 ibalp_subsumption(l1,l2,gor); % Discretely valued field standard form subsume. [l1] and [l2] are % lists of atomic formulas. Returns one of [keep1], [keep2], [nil]. if gor eq 'or then ( if ibalp_subsumep!-and(l1,l2) then 'keep2 else if ibalp_subsumep!-and(l2,l1) then 'keep1 ) else % [gor eq 'and] if ibalp_subsumep!-or(l1,l2) then 'keep1 else if ibalp_subsumep!-or(l2,l1) then 'keep2 else nil; procedure ibalp_subsumep!-and(l1,l2); % 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 ibalp_subsumep!-or(l1,l2); % 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 ibalp_sacat(a1,a2,gor); % 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 formulas 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 rhs1,rhs2; if ibalp_arg2l a1 neq ibalp_arg2l a2 then return nil; rhs1 := ibalp_arg2r a1; rhs2 := ibalp_arg2r a2; if rhs1 = rhs2 then return 'keep; if rhs1 = 0 and rhs2 = 1 or rhs1 = 1 and rhs2 = 0 then return 'drop; return nil end; %%% --- this part might become ibalpmisc.red --- %%% procedure ibalp_atab(f); cl_atab cl_simpl(f,nil,-1); procedure ibalp_itab(f); cl_itab cl_simpl(f,nil,-1); procedure ibalp_a2cdl(atml); % Atomic to case distinction list. [atml] is a list of atomic % formulas with multiplicity, the right hand side of which is % always zero. Returns a list, each containing a list of case % distinction w.r.t. the term $t$, i.e. ${t<0,t=0,t>0}$ resp. % ${t=0,t neq 0}$. for each pr in atml collect {ibalp_mk2('equal,w,0),ibalp_mk2('equal,w,1)} where w=ibalp_arg2l car pr; procedure ibalp_substat(atf,new,old); % Substitute into atomic formula. [atf] is an atomic formula; [old] % is a variable; [new] is a term. ibalp_mk2(ibalp_op atf,ibalp_qesubt(ibalp_arg2l atf,old,new), ibalp_qesubt(ibalp_arg2r atf,old,new)); procedure ibalp_ordatp(a1,a2); % Ordered atomic formula predicate. [a1] and [a2] are atomic % formulas. Returns [t] iff [a1] is less than [a2]. begin scalar u1,u2; u1 := ibalp_arg2l a1; u2 := ibalp_arg2l a2; if u1 neq u2 then return ibalp_ordp(u1,u2); u1 := ibalp_arg2r a1; u2 := ibalp_arg2r a2; if u1 neq u2 then return ibalp_ordp(u1,u2); return ibalp_ordrelp(ibalp_op a1,ibalp_op a2) end; procedure ibalp_ordp(u1,u2); ordp(!*k2f u1,!*k2f u2); procedure ibalp_ordrelp(r1,r2); not not (r2 memq (r1 memq '(equal neq))); procedure ibalp_negateat(atf); % Negate atomic formula. [atf] is an atomic formula. % Returns an atomic formula equivalent to $\lnot [atf]$. ibalp_mk2(ibalp_op atf,ibalp_arg2l atf,ibalp_negatet ibalp_arg2r atf); procedure ibalp_negatet(u); if u = 0 then 1 else if u = 1 then 0 else {'bnot,u}; procedure seidl_negateat(atf); % Negate atomic formula. [atf] is an atomic formula. % Returns an atomic formula equivalent to $\lnot [atf]$. The % relation is left unchanged, and ibalb_cveq relies on this. begin scalar lhs,rhs,rel,op; rhs := ibalp_arg2r atf; lhs := ibalp_arg2l atf; rel := ibalp_op atf; % flip 0 and 1, if possible if rhs member {0,1} then return ibalp_mk2(rel,lhs,ibalp_flip01 rhs); if lhs member {0,1} then return ibalp_mk2(rel,ibalp_flip01 lhs,rhs); % drop a bnot, if possible op := ibalp_op rhs; if op equal 'bnot then return ibalp_mk2(rel,lhs,ibalp_arg1 rhs); op := ibalp_op lhs; if op equal 'bnot then return ibalp_mk2(rel,ibalp_arg1 lhs,rhs); % otherwise: negate left side return ibalp_mk2(rel,ibalp_mk1('bnot,rhs),rhs); end; procedure ibalp_flip01(n); if n = 1 then 0 else if n = 0 then 1 else rederr{"ibalb_flip01: cannot flip",n}; procedure ibalp_cveq(a); % Convert to equation. [a] is an atom. Returns an atom. if ibalp_op a eq 'equal then a else ibalp_mk2('equal,ibalp_arg2l w,ibalp_arg2r w) where w=ibalp_negateat(a); procedure ibalp_termmlat(at); % Term multiplicity list of atomic formula. [at] is an atomic % formula. Returns the multiplicity list off all non-zero terms in % [at]. begin scalar lhs,rhs; lhs := ibalp_arg2l at; rhs := ibalp_arg2r at; if lhs = 0 and rhs = 0 then return nil; if lhs = 0 then return {rhs . 1}; if rhs = 0 then return {lhs . 1}; if lhs = rhs then return {lhs . 2}; return {lhs . 1,rhs . 1} end; %(rl_varlat!* . ibalp_varlat))); %%% needs to be written in ibalpmisc.red %%% --- this part might become ibalpsiat.red --- %%% procedure ibalp_simplat1(f,sop); % Simplify atomic formula. [f] is an atomic formula; [sop] is the % boolean operator [f] occurs with or [nil]. Maybe later: accesses % switches [rlsiatadv], [rlsipd], [rlsiexpl], and [rlsiexpla]. % Returns a quantifier-free formula that is a simplified equivalent % of [f]. begin scalar lhs,rhs; if not (ibalp_op f memq '(equal neq)) then return nil; % why not error? % left-hand side domain element: switch sides for pcprint lhs := ibalp_arg2l f; rhs := ibalp_arg2r f; if numberp lhs then f := ibalp_mk2(ibalp_op f,rhs,lhs); f := ibalp_cveq f; % from now on, we have an equation lhs := ibalp_arg2l f; rhs := ibalp_arg2r f; % two numbers if numberp lhs and numberp rhs then return if lhs eq rhs then 'true else 'false; % if we have a "propositional variable", we're done: if idp lhs and numberp rhs then return f; % from now on we have a complex term (longer than a "propositional % variable") to expand, and to simplify. lhs := ibalp_term2fo lhs; rhs := ibalp_term2fo rhs; return cl_simpl(cl_nnf rl_mk2('equiv,lhs,rhs),nil,-1) end; procedure ibalp_term2fo(term); % Convert term to Formula. [term] is a lisp-prefix expression over % the language of initial boolean algebras. Returns a formula, with % atoms being only of the form [a=1]. begin scalar rel; if numberp term then return if term = 0 then 'false else 'true; if idp term then return ibalp_mk2('equal,term,1); rel := ibalp_op(term); if rel eq 'bnot then return rl_mk1('not,ibalp_term2fo ibalp_arg1 term); if rel eq 'band then return rl_mkn('and,for each a in ibalp_argn term collect ibalp_term2fo a); if rel eq 'bor then return rl_mkn('or,for each a in ibalp_argn term collect ibalp_term2fo a); if rel eq 'bimpl then return rl_mk2('impl,ibalp_term2fo ibalp_arg2l term, ibalp_term2fo ibalp_arg2r term); if rel eq 'brepl then return rl_mk2('repl,ibalp_term2fo ibalp_arg2l term, ibalp_term2fo ibalp_arg2r term); if rel eq 'bequiv then return rl_mk2('equiv, ibalp_term2fo ibalp_arg2l term, ibalp_term2fo ibalp_arg2r term); rederr {"ibalp_term2fo: unknown symbol:",rel} end; procedure ibalp_varlat(a); % Variable list atomic formlua. [a] is an atomic formula. Returns a % list of identifiers. The set of variables ocurring in [a]. union(ibalp_varlt ibalp_arg2l a,ibalp_varlt ibalp_arg2r a); procedure ibalp_varlt(u); % Variable list term. [u] is an IBALP term. Returns a list of % identifiers. The set of variables ocurring in [u]. ibalp_varlt1(u,nil); procedure ibalp_varlt1(u,vl); % Variable list term. [u] is an IBALP term; [vl] is a list of % identifiers. Returns a list of identifiers. The set of variables % ocurring in [u] added to [vl]. begin if u = 0 or u = 1 then return nil; if idp u then return lto_insertq(u,vl); for each arg in ibalp_argn u do vl := ibalp_varlt1(arg,vl); return vl end; procedure ibalp_transform(f,v); % Transform formula. [f] is a quantifier-free formula; [v] is a % variable. Returns $([f] . nil)$. This behavior informs [cl_qe] % that there no transformation possible. f . nil; procedure ibalp_trygauss(f,v); % Try Gauss. [f] is a quantifier-free formula; [v] is a variable. % Returns [failed]. This behavior informs [cl_qe] that there no % Gauss elimination possible. 'failed; procedure ibalp_specelim(f,vl,theo,ans,bvl); % Special elimination. [f] is a quantifier-free formula; [vl] is a % list of variables; [theo] is a theory; [ans] is Bool; [bvl] is % the list of bound variables. Returns [failed]. This behavior % informs [cl_qe] that there no special elimination possible. 'failed; switch ibalpbadvarsel; procedure ibalp_varsel(f,vl,theo); % Variable selection. [vl] is a list of variables; [f] is a % quantifier-free formula; [theo] is the current theory. Returns a % variable. begin scalar v; integer n; if not !*rlqevarsel then return car sort(vl,'ibalp_ordp); if !*ibalpbadvarsel then return ibalp_badvarsel(f,vl); for each pr in cl_termml f do if car pr memq vl and cdr pr > n then << v := car pr; n := cdr pr >>; return v or car sort(vl,'ibalp_ordp) end; procedure ibalp_badvarsel(f,vl); begin scalar v; integer n; for each pr in cl_termml f do if car pr memq vl and - cdr pr < n then << v := car pr; n := cdr pr >>; return v or car sort(vl,'ibalp_ordp) end; % % procedure ibalp_varsel(f,vl,theo); % % Variable selection. [vl] is a list of variables; [f] is a % % quantifier-free formula; [theo] is the current theory. Returns a % % variable. % begin scalar v,found,gvp; % if not !*rlqevarsel then % return car vl; % while reverse vl and not found do << % v := car vl; % vl := cdr vl; % gvp := not ibalp_goodvarp(f,v,{0,1}); % good var is bad var once more % if !*ibalpbadvarsel then % gvp := not gvp; % if gvp then % found := t % >>; % return v % end; % procedure ibalp_goodvarp(f,v,l); % begin scalar argl; % if rl_cxp rl_op f then << % argl := rl_argn f; % while argl and l do << % l := ibalp_goodvarp(car argl,v,l); % argl := cdr argl % >>; % return l % >>; % if ibalp_arg2l f eq v then % return deletip(ibalp_arg2r f,l); % return l % end; procedure ibalp_translat(atf,v,theo,pos,ans); % Translate atomic formula. [atf] is an atomic formula $\rho(t,0)$; % [v] is a variable; [theo] is the current theory; [pos], [ans] are % Bool. Returns an ALP. if ibalp_arg2l atf neq v then nil . nil else if pos then ibalp_mkalp('equal,{ibalp_arg2r atf}) else if ibalp_arg2r atf = 1 then ibalp_mkalp('equal,{0}) else ibalp_mkalp('equal,{1}); procedure ibalp_mkalp(tag,l); % Make alist pair. [tag] is a key; [l] is an entry. Returns an ALP. {tag . l} . {tag . 1}; %DS elimination_set % A list $(...,(p . (l_1,...,l_n)),...)$ where the $p$ are procedures % and the $l_i$ are parameter lists $(l_{i1},...,l_{im})$ such that % there is $p(bvl,theo,f,v,l_{i1},...,l_{im})$ called for % substitution, where $f$ is the considered formula, and $v$ the % considered variable. procedure ibalp_elimset(v,alp); % Elimination set. [v] is a variable; [alp] is a pair of alists. % Returns an elimination set. << if !*rlverbose and not cdr cdaar alp then ioto_prin2 "S"; {'ibalp_qesub . for each bconst in cdaar alp collect {bconst}} >>; procedure ibalp_qesub(bvl,theo,f,v,bconst); theo . cl_apply2ats1(f,'ibalp_qesubat,{v,bconst}); procedure ibalp_qesubat(atf,v,bconst); ibalp_mk2(ibalp_op atf, ibalp_qesubt(ibalp_arg2l atf,v,bconst),ibalp_arg2r atf); procedure ibalp_qesubt(u,v,bconst); if u eq v then bconst else if atom u then u else car u . for each arg in cdr u collect ibalp_qesubt(arg,v,bconst); procedure ibalp_qemkans(an,atr); sort(for each x in an collect {'equal,car x,car caddr x}, function(lambda(x,y); ordp(!*k2f cadr x,!*k2f cadr y))); procedure ibalp_qscsaat(at); if not(idp ibalp_arg2l at and ibalp_arg2r at memq '(1 0)) then rederr {"ibalp_qscsaat: cannot process",at} else (ibalp_arg2l at . ibalp_arg2r at ); procedure ibalp_qssubat(pl,at); begin scalar w; if not(idp ibalp_arg2l at and ibalp_arg2r at memq '(1 0)) then rederr {"ibalp_qssubat: cannot process",at}; w := assoc(ibalp_arg2l at,pl); if w then return ibalp_mk2(ibalp_op at,cdr w,ibalp_arg2r at); return at end; on raise; % static case sensitivity was for compilation only endmodule; % [ibalp] end; % of file