Artifact b5ea806a5d0ed1ff651fbaf5e68e8aa11d013943262ec7418cada3f9bcfcfb57:
- Executable file
r38/packages/redlog/clqe.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: 31680) [annotate] [blame] [check-ins using] [more...]
% ---------------------------------------------------------------------- % $Id: clqe.red,v 1.26 2003/12/02 15:31:19 sturm Exp $ % ---------------------------------------------------------------------- % Copyright (c) 1995-1999 Andreas Dolzmann and Thomas Sturm % ---------------------------------------------------------------------- % $Log: clqe.red,v $ % Revision 1.26 2003/12/02 15:31:19 sturm % Use ioto_nterpri for verbose output ("+ 4" is a most conservative guess). % % Revision 1.25 2003/01/31 15:31:52 sturm % Worked on verbosity output of QE routines. % % Revision 1.24 2002/08/23 12:32:10 dolzmann % Added local quantifier elimination. % % Revision 1.23 2002/05/28 13:21:54 sturm % Added black box rl_fbqe() and corresponding switch rlqefb. % That is, for ofsf, rlqe uses rlcad in case of failure now. % % Revision 1.22 2001/05/15 18:30:25 sturm % Changed eq on numbers to equal as Tony suggested. % % Revision 1.21 1999/04/13 13:11:00 sturm % Updated comments for exported procedures. % % Revision 1.20 1999/03/22 17:07:59 dolzmann % Changed copyright information. % Reformatted comments. % % Revision 1.19 1999/03/21 13:34:57 dolzmann % Changed error message in cl_qeipo1. % Adapted cl_qews to the changed protocol of rl_trygauss. % Use rl_qe instead of cl_qe in cl_qeipo1 and cl_qews1. % % Revision 1.18 1999/03/18 14:08:03 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.17 1999/01/17 15:36:43 dolzmann % Corrected some typos in the comments. % % Revision 1.16 1998/04/09 10:52:07 sturm % Removed scalar binding of argument bvl in procedure cl_trygauss. % % Revision 1.15 1997/10/02 09:14:06 sturm % Fixed a bug in answer computation with shift. % % Revision 1.14 1996/10/27 15:19:34 sturm % cl_qe and cl_qea did not pass the bvl argument to cl_qe1. % cl_qews1 did not pass the bvl argument to rl_trygauss. % % Revision 1.13 1996/10/23 12:02:37 sturm % Added "exceptionlist" paramter to rlgqe and rlgqea. Several quantifier % blocks are treated correctly now. % % Revision 1.12 1996/10/23 11:27:14 dolzmann % Added switch rlqevarsel and corresponding code. % % Revision 1.11 1996/10/07 11:45:53 sturm % Added fluids for CVS and copyright information. % % Revision 1.10 1996/09/29 14:22:21 sturm % Introduced services rlqea and rlgqea. % % Revision 1.9 1996/09/05 11:12:45 dolzmann % Rewritten procedure cl_qeblock2. % Fluid variable cl_identify!-atl!* is cleared before eliminating each % variable in each container element. % Added comments. % Implemented a deep Gauss elimination. % % Revision 1.8 1996/08/01 11:44:21 reiske % Added procedures cl_qeipo, cl_qews: quantifier elimination in position. % % Revision 1.7 1996/07/07 14:35:54 sturm % Turned some cl calls into service calls. % Removed use of fluid zehn!*. % % Revision 1.6 1996/06/07 08:53:16 sturm % Ignore answers when checking for equal container elements. % % Revision 1.5 1996/06/05 15:05:27 sturm % Split disjunctions when adding to the container, particularly in the % beginning. % Mind !*rlqegsd also in the beginning. % % Revision 1.4 1996/05/21 17:13:29 sturm % Removed binding of !*rl_siexpla in cl_gqe. % % Revision 1.3 1996/05/13 13:33:36 sturm % Added formula simplification using the simplified theory to cl_gqe. % % Revision 1.2 1996/05/12 08:26:55 sturm % Added procedure cl_gqe. % Procedure cl_qe turns on rlsipw and rlsipo. % Added code for generic branch computation. % % Revision 1.1 1996/03/22 10:31:31 sturm % Moved and split. % % ---------------------------------------------------------------------- lisp << fluid '(cl_qe_rcsid!* cl_qe_copyright!*); cl_qe_rcsid!* := "$Id: clqe.red,v 1.26 2003/12/02 15:31:19 sturm Exp $"; cl_qe_copyright!* := "(c) 1995-1999 by A. Dolzmann and T. Sturm" >>; module clqe; % Common logic quantifier elimination by elimination sets. Submodule % of [cl]. Currently restricted to quadratic formulas. %DS % <CONTAINER ELEMENT> ::= % (<VARLIST> . <FORMULA>) . (<ANSWER> . <ANSWER TRANSFORMATION>) % <VARLIST> ::= <VARIABLE LIST> | 'BREAK % <FORMULA> ::= "quantifier-free formula" % <ANSWER> ::= (<SUBST_TRIPLET>,...) "[nil] if not ans" % <SUBST_TRIPLET> ::= (<VARIABLE>, <SUBST_FUNCTION>, <ARGUMENT LIST>, <ATR>) % <ANSWER TRANSFORMATION> ::= "context dependent, [nil] if not ans" smacro procedure cl_mkcoel(vl,f,an,atr); % Common logic make container element. [vl] is a list of variables; % [f] is a quantifier-free formula; [an] is an answer; [atr] is an % answer transformation. (vl . f) . (an . atr); smacro procedure cl_covl(x); % Common logic container variable list. [x] is a container element. % Returns the variable list from [x]. caar x; smacro procedure cl_cof(x); % Common logic container formula. [x] is a container element. % Returns the formula from [x]. cdar x; smacro procedure cl_coan(x); % Common logic container answer. [x] is a container element. % Returns the answer from [x]. cadr x; smacro procedure cl_coatr(x); % Common logic container answer translation. [x] is a container % element. Returns the answer transformation from [x]. cddr x; smacro procedure cl_co2j(x); % Common logic container to junction. [x] is a container element. % Returns the S-expression [cl_cpf(x) . cl_coan(x) . cl_coatr(x)]. cdar x . cadr x . cddr x; procedure cl_comember(ce,l); % Common logic container memeber. [ce] is a container element; [l] % is a list of container elements. Returns non-[nil], if there is % an container element $e$ in [l], such that the formula and the % variable list of $e$ are equal to the formula and variable list % of [ce]. This procedure does not use the access functions! if l then car ce = caar l or cl_comember(ce,cdr l); procedure cl_gqe(f,theo,xbvl); % Common logic generic quantifier elimination. [f] is a formula; % [theo] is a THEORY; [xbvl] is a list of variables. Returns a pair % $\Theta . \phi$. $\Theta$ is a THEORY extending [theo] by % assumptions on free variables of [f] that are not in [xbvl]; % $\phi$ is a formula. We have $\Theta \models [f] % \longleftrightarrow \phi$. $\phi$ is obtained from [f] by % eliminating as much quantifiers as possible. Accesses the switch % [rlqepnf]; if [rlqepnf] is on, then [f] has to be prenex. begin scalar w,theo,!*rlqegen,!*rlsipw,!*rlsipo; !*rlsipw := !*rlqegen := T; w := cl_qe1(f,theo,xbvl); theo := rl_thsimpl car w; return theo . rl_simpl(cdr w,theo,-1) end; procedure cl_gqea(f,theo,xbvl); % Common logic generic quantifier elimination with answer. [f] is a % formula; [theo] is a THEORY; [xbvl] is a list of variables. % Returns a pair $\Theta . \Phi$. $\Theta$ is a THEORY extending % [theo] by assumptions on free variables of [f] that are not in % [xbvl]; $\Phi$ is a list $(..., (c_i, A_i), ...)$, where the % $c_i$ are quantifier-free formulas, and the $A_i$ are lists of % equations. We have $\Theta \models \bigvee_i c_i % \longleftrightarrow [f]$. Whenever some $c_i$ holds for an % interpretation of the parameters, then [f] holds, and $A_i$ % describes a satisfying sample point. Accesses the switch % [rlqepnf]; if [rlqepnf] is on, then [f] has to be prenex. begin scalar w,theo,!*rlqegen,!*rlsipw,!*rlsipo,!*rlqeans; !*rlsipw := !*rlqegen := !*rlqeans := T; w := cl_qe1(f,theo,xbvl); theo := rl_thsimpl car w; return theo . cdr w end; procedure cl_lqe(f,theo,pt); % Common logic local quantifier elimination. [f] is a formula; % [theo] is a THEORY; [pt] is a list of equations $v=z$, where $v$ % is a variable and $z$ is an INTEGER, namely the suggested value % for the local parameter $v$. Returns a pair $\Theta . \phi$. % $\Theta$ is a THEORY extending [theo]; $\phi$ is a formula. We % have $\Theta \models [f] \longleftrightarrow \phi$. $\phi$ is % obtained from [f] by eliminating as much quantifiers as possible. % Accesses the switch [rlqepnf]; if [rlqepnf] is on, then [f] has % to be prenex. Accesses the fluids [cl_pal!*], [cl_lps!*], and % [cl_theo!*]. [cl_lps!*] is the list of local parameters; [cl_pal] % is a ALIST containing the suggested values for the local % parameters; and [cl_theo!*] is the theory generated by the local % quantifier elimination. begin scalar w,theo,!*rlqelocal,!*rlsipw,!*rlsipo,cl_pal!*,cl_lps!*, cl_theo!*; !*rlsipw := !*rlqelocal := T; cl_pal!* := pt; cl_lps!* := for each x in pt collect car x; cl_theo!* := nil; w := for each x in theo collect rl_subat(cl_pal!*,x); w := rl_simpl(rl_smkn('and,w),nil,-1); if w eq 'false then rederr "rllqe: inconsistent theory"; w := cl_qe1(f,theo,nil); theo := nconc(cl_theo!*,theo); w := cdr w; cl_pal!* := cl_lps!* := cl_theo!* := nil; return rl_lthsimpl(theo) . rl_simpl(w,theo,-1) end; procedure cl_qe(f,theo); % Common logic quantifier elimination. [f] is a formula; [theo] is % a THEORY. Returns a formula $\phi$. We have $[theo] \models [f] % \longleftrightarrow \phi$. $\phi$ is obtained from [f] by % eliminating as much quantifiers as possible. Accesses the switch % [rlqepnf]; if [rlqepnf] is on, then [f] has to be prenex. begin scalar !*rlsipw,!*rlsipo; !*rlsipw := !*rlsipo := T; return cl_qe1(f,theo,nil) end; procedure cl_qea(f,theo); % Common logic quantifier elimination with answer. [f] is a % formula; [theo] is a THEORY. Returns a list of pairs $(..., (c_i, % A_i), ...)$. The $c_i$ are quantifier-free formulas, and the % $A_i$ are lists of equations. We have $[theo] \models \bigvee_i % c_i \longleftrightarrow [f]$. Whenever some $c_i$ holds for an % interpretation of the parameters, [f] holds, and $A_i$ describes % a satisfying sample point. Accesses the switch [rlqepnf]; if % [rlqepnf] is on, then [f] has to be prenex. begin scalar !*rlsipw,!*rlsipo,!*rlqeans; !*rlsipw := !*rlsipo := !*rlqeans := T; return cl_qe1(f,theo,nil) end; procedure cl_qe1(f,theo,xbvl); % Common logic quantifier elimination. [f] is a linear formula % which is prenex if the switch [rlqepnf] is off; [theo] is a list % of atomic formulas, which serve as background theory. If the % switch [rlqeans] and [rlqegen] is off a quantifier-free % equivalent of [f] is returned. With [rlqeans] on, a list % $(...(c_i,a_i)...)$ is returned, where the $c_i$ are % quantifier-free formulas, and the $a_i$ are lists of equations. % With [rlqegen] on, a pair $(\theta . \phi)$ is returned, such % that $\Theta \models [f] \longleftrightarrow \phi$. begin scalar svrlidentify,q,op,ql,varl,varll,delvarl,answer,result; if !*rlqepnf then f := rl_pnf f; f := rl_simpl(f,theo,-1); if f eq 'inctheo then return 'inctheo; if not rl_quap rl_op f then << result := if !*rlqeans then {{f,nil}} else f; if !*rlqegen or !*rlqelocal then result := theo . result; return result >>; % Split [f] into its matrix, a quantifier list, a list of % variable lists, and a list off all quantified variables. q := op := rl_op f; repeat << if op neq q then << ql := q . ql; varll := varl . varll; q := op; varl := nil >>; varl := rl_var f . varl; delvarl := rl_var f . delvarl; f := rl_mat f >> until not rl_quap(op := rl_op f); ql := q . ql; varll := varl . varll; % Remove atomic formulas containing quantified variables from % the theory theo := for each atf in theo join if null intersection(rl_varlat atf,delvarl) then {atf}; % Iteratively apply [cl_qeblock] to the quantifier blocks. svrlidentify := !*rlidentify; answer := nil . nil; while null car answer and ql do << on1 'rlidentify; q := car ql; ql := cdr ql; varl := car varll; varll := cdr varll; if !*rlverbose then ioto_tprin2 {"---- ",(q . reverse varl)}; answer := cl_qeblock( f,q,varl,theo,!*rlqeans and null ql,union(delvarl,xbvl)); theo := cdr answer; answer := car answer; f := cdr answer; off1 'rlidentify >>; onoff('rlidentify,svrlidentify); % Requantify with the variables that could not be eliminated. if car answer then << if !*rlqeans then rederr "cl_qe: requantification impossible"; for each v in car answer do f := rl_mkq(q,v,f); for each q in ql do << varl := car varll; varll := cdr varll; for each v in varl do f := rl_mkq(q,v,f) >>; >>; result := if !*rlqeans then for each x in f collect {car x,rl_qemkans(cadr x,cddr x)} else << if !*rlqefb and car answer then << if !*rlverbose then ioto_tprin2 {"++++ Entering fallback QE: "}; f := rl_fbqe f >>; rl_simpl(f,theo,-1) >>; if !*rlqegen or !*rlqelocal then result := theo . result; return result end; procedure cl_qeblock(f,q,varl,theo,ans,bvl); % Common logic quabtifier eliminate block. [f] is a quantifier-free % formula; [q] is a quantifier; [varl] is a variable list; [theo] % is the current theory; [ans] is Boolean. begin scalar w; if q eq 'ex then return cl_qeblock1(rl_simpl(f,theo,-1),varl,theo,ans,bvl); % [q eq 'all] w := cl_qeblock1(rl_simpl(rl_nnfnot f,theo,-1),varl,theo,ans,bvl); theo := cdr w; w := car w; if ans then return (car w . for each x in cdr w collect rl_nnfnot car x . cdr x) . theo; return (car w . rl_nnfnot cdr w) . theo end; procedure cl_qeblock1(f,varl,theo,ans,bvl); % Common logic quantifier eliminate block 1. if !*rlqeheu then cl_qeblock2(f,varl,theo,ans,bvl) else cl_qeblock3(f,varl,theo,ans,bvl); procedure cl_qeblock2(f,varl,theo,ans,bvl); % Common logic quantifier eliminate block 2. [f] is a % quantifier-free formula; [varl] is a list of variables; [theo] is % a list of atomic formulas; [ans] is bool. With [rlqeheu] on, % check for decision problem. begin scalar !*rlqedfs,atl; atl := cl_atl1 f; !*rlqedfs := T; while atl do if setdiff(rl_varlat car atl,varl) then !*rlqedfs := atl := nil else atl := cdr atl; return cl_qeblock3(f,varl,theo,ans,bvl) end; procedure cl_qeblock3(f,varl,theo,ans,bvl); % Common logic quantifier eliminate block 3. [f] is a % quantifier-free formula; [varl] is a list of variables; [theo] is % a list of atomic formulas; [ans] is bool. begin scalar w,co,remvl,newj,cvl,coe; integer c,vlv,dpth,count,delc,oldcol; if !*rlverbose then << dpth := length varl; if !*rlqedfs then << vlv := dpth / 4; ioto_prin2t {" [DFS: depth ",dpth,", watching ",dpth - vlv,"]"} >> else ioto_prin2t {" [BFS: depth ",dpth,"]"} >>; cvl := varl; if !*rlqegsd then f := rl_gsd(f,theo); if rl_op f = 'or then for each x in rl_argn f do co := cl_save(co,{cl_mkcoel(cvl,x,nil,nil)}) else co := cl_save(co,{cl_mkcoel(cvl,f,nil,nil)}); while co do << on1 'rlidentify; w := cl_get(co); co := cdr w; coe := car w; cvl := cl_covl coe; count := count+1; if !*rlverbose then if !*rlqedfs then << if vlv = length cvl then ioto_tprin2t {"-- crossing: ",dpth - vlv}; ioto_prin2 {"[",dpth - length cvl} >> else << if c=0 then << ioto_tprin2t {"-- left: ",length cvl}; c := cl_colength(co) + 1 >>; ioto_nterpri(length explode c + 4); ioto_prin2 {"[",c}; c := c - 1 >>; w := cl_qevar( cl_cof coe,cl_covl coe,cl_coan coe,cl_coatr coe,theo,ans,bvl); theo := cdr w; w := car w; if car w then << % We have found a suitable variable. w := cdr w; if w then if cl_covl car w eq 'break then << co := nil; newj := {cl_co2j car w} >> else if cdr cvl then << if !*rlverbose then oldcol := cl_colength(co); co := cl_save(co,w); if !*rlverbose then delc := delc + oldcol + length w - cl_colength(co) >> else for each x in w do newj := lto_insert(cl_co2j x,newj) >> else << % There is no eliminable variable. % Invalidate this entry, and save its variables for later % requantification. if !*rlverbose then ioto_prtmsg("+++" . cdr w); remvl := union(cvl,remvl); newj := lto_insert(cl_co2j coe,newj) >>; if !*rlverbose then << ioto_prin2 "] "; if !*rlqedfs and null cvl then ioto_prin2 ". " >> >>; if !*rlverbose then ioto_prin2{"[DEL:",delc,"/",count,"]"}; if ans then return (remvl . newj) . theo; return (remvl . rl_smkn('or,for each x in newj collect car x)) . theo end; procedure cl_qevar(f,vl,an,atr,theo,ans,bvl); % Quantifier eliminate one variable. [f] is a quantifier-free % formula; [vl] is a non-empty list of variables; [an] is an % answer; [theo] is a list of atomic formulas; [ans] is Boolean. % Returns a pair $a . p$. Either $a=[T]$ and $p$ is a pair of a % list of container elements and a theory or $a=[nil]$ and $p$ is % an error message. If there is a container element with ['break] % as varlist, this is the only one. begin scalar w,v,alp,hit,ww; for each vv in vl do if cdr (w := rl_transform(f,vv)) then << hit := T; f := car w; atr := rl_updatr(atr,cdr w) >>; if hit then f := rl_simpl(f,theo,-1); w := rl_trygauss(f,vl,theo,ans,bvl); if w neq 'failed then << theo := cdr w; w := car w; if !*rlverbose then ioto_prin2 "g"; vl := delq(car w,vl); ww := cl_esetsubst(f,car w,cdr w,vl,an,atr,theo,ans,bvl); if !*rlqelocal then return (T . car ww) . cl_theo!* else return (T . car ww) . cdr ww >>; w := rl_specelim(f,vl,theo,ans,bvl); if w neq 'failed then return w; % elimination set method if !*rlqevarsel then v := rl_varsel(f,vl,theo) else v := car vl; vl := delq(v,vl); alp := cl_qeatal(f,v,theo,ans); if car alp = 'failed then return (nil . cdr alp) . theo; if alp = '(nil . nil) then << % [v] does not occur in [f]. if !*rlverbose then ioto_prin2 "*"; return (T . {cl_mkcoel(vl,f,ans and an,ans and atr)}) . theo >>; if !*rlverbose then ioto_prin2 "e"; ww := cl_esetsubst(f,v,rl_elimset(v,alp),vl,an,atr,theo,ans,bvl); if !*rlqelocal then return (T . car ww) . cl_theo!* else return (T . car ww) . cdr ww end; procedure cl_esetsubst(f,v,eset,vl,an,atr,theo,ans,bvl); % Common logic elimination set substitution. [f] is a % quantifier-free formula; [v] is a kernel; [eset] is an % elimination set; [an] is an answer; [atr] in an answer % translation; [theo] is the current theory; [ans] is Boolean. % Returns a pair $l . \Theta$, where $\Theta$ is the new theory and % $l$ is a list of container elements. If there is a container % element with ['break] as varlist, this is the only one. begin scalar a,d,u,elimres,junct,bvl,w; while eset do << a := caar eset; d := cdar eset; eset := cdr eset; while d do << u := car d; d := cdr d; w := apply(a,bvl . theo . f . v . u); theo := union(theo,car w); elimres := rl_simpl(cdr w,theo,-1); if !*rlqegsd then elimres := rl_gsd(elimres,theo); if elimres eq 'true then << junct := {cl_mkcoel('break,elimres, cl_updans(v,a,u,an,atr,ans),ans and atr)}; eset := d := nil >> else if elimres neq 'false then if rl_op elimres eq 'or then for each subf in rl_argn elimres do junct := cl_mkcoel(vl,subf, cl_updans(v,a,u,an,atr,ans),ans and atr) . junct else junct := cl_mkcoel(vl,elimres, cl_updans(v,a,u,an,atr,ans),ans and atr) . junct; >> >>; return junct . theo end; procedure cl_updans(v,a,u,an,atr,ans); ans and {v,a,u,atr} . an; procedure cl_qeatal(f,v,theo,ans); % Common logic quantifier elimination atomic formula list. [f] is a % formula; [v] is avariable; [theo] is the current theory, [ans] is % Boolean. Returns an ALP. cl_qeatal1(f,v,theo,T,ans); procedure cl_qeatal1(f,v,theo,flg,ans); % Common logic quantifier elimination ataomic formula list. [f] is % aformula; [v] is avariable; [theo] is the current theory, [flg] % and [ans] are Boolean. Returns an ALP. If [flg] is non-[nil] [f] % has to be considered negated. begin scalar op,w,ww; op := rl_op f; w := if rl_tvalp op then {nil . nil} else if op eq 'not then {cl_qeatal1(rl_arg1 f,v,theo,not flg,ans)} else if rl_junctp op then for each subf in rl_argn f collect cl_qeatal1(subf,v,theo,flg,ans) else if op eq 'impl then {cl_qeatal1(rl_arg2l f,v,theo,not flg,ans), cl_qeatal1(rl_arg2r f,v,theo,flg,ans)} else if op eq 'repl then {cl_qeatal1(rl_arg2l f,v,theo,flg,ans), cl_qeatal1(rl_arg2r f,v,theo,not flg,ans)} else if op eq 'equiv then {cl_qeatal1(rl_arg2l f,v,theo,not flg,ans), cl_qeatal1(rl_arg2r f,v,theo,flg,ans), cl_qeatal1(rl_arg2l f,v,theo,flg,ans), cl_qeatal1(rl_arg2r f,v,theo,not flg,ans)} else if rl_quap op then rederr "argument formula not prenex" else % [f] is an atomic formula. {rl_translat(f,v,theo,flg,ans)}; if (ww := atsoc('failed,w)) then return ww; return cl_alpunion w end; procedure cl_alpunion(pl); % Common logic ALP union. [pl] is a list of ALP's. Returns the % union of all ALP's in [pl]. begin scalar uall,pall; for each pair in pl do << uall := car pair . uall; pall := cdr pair . pall >>; return lto_alunion(uall) . lto_almerge(pall,'plus2) end; procedure cl_save(co,dol); % Common logic save into container. [co] is a container; [dol] is a % list of container elements. Returns a container. if !*rlqedfs then cl_push(co,dol) else cl_enqueue(co,dol); procedure cl_push(co,dol); % Common logic push into container. [co] is a container; [dol] is a % list of container elements. Returns a container. << for each x in dol do co := cl_coinsert(co,x); co >>; procedure cl_coinsert(co,ce); % Common logic insert into container. [co] is a container; [ce] is % a container element. Returns a container. if cl_comember(ce,co) then co else ce . co; procedure cl_enqueue(co,dol); % Common logic enqueue into container. [co] is a container; [dol] % is a list of container elements. Returns a container. << if null co and dol then << co := {nil,car dol}; car co := cdr co; dol := cdr dol >>; for each x in dol do if not cl_comember(x,cdr co) then car co := (cdar co := {x}); co >>; procedure cl_get(co); % Common logic get from container. [co] is a container. Returns a % pair $(e . c)$ where $e$ is a container element and $c$ is the % container [co] without the entry $e$. if !*rlqedfs then cl_pop(co) else cl_dequeue(co); procedure cl_pop(co); % Common logic pop from container. [co] is a container. Returns a % pair $(e . c)$ where $e$ is a container element and $c$ is the % container [co] without the entry $e$. co; procedure cl_dequeue(co); % Common logic dequeue from container. [co] is a container. Returns % a pair $(e . c)$ where $e$ is a container element and $c$ is the % container [co] without the entry $e$. if co then cadr co . if cddr co then (car co . cddr co); procedure cl_colength(co); % Common logic container length. [co] is a container. Returns the % number of elements in [co]. if !*rlqedfs or null co then length co else length co - 1; procedure cl_qeipo(f,theo); % Common logic quantifier elimination in position. [f] is a % positive formula; [theo] is a THEORY. Returns a quantifier-free % formula equivalent to [f] wrt. [theo] by recursively making [f] % anti-prenex and eliminating the quantifiers. begin scalar w,!*rlqeans; repeat << w := cl_qeipo1(cl_apnf rl_simpl(f,theo,-1),theo); f := cdr w >> until not car w; return f end; procedure cl_qeipo1(f,theo); % Quantifier eliminate in position subroutine. begin scalar op,nf,a,argl,ntheo; op := rl_op f; if rl_quap op then << for each subf in theo do if not(rl_var f memq rl_varlat subf) then ntheo := subf . ntheo; nf := cl_qeipo1(rl_mat f,ntheo); if car nf then return T . rl_mkq(op,rl_var f,cdr nf); a := rl_qe(rl_mkq(op,rl_var f,cdr nf),ntheo); if rl_quap rl_op a then rederr "cl_qeipo1: Could not eliminate quantifier"; return T . a >>; if rl_junctp op then << argl := rl_argn f; if op eq 'and then for each subf in argl do if cl_atfp subf then theo := subf . theo; if op eq 'or then for each subf in argl do if cl_atfp subf then theo := rl_negateat subf . theo; while argl do << a := cl_qeipo1(car argl,theo); nf := cdr a . nf; argl := cdr argl; if car a then << nf := nconc(reversip nf,argl); argl := nil >> >>; return if car a then T . rl_mkn(op,nf) else nil . rl_mkn(op,reversip nf) >>; % f is atomic. return nil . f end; procedure cl_qews(f,theo); % Common logic quantifier elimination with selection. [f] is a % formula; [theo] is a THEORY. Returns a quantifier-free formula % equivalent to [f] wrt. [theo] by selecting a quantifier from the % innermost block, moving it inside as far as possible and % eliminating it. Accesses the switch [rlqepnf]; if [rlqepnf] is % on, then [f] has to be prenex. begin scalar q,op,ql,varl,varll,!*rlqeans; if !*rlqepnf then f := rl_pnf f; f := rl_simpl(f,theo,-1); if not rl_quap rl_op f then return f; % Split [f] into its matrix, a quantifier list, and a list of % variable lists. q := rl_op f; while rl_quap(op:=rl_op f) do << if op neq q then << ql := q . ql; varll := varl . varll; q := op; varl := nil >>; varl := rl_var f . varl; f := rl_mat f; >>; ql := q . ql; varll := varl . varll; while ql do << q := car ql; ql := cdr ql; varl := car varll; varll := cdr varll; if q eq 'ex then f := cl_qews1(varl,f,theo) else f := rl_nnfnot cl_qews1(varl,rl_nnfnot f,theo) >>; return f end; procedure cl_qews1(varl,mat,theo); % Common logic quantifier eliminate with selection subroutine. % [varl] is a list of variables; [mat] is a quantifier-free % formula; [theo] is a list of atomic formulas. Returns a formula, % where all existentially quantified variables from [varl] are % eliminated. begin scalar v,w; while varl do << w := rl_trygauss(mat,varl,theo,nil,nil); if w eq 'failed then << v := rl_varsel(mat,varl,theo); mat := cl_qeipo(rl_mkq('ex,v,mat),theo) >> else << v := caar w; mat := rl_qe(rl_mkq('ex,v,mat),theo) >>; varl := delete(v,varl) >>; return mat end; %DS % <GRV> ::= ['failed] | (<KERNEL> . <ELIMINATION SET>) . <THEORY> % <IGRV> ::= (['failed] . [nil]) | % ['gignore] . ([nil] . <THEORY SUPPLEMENT>) | % <GAUSS TYPE IDENTIFICATION> . (<ELIMINATION SET> . <THEORY SUPPLEMENT>) % <GAUSS TYPE IDENTIFICATION> ::= ("verbose output", <DATA>,...) procedure cl_trygauss(f,vl,theo,ans,bvl); % Common logic try Gauss elimination. [f] is a quantifier-free % formula; [vl] is a list of variables existentially quantified in % the current block; [theo] a THEORY; [ans] is bool; [bvl] is a % list of variables. Returns a GRV, where no assumption on the % variables in [bvl] are made. begin scalar w; w := cl_trygauss1(f,vl,theo,ans,bvl); if w eq 'failed then return 'failed; return car w . union(cdr w,theo) end; procedure cl_trygauss1(f,vl,theo,ans,bvl); % Try deep Gauss elimination. [f] is a quantifier-free formula; [vl] is % the current existential variable block; [theo] is a list of % atomic formulas, the current theory; [ans] is Boolean; [bvl] is a % list of variables that are considered non-parametric. Returns % a GRV. begin scalar w,v,csol,ev; csol := '(failed . nil); if null !*rlqevarsel then vl := {car vl}; while vl do << v := car vl; vl := cdr vl; w := cl_trygaussvar(f,v,theo,ans,bvl); if car w neq 'gignore and rl_bettergaussp(w,csol) then << csol := w; ev := v; if rl_bestgaussp(csol) then vl := nil; >>; >>; if car csol eq 'failed then return 'failed; if !*rlverbose then ioto_prin2 caar csol; return (ev . cadr csol) . cddr csol; end; procedure cl_trygaussvar(f,v,theo,ans,bvl); % Try Gauss elimination wrt. one variable. [f] is a formula; [v] % is a kernel; [theo] is a theory; [ans] is Boolean; [bvl] is a % list of kernels. Returns a IGRV. << if cl_atfp f then rl_qefsolset(f,v,theo,ans,bvl) else if rl_op f eq 'and then cl_gaussand(rl_argn f,v,theo,ans,bvl) else if rl_op f eq 'or then cl_gaussor(rl_argn f,v,theo,ans,bvl) else % TODO: Gauss elimination for formulas with extended Boolean op's '(failed . nil) >>; procedure cl_gaussand(fl,v,theo,ans,bvl); begin scalar w, curr; curr := cl_trygaussvar(car fl,v,theo,ans,bvl); fl := cdr fl; while fl and not(rl_bestgaussp curr) do << w := cl_trygaussvar(car fl,v,theo,ans,bvl); curr := cl_gaussintersection(w,curr); fl := cdr fl >>; return curr end; procedure cl_gaussor(fl,v,theo,ans,bvl); begin scalar w,curr; curr := cl_trygaussvar(car fl,v,theo,ans,bvl); fl := cdr fl; while fl and (car curr neq 'failed) do << w := cl_trygaussvar(car fl,v,theo,ans,bvl); fl := cdr fl; curr := cl_gaussunion(curr,w) >>; return curr end; procedure cl_gaussunion(grv1,grv2); begin scalar tag,eset,theo; if car grv1 eq 'failed or car grv2 eq 'failed then return '(failed . nil); tag := if car grv1 eq 'gignore then car grv2 else if car grv2 eq 'gignore then car grv1 else if rl_bettergaussp(grv1,grv2) then car grv2 else car grv1; eset := rl_esetunion(cadr grv1,cadr grv2); theo := union(cddr grv1,cddr grv2); return tag . ( eset . theo ) end; procedure cl_gaussintersection(grv1,grv2); if car grv1 eq 'gignore and car grv2 eq 'gignore then if length cddr grv1 < length cddr grv2 then grv1 else grv2 else if car grv1 eq 'gignore then grv2 else if car grv2 eq 'gignore then grv1 else if rl_bettergaussp(grv1,grv2) then grv1 else grv2; procedure cl_specelim(f,vl,theo,ans,bvl); % Common logic special elimination. [f] is a quantifier-free % formula; [vl] is a list of variables existentially quantified in % the current block; [theo] a THEORY; [ans] is bool; [bvl] is a % list of variables. Returns a GRV. 'failed; procedure cl_fbqe(f); % Common logic fallback quantifier elimination. [f] is a formula. % returns a formula equivalent to [f]. << if !*rlverbose then ioto_prin2t "no fallback QE specified"; f >>; endmodule; % [clqe] end; % of file