File r37/packages/redlog/rlsched.red artifact 682050c78f part of check-in fe6b5d0560

% ----------------------------------------------------------------------
% $Id: rlsched.red,v 1.23 1999/03/23 09:23:57 dolzmann Exp $
% ----------------------------------------------------------------------
% Copyright (c) 1995-1999 Andreas Dolzmann and Thomas Sturm
% ----------------------------------------------------------------------
% $Log: rlsched.red,v $
% 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.23 1999/03/23 09:23:57 dolzmann 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('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('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('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);

% 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);

endmodule;  % [rlsched]

end;  % of file