reduce-historical/r38/packages/redlog/rlsched.red

% ----------------------------------------------------------------------
% $Id: rlsched.red,v 1.47 2003/10/21 15:23:47 gilch Exp $
% ----------------------------------------------------------------------
% Copyright (c) 1995-1999 Andreas Dolzmann and Thomas Sturm
% ----------------------------------------------------------------------
% $Log: rlsched.red,v $
% Revision 1.47  2003/10/21 15:23:47  gilch
% Added services rlhqe and rlghqe.
%
% Revision 1.46  2003/08/28 13:48:54  seidl
% Added service rlcadproj.
%
% Revision 1.45  2003/08/19 09:30:56  seidl
% Introduced blackbox "bsatp" (bound satisfiability predicate).
%
% Revision 1.44  2003/08/12 14:15:42  seidl
% Added blackbox rl_b2atl.
%
% Revision 1.43  2003/07/11 17:16:09  sturm
% New service rlqnum (number of quantifiers).
%
% Revision 1.42  2003/06/11 08:47:19  dolzmann
% Added black boxes rl_qssimpl and rl_qssiadd.
%
% Revision 1.41  2003/06/04 06:11:14  dolzmann
% Added black box rl_qssusuat.
%
% Revision 1.40  2003/06/03 11:22:37  dolzmann
% Added black boxes rl_qsconsens, rl_qstrycons, rl_qsimpltestccl,
% rl_qssubsumep, rl_qstautp used for the quine simplication.
%
% Revision 1.39  2003/06/01 14:44:19  seidl
% Added blackboxes rl_b2terml (bound to term list) and rl_simplb (simplify
% bound).
%
% Revision 1.38  2003/05/27 07:33:25  dolzmann
% Introduced new black box rl_qssub.
%
% Revision 1.37  2003/05/23 16:02:07  dolzmann
% Added black-box rl_qscsaat
%
% Revision 1.36  2003/05/21 09:05:21  dolzmann
% Added service rlquine.
%
% Revision 1.35  2003/02/02 22:19:32  seidl
% Changed interface for service cad.
%
% Revision 1.34  2003/01/29 15:24:49  sturm
% Added service rlexpand for context pasf. Had to split pasf_exprng for this.
%
% Revision 1.33  2003/01/29 10:43:43  sturm
% Built clean optional argument interface for rlcad and rlgcad. This was buggy.
%
% Revision 1.32  2003/01/25 11:49:41  sturm
% Changed return value and interface for rlcadporder/ofsf_cadporder and
% rlgcadporder/ofsf_gcadporder. They return a list of variables now.
% s2a conversion is done in the scheduler now. Adapted rlcad/ofsf_cad and
% rlgcad/ofsf_gcad accordingly.
%
% Revision 1.31  2003/01/13 10:01:10  dolzmann
% Added entry points for xopt.
%
% Revision 1.30  2003/01/11 17:58:01  sturm
% Added AM services rlcadporder, rlgcadporder for ofsf.
%
% Revision 1.29  2002/08/23 12:32:01  dolzmann
% Added local quantifier elimination.
%
% Revision 1.28  2002/05/29 11:46:35  sturm
% Provided ofsf_gcad() and corresponding AM interface.
%
% Revision 1.27  2002/05/28 13:22:00  sturm
% Added black box rl_fbqe() and corresponding switch rlqefb.
% That is, for ofsf, rlqe uses rlcad in case of failure now.
%
% Revision 1.26  2002/05/28 13:12:24  seidla
% Added switches rlcadpreponly, rlcadte and rlcadpbfvs, changed default for
% switch rlcadaproj to off.
%
% Revision 1.25  2002/01/25 12:38:53  sturm
% Removed obsolete optional argument [n] from ofsfcad().
%
% Revision 1.24  2002/01/16 13:04:02  seidla
% Imported CAD from rlprojects.
%
% Revision 1.23  1999/03/23 09:23:57  dolzmann
% Changed copyright information.
%
% Revision 1.22  1999/03/21 13:39:11  dolzmann
% Added black boxes rl_susipost, rl_susitf, and rl_susibin.
%
% Revision 1.21  1999/03/19 12:19:06  dolzmann
% Added service rlmkcanonic.
%
% Revision 1.20  1999/03/18 14:08:22  sturm
% Added new service rl_specelim!* in cl_qe for covering the "super
% quadratic special case' for ofsf. This method is toggled by switch
% rlsqsc, which is off by default. Context dvfsf uses cl_specelim which
% is constantly "false." Context acfsf does not use cl_qe at all.
%
% Revision 1.19  1999/01/17 16:32:12  dolzmann
% Added service rl_explats.
%
% Revision 1.18  1997/08/24 16:18:53  sturm
% Added service rl_surep with black box rl_multsurep.
% Added service rl_siaddatl.
%
% Revision 1.17  1997/08/14 10:10:47  sturm
% Renamed rldecdeg to rldecdeg1.
% Added service rldecdeg.
%
% Revision 1.16  1997/08/13 12:46:38  dolzmann
% Introduced service rldecdeg.
%
% Revision 1.15  1996/10/23 12:02:54  sturm
% Added "exceptionlist" paramter to rlgqe and rlgqea. Several quantifier
% blocks are treated correctly now.
%
% Revision 1.14  1996/10/21 06:13:52  dolzmann
% Changed interface for services rlstruct and rlifstruct: Second
% parameter is now optional, default is v.
%
% Revision 1.13  1996/10/17 13:52:25  sturm
% Introduced services rlvarl, rlfvarl, and rlbvarl. Renamed cl_varl to
% cl_varl1 for this.
%
% Revision 1.12  1996/10/07 12:03:57  sturm
% Added fluids for CVS and copyright information.
%
% Revision 1.11  1996/10/01 10:25:19  reiske
% Introduced new service rltnf and related code.
%
% Revision 1.10  1996/09/30 16:57:41  sturm
% Switched to new tableau code.
%
% Revision 1.9  1996/09/29 14:21:29  sturm
% Removed switch rlqeans. Introduced service rlqea instead.
% Also introduced corresponding service rlgqea.
%
% Revision 1.8  1996/09/05 11:17:19  dolzmann
% Changed interface for service rlatb.
% Introduced new services rl_ifacml, rl_struct, rl_ifstruct, rl_termml, and
% rl_terml.
% Introduced new black boxes rl_qefsolset, rl_bettergaussp!*, rl_bestgaussp,
% rl_esetunion, rl_structat, rl_ifstructat, and rl_termmlat.
%
% Revision 1.7  1996/08/01 11:46:18  reiske
% Introduced new services rl_natab, rl_nitab, rl_qeipo, and rl_gentheo.
% Introduced new black boxes rl_a2cdl and rl_getineq.
%
% Revision 1.6  1996/07/13 11:23:05  dolzmann
% Introduced new black box rl_smcpknowl.
%
% Revision 1.5  1996/07/07 14:37:22  sturm
% Introduced new service rl_nnfnot.
% Introduced new black box rl_eqnrhskernels.
%
% Revision 1.4  1996/05/21 17:32:42  sturm
% Added service rl_subfof and black boxes rl_subat, rl_subalchk.
%
% Revision 1.3  1996/05/12 08:28:38  sturm
% Introduced new services rlthsimpl and rlgqe.
%
% Revision 1.2  1996/04/18 14:32:33  sturm
% Fixed bugs in macro calls.
%
% Revision 1.1  1996/03/22 12:18:30  sturm
% Moved and split.
%
% ----------------------------------------------------------------------
lisp <<
   fluid '(rl_sched_rcsid!* rl_sched_copyright!*);
   rl_sched_rcsid!* :=
      "$Id: rlsched.red,v 1.47 2003/10/21 15:23:47 gilch Exp $";
   rl_sched_copyright!* :=
      "Copyright (c) 1995-1999 by A. Dolzmann and T. Sturm"
>>;

module rlsched;
% Reduce logic component scheduler. Submodule of [redlog]. Service and
% black-box scheduler possibly including AM interface construction.

rl_mkserv('subfof,'(dummy dummy),nil,nil,nil,nil);

rl_mkserv('identifyonoff,'(reval),nil,nil,'null,nil);

rl_mkserv('simpl,'(rl_simp),
   '(rl_a2s!-atl rl_a2s!-number),'((list) -1),'rl_s2a!-simpl,T);

rl_mkserv('thsimpl,'(rl_a2s!-atl),nil,nil,'rl_s2a!-atl,T);

rl_mkserv('lthsimpl,'(rl_a2s!-atl),nil,nil,'rl_s2a!-atl,nil);

rl_mkserv('pnf,'(rl_simp),nil,nil,'rl_mk!*fof,T);

rl_mkserv('apnf,'(rl_a2s!-posf),nil,nil,'rl_mk!*fof,T);

rl_mkserv('nnf,'(rl_simp),nil,nil,'rl_mk!*fof,T);

rl_mkserv('nnfnot,'(dummy),nil,nil,nil,nil);

rl_mkserv('cnf,'(rl_simp),nil,nil,'rl_mk!*fof,T);

rl_mkserv('dnf,'(rl_simp),nil,nil,'rl_mk!*fof,T);

rl_mkserv('ex,'(rl_simp),'(rl_a2s!-varl),'((list)),'rl_mk!*fof,T);

rl_mkserv('all,'(rl_simp),'(rl_a2s!-varl),'((list)),'rl_mk!*fof,T);

rl_mkserv('gqe,'(rl_simp),'(rl_a2s!-atl rl_a2s!-varl),'((list)
   (list)),'rl_s2a!-gqe,T);

rl_mkserv('gqea,'(rl_simp),'(rl_a2s!-atl rl_a2s!-varl),'((list)
   (list)),'rl_s2a!-gqea,T);

rl_mkserv('lqe,'(rl_simp rl_a2s!-atl rl_a2s!-pt),nil,nil,'rl_s2a!-gqe,T);

rl_mkserv('qe,'(rl_simp),'(rl_a2s!-atl),'((list)),'rl_s2a!-simpl,T);

rl_mkserv('qea,'(rl_simp),'(rl_a2s!-atl),'((list)),'rl_s2a!-qea,T);

rl_mkserv('atnum,'(rl_simp),nil,nil,'aeval,T);

rl_mkserv('qnum,'(rl_simp),nil,nil,'aeval,T);

rl_mkserv('gsc,'(rl_simp),'(rl_a2s!-atl),'((list)),'rl_s2a!-simpl,T);

rl_mkserv('gsd,'(rl_simp),'(rl_a2s!-atl),'((list)),'rl_s2a!-simpl,T);

rl_mkserv('gsn,'(rl_simp),'(rl_a2s!-atl),'((list)),'rl_s2a!-simpl,T);

rl_mkserv('opt,'(rl_a2s!-atl rl_a2s!-targfn),
   '(rl_a2s!-varl rl_a2s!-number),'((list) 8),'rl_s2a!-opt,T);

rl_mkserv('atl,'(rl_simp),nil,nil,'rl_s2a!-atl,T);

rl_mkserv('atml,'(rl_simp),nil,nil,
   function(lambda x; rl_s2a!-ml(x,'rl_mk!*fof)),T);

rl_mkserv('matrix,'(rl_simp),nil,nil,'rl_mk!*fof,T);

rl_mkserv('ifacl,'(rl_simp),nil,nil,'rl_s2a!-terml,T);

rl_mkserv('ifacml,'(rl_simp),nil,nil,
   function(lambda x; rl_s2a!-ml(x,'rl_s2a!-term)),T);

rl_mkserv('tab,'(rl_simp rl_a2s!-atl),nil,nil,'rl_mk!*fof,T);

rl_mkserv('atab,'(rl_simp),nil,nil,'rl_mk!*fof,T);

rl_mkserv('itab,'(rl_simp),nil,nil,'rl_mk!*fof,T);

rl_mkserv('qeipo,'(rl_simp),'(rl_a2s!-atl),'((list)),'rl_s2a!-simpl,T);

rl_mkserv('qews,'(rl_simp),'(rl_a2s!-atl),'((list)),'rl_s2a!-simpl,T);

rl_mkserv('gentheo,'(rl_a2s!-atl rl_simp),'(rl_a2s!-varl),'((list)),
   'rl_s2a!-gqe,T);

rl_mkserv('tnf,'(rl_simp rl_a2s!-terml),nil,nil,'rl_mk!*fof,T);

rl_mkserv('terml,'(rl_simp),nil,nil,'rl_s2a!-terml,T);

rl_mkserv('termml,'(rl_simp),nil,nil,
   function(lambda x; rl_s2a!-ml(x,'rl_s2a!-term)),T);

rl_mkserv('struct,'(rl_simp),'(rl_a2s!-id),'(v),'rl_s2a!-struct,T);

rl_mkserv('ifstruct,'(rl_simp),'(rl_a2s!-id),'(v),'rl_s2a!-struct,T);

rl_mkserv('varl,'(rl_simp),nil,nil,'rl_s2a!-varl,T);

rl_mkserv('fvarl,'(rl_simp),nil,nil,'rl_s2a!-fbvarl,T);

rl_mkserv('bvarl,'(rl_simp),nil,nil,'rl_s2a!-fbvarl,T);

rl_mkserv('decdeg1,'(rl_simp),'(rl_a2s!-decdeg1),'(fvarl),'rl_s2a!-decdeg1,T);

rl_mkserv('decdeg,'(rl_simp),nil,nil,'rl_mk!*fof,T);

rl_mkserv('explats,'(rl_simp),nil,nil,'rl_mk!*fof,T);

rl_mkserv('mkcanonic,'(rl_simp),nil,nil,'rl_mk!*fof,T);

rl_mkserv('surep,'(dummy dummy),nil,nil,nil,nil);

rl_mkserv('siaddatl,'(dummy dummy),nil,nil,nil,nil);

rl_mkserv('xqe,'(rl_simp),nil,nil,'rl_mk!*fof,T);

rl_mkserv('xqea,'(rl_simp),nil,nil,'rl_s2a!-qea,T);

rl_mkserv('cad,'(rl_simp),'(rl_a2s!-idlist),'((list)),
   function(lambda x; rl_mk!*fof cdr x),T);

rl_mkserv('gcad,'(rl_simp),'(rl_a2s!-idlist),'((list)),'rl_s2a!-gqe,T);

rl_mkserv('cadporder,'(rl_simp),nil,nil,'rl_s2a!-idlist,T);

rl_mkserv('gcadporder,'(rl_simp),nil,nil,'rl_s2a!-idlist,T);

rl_mkserv('cadproj,'(rl_simp),'(rl_a2s!-idlist),'((list)),
   function(lambda x; rl_s2a!-sflist cdr x),T);

procedure rl_s2a!-sflist(sfll);
   % . [sfl] is a list of SF.
   begin scalar fl,f;
      return 'list . for each fl in sfll collect
	 'list . for each f in fl collect prepf f
   end;

rl_mkserv('cadswitches,nil,nil,nil,function(lambda x; x),T);

rl_mkserv('expand,'(rl_simp),nil,nil,'rl_mk!*fof,T);

rl_mkserv('hqe,'(rl_simp),nil,nil,'rl_mk!*fof,T); 

rl_mkserv('ghqe,'(rl_simp),nil,nil,'rl_s2a!-ghqe,T); 

rl_mkserv('quine,'(rl_simp),nil,nil,'rl_mk!*fof,T);


% Black box scheduler.

rl_mkbb('rl_simplat1,2);

rl_mkbb('rl_smupdknowl,4);

rl_mkbb('rl_smrmknowl,2);

rl_mkbb('rl_smcpknowl,1);

rl_mkbb('rl_smmkatl,4);

rl_mkbb('rl_smsimpl!-impl,5);

rl_mkbb('rl_smsimpl!-equiv1,5);

rl_mkbb('rl_negateat,1);

rl_mkbb('rl_varlat,1);

rl_mkbb('rl_varsubstat,3);

rl_mkbb('rl_translat,5);

rl_mkbb('rl_elimset,2);

rl_mkbb('rl_trygauss,5);

rl_mkbb('rl_varsel,3);

rl_mkbb('rl_qemkans,2);

rl_mkbb('rl_ordatp,2);

rl_mkbb('rl_subsumption,3);

rl_mkbb('rl_transform,2);

rl_mkbb('rl_updatr,2);

rl_mkbb('rl_sacat,3);

rl_mkbb('rl_sacatlp,2);

rl_mkbb('rl_bnfsimpl,2);

rl_mkbb('rl_fctrat,1);

rl_mkbb('rl_tordp,2);

rl_mkbb('rl_a2cdl,1);

rl_mkbb('rl_t2cdl,1);

rl_mkbb('rl_subat,2);

rl_mkbb('rl_subalchk,1);

rl_mkbb('rl_eqnrhskernels,1);

rl_mkbb('rl_getineq,2);

rl_mkbb('rl_qefsolset,5);

rl_mkbb('rl_bettergaussp,2);

rl_mkbb('rl_bestgaussp,1);

rl_mkbb('rl_esetunion,2);

rl_mkbb('rl_structat,2);

rl_mkbb('rl_ifstructat,2);

rl_mkbb('rl_termmlat,1);

rl_mkbb('rl_multsurep,2);

rl_mkbb('rl_specelim,5);

rl_mkbb('rl_susipost,2);

rl_mkbb('rl_susitf,2);

rl_mkbb('rl_susibin,2);

rl_mkbb('rl_fbqe,1);

rl_mkbb('rl_qscsaat,1);

rl_mkbb('rl_qssubat,2);

rl_mkbb('rl_qsconsens,3);

rl_mkbb('rl_qstrycons,4);

rl_mkbb('rl_qsimpltestccl,3);

rl_mkbb('rl_qssubsumep,3);

rl_mkbb('rl_qstautp,1);

rl_mkbb('rl_qssusuat,3);

rl_mkbb('rl_qssiadd,4);

rl_mkbb('rl_qssimpl,3);

rl_mkbb('rl_b2terml,2);

rl_mkbb('rl_simplb,2);

rl_mkbb('rl_b2atl,2); 

rl_mkbb('rl_bsatp,1); 

endmodule;  % [rlsched]

end;  % of file