% ----------------------------------------------------------------------
% $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
