% ----------------------------------------------------------------------
% $Id: pasf.red,v 1.57 2004/02/22 21:08:15 lasaruk Exp $
% ----------------------------------------------------------------------
% Copyright (c) 2002 Andreas Dolzmann, Andreas Seidl, and Thomas Sturm
% ----------------------------------------------------------------------
% $Log: pasf.red,v $
% Revision 1.57 2004/02/22 21:08:15 lasaruk
% Added switch rlsusisubst for substitution of equalities. Substitution
% results in smaller formulas or formulas with less free variables.
% Up to 80% length reduction. Switch rlsusitr should not be used yet.
%
% Revision 1.56 2003/12/30 10:25:56 lasaruk
% Fixed bug in pasf_resimpat that caused crashes after value substitutions
%
% Revision 1.55 2003/12/11 15:24:02 sturm
% Switch on rlsusi for this context.
%
% Revision 1.54 2003/12/11 10:51:19 lasaruk
% Smart simplification improoved.
%
% Revision 1.53 2003/12/02 14:36:31 sturm
% Witch rlpasfvb off by default!
%
% Revision 1.52 2003/11/28 12:59:38 sturm
% Print congruences as ~n~ instead of =n= to avoid confusion.
%
% Revision 1.51 2003/11/07 12:08:12 sturm
% Improved printing.
%
% Revision 1.50 2003/11/05 13:56:19 lasaruk
% Some more changes. pasf_content renamed to pasf_gcd with more
% exact specificaton. lisp, symbolic and some "comments" are removed.
%
% Revision 1.49 2003/11/05 13:27:14 lasaruk
% Some major redlog programming rules applied to the code.
% Formulas are made positive acc. to the current kernel order.
%
% Revision 1.48 2003/10/16 16:17:38 lasaruk
% Compiler error messages partially removed. All others are due
% to the noncompleteness of packet.
%
% Revision 1.47 2003/10/12 19:41:11 sturm
% Introduced rl_texmacs. The test "if get('or,'fancy!-infix!-symbol) = 218"
% does not work in general since Windows does not guarantee to load
% fmprint at startup.
%
% Revision 1.46 2003/10/12 18:26:14 sturm
% Printing for both fmprint and tmprint in pasf now.
% The test is done via "if get('or,'fancy!-infix!-symbol) = 218" for now.
% IBALP printing remains to be adapted.
%
% Revision 1.45 2003/10/12 16:53:26 sturm
% Texmacs fancy-printing crashed Windows. Substituted fancy procedures
% by less fancy but working ones for now.
%
% Revision 1.44 2003/09/09 10:56:17 lasaruk
% check for correct form improoved
%
% Revision 1.43 2003/09/02 07:22:41 seidl
% Changed fancyprinting for TeXmacs from division to congruence.
%
% Revision 1.42 2003/08/28 15:30:40 lasaruk
% Simplification verbose output done better. QE-Bug with truth values
% corrected (will be done more effitient). Some fancy examples added.
%
% Revision 1.41 2003/08/27 16:10:04 lasaruk
% Added switch rlpasfatfsimpvb to print out simplification steps if
% simplification was really done. Check for correct PASF form added.
%
% Revision 1.40 2003/08/21 14:52:02 seidl
% Fancy printing for bounded quantifiers (for TeXmacs).
%
% Revision 1.39 2003/08/19 09:36:11 seidl
% Defined blackbox "bsatp" to be pasf_qff2ivl; there could be a more
% efficient implementation. Introduced temporarly switch rlsiverbose,
% which provides verbose output for rules (TV), (EQ), (SB), (SM), (STRB)
% during simplification of bounded quantifiers.
%
% Revision 1.38 2003/08/14 21:44:38 seidl
% Simplification of bounded quantifiers looks quite good now. A hack has
% to be cured by a blackbox bsatp (bound sat. predicate). rlsism can be
% savely turned on now in pasf, but there is a problem with susi and
% congruences.
%
% Revision 1.37 2003/07/22 08:45:03 seidl
% Improved simplifiations of equations and negated equations. Still there
% can be done more. Simplification of atomic formulas has to be thoroughly
% revised.
%
% Revision 1.36 2003/07/21 21:57:41 seidl
% Intermediate check-in. Part of advanced smart simplification works
% already.
%
% Revision 1.35 2003/07/17 16:12:20 lasaruk
% Congruence bug removed. Printing methods for congruences rewritten.
%
% Revision 1.34 2003/07/16 13:50:47 lasaruk
% Debug messages removed. Bug in printing congurences removed.
% Testfile adjusted to changes (working cases).
%
% Revision 1.33 2003/07/16 12:43:44 lasaruk
% conflicts resolved. pasf_simpl removed. implementation of
% pasf_simplb and pasf_b2terml added and tested.
% temporary method for pasf_b2terml in algebraic mode added.
% empty list bug in pasf_ivl2qff removed.
% expansion method uses now pasf_b2terml. some comments done
% better.
%
% Revision 1.32 2003/07/15 12:40:41 seidl
% Renamed pasf_iv2qff to pasf_ivl2qff and pasf_qff2iv to pasf_qff2ivl.
% Provided algebraic mode access to simplb, ivl2qff, qdd2ivl. Changed
% pasf_mkrng so intervals with same upper and lower bound result in an
% equation. Fixed serious bug in pasf_prepat. Added cvs header to
% pasf.tst. Todo Lasaruk: pasf_ivl2qff crashes with empty interval as
% argument, see testfile.
%
% Revision 1.31 2003/07/14 12:37:58 lasaruk
% Common utilities attached and tested (see the testfile).
%
% Revision 1.30 2003/06/04 12:33:40 lasaruk
% Some smaller modifications.
%
% Revision 1.29 2003/05/22 22:00:58 lasaruk
% DNF added.
%
% Revision 1.28 2003/05/17 16:27:56 lasaruk
% Pasf simplification added. Some errors corrected.
%
% Revision 1.27 2003/04/20 12:04:04 lasaruk
% Completely removed any reference to range predicates (in input
% also). PNF made shorter.
%
% Revision 1.26 2003/04/14 10:11:39 lasaruk
% Changes to work with bounded quantifieres added . Simplification bug
% (content) removed. Range predicates removed.
%
% Revision 1.25 2003/03/26 11:19:23 lasaruk
% Formula runthrough rewritten as cl_atnum. True/false in rlexpabnd bug
% removed. Some services added.
%
% Revision 1.24 2003/03/11 00:41:29 lasaruk
% Prenex normal form with correct range predicate handling added. Documentation
% extended. Todo section added.
%
% Revision 1.23 2003/03/04 09:33:23 lasaruk
% Advanced simplification. PNF code attached but not used yet. Some code
% migration. Documentation debugged.
%
% Revision 1.22 2003/02/17 10:55:40 lasaruk
% Stable full featured version
%
% Revision 1.21 2003/02/01 07:38:33 lasaruk
% Recursive range expansion.
%
% Revision 1.20 2003/01/31 14:09:17 lasaruk
% Test for range predicate check added.
%
% Revision 1.19 2003/01/30 11:48:26 sturm
% Fixed bugs in operator declaration for congruences and range.
% Changed output routine for range.
%
% Revision 1.18 2003/01/29 15:24:47 sturm
% Added service rlexpand for context pasf. Had to split pasf_exprng for this.
%
% Revision 1.17 2003/01/29 15:06:52 sturm
% Made rlsism a context switch. It has to be off in this context for now.
%
% Revision 1.16 2003/01/27 17:40:01 lasaruk
% Switches renamed. Bugs in docu fixed.
%
% Revision 1.15 2003/01/26 17:49:37 lasaruk
% Null congruence error added. Terms without quant. varl. stay
% untouched. Bugs fixed.
%
% Revision 1.14 2003/01/21 10:43:34 lasaruk
% logging changed to verbose
%
% Revision 1.13 2003/01/20 10:35:56 lasaruk
% Switches pasf_logging and pasf_rangeexpand added.
% WARNING: Actually block elimination does not work in not expansion mode.
%
% Revision 1.12 2002/12/23 07:06:33 lasaruk
% operator pasf_opn and pasf_op differed
%
% Revision 1.11 2002/12/10 08:49:41 lasaruk
% Correct elimination of an exist. quantifier call added.
% Procedures debugged.
%
% Revision 1.10 2002/12/02 12:53:37 lasaruk
% Elimination of one variable in front of an ex quantifier. Not really
% worth looking at.
%
% Revision 1.9 2002/10/18 13:39:11 lasaruk
% QE one variable preparation added. No bounded quantifiers first.
%
% Revision 1.8 2002/10/10 09:09:20 lasaruk
% Range predicate implemented. Todo: logical negation of range predicate
%
% Revision 1.7 2002/10/02 14:31:19 lasaruk
% Initial check in. Only dummy methods for advanced simplification first.
%
% Revision 1.6 2002/09/26 14:54:55 lasaruk
% Errors corrected. Negation form implemented.
%
% Revision 1.5 2002/09/26 10:47:31 lasaruk
% Prenex normal form functionality added. Tests follow.
%
% Revision 1.4 2002/09/19 08:49:42 lasaruk
% All operators are binary. Before printing modulus of cong and ncong is
% put directly after the operator. Ordering corrected.
%
% Revision 1.3 2002/09/16 10:49:55 lasaruk
% Testversion for cong and ncong with dotted pair operator and 2 parameters.
%
% Revision 1.2 2002/08/23 08:07:19 seidl
% Added service rl_atl with trival black box rl_ordatp.
% Created module pasfmisc for this.
%
% Revision 1.1 2002/08/22 14:01:54 sturm
% Initial check-in.
%
% ----------------------------------------------------------------------
lisp <<
fluid '(pasf_rcsid!* pasf_copyright!*);
pasf_rcsid!* := "$Id: pasf.red,v 1.57 2004/02/22 21:08:15 lasaruk Exp $";
pasf_copyright!* :=
"Copyright (c) 1995-2002 by A. Dolzmann, A. Seidl, and T. Sturm"
>>;
module pasf;
% Presburger arithmetic standard form. Main module. Algorithms on
% first-order formulas over the language of rings together with
% congruences, i.e., binary relations [equal], [neq], [cong], [ncong],
% [leq], [geq], [lessp], [greaterp]. The terms are SF's.
create!-package('(pasf pasfbnf pasfmisc pasfnf pasfsiat pasfqe pasfsism),nil);
load!-package 'cl;
load!-package 'rltools;
imports rltools,cl;
fluid '(!*rlverbose);
flag('(pasf),'rl_package);
% Switches
switch rlpasfrangeexpand;
switch rlpasfvb;
switch rlpasfsimplify;
switch rlsiverbose;
switch rlsusitr;
switch rlsusisubst;
% Verboseswitch for atomic formula simplification
switch rlpasfatfsimpvb;
off1 'rlpasfrangeexpand;
off1 'rlpasfvb;
on1 'rlpasfsimplify;
off1 'rlsiverbose;
off1 'rlsusitr;
off1 'rlpasfatfsimpvb;
off1 'rlsusisubst;
% Parameters
put('pasf,'rl_params,'(
(rl_subat!* . pasf_subat)
(rl_subalchk!* . pasf_subalchk)
(rl_eqnrhskernels!* . pasf_eqnrhskernels)
(rl_simplat1!* . pasf_simplat1)
(rl_ordatp!* . pasf_ordatp)
(rl_op!* . pasf_op)
(rl_simplb!* . pasf_simplb)
(rl_varsubstat!* . pasf_varsubstat)
(rl_negateat!* . pasf_negateat)
(rl_bnfsimpl!* . cl_bnfsimpl)
(rl_tordp!* . ordp)
(rl_termmlat!* . pasf_termmlat)
(rl_sacat!* . pasf_sacat)
(rl_sacatlp!* . cl_sacatlp)
(rl_varlat!* . pasf_varlat)
(rl_smupdknowl!* . pasf_smwupdknowl)
(rl_smrmknowl!* . pasf_smwrmknowl)
(rl_smcpknowl!* . pasf_smwcpknowl)
(rl_smmkatl!* . pasf_smwmkatl)
(rl_smsimpl!-impl!* . cl_smsimpl!-impl)
(rl_smsimpl!-equiv1!* . cl_smsimpl!-equiv1)
(rl_susibin!* . pasf_susibin)
(rl_susipost!* . pasf_susipost)
(rl_susitf!* . pasf_susitf)
(rl_bsatp!* . pasf_qff2ivl)
));
% Services
put('pasf,'rl_services,'(
(rl_apnf!* . cl_apnf)
(rl_atml!* . cl_atml)
(rl_terml!* . cl_terml)
(rl_termml!* . cl_termml)
(rl_tnf!* . cl_tnf)
(rl_varl!* . cl_varl)
(rl_fvarl!* . cl_fvarl)
(rl_bvarl!* . cl_bvarl)
(rl_all!* . cl_all)
(rl_ex!* . cl_ex)
(rl_simpl!* . cl_simpl)
(rl_atnum!* . cl_atnum)
(rl_matrix!* . cl_matrix)
(rl_qe!* . pasf_qe)
(rl_expand!* . pasf_expand)
(rl_atl!* . cl_atl)
(rl_pnf!* . pasf_pnf)
(rl_dnf!* . cl_dnf)
(rl_cnf!* . cl_cnf)
(rl_nnf!* . cl_nnf)
(rl_simplb!* . pasf_simplb)
(rl_b2terml!* . pasf_b2terml)
(rl_b2atl!* . pasf_b2atl)
));
% Switches
put('pasf,'rl_cswitches,'(
(rlsism . t)
(rlsusi . t)));
% Admin
put('pasf,'simpfnname,'pasf_simpfn);
put('pasf,'rl_prepat,'pasf_prepat);
put('pasf,'rl_resimpat,'pasf_resimpat);
put('pasf,'rl_lengthat,'pasf_lengthat);
put('pasf,'rl_prepterm,'prepf);
put('pasf,'rl_simpterm,'pasf_simpterm);
algebraic infix equal;
put('equal,'pasf_simpfn,'pasf_simpat);
put('equal,'number!-of!-args,2);
algebraic infix neq;
put('neq,'pasf_simpfn,'pasf_simpat);
put('neq,'number!-of!-args,2);
put('neq,'rtypefn,'quotelog);
newtok '((!< !>) neq);
algebraic operator cong;
put('cong,'prifn,'pasf_pricong);
put('cong,'pasf_simpfn,'pasf_simpat);
put('cong,'number!-of!-args,3);
put('cong,'rtypefn,'quotelog);
put('cong,'fancy!-prifn,'pasf_fancy!-pricong);
procedure pasf_pricong(x);
if null !*nat then
'failed
else <<
maprin cadr x;
prin2!* " ~";
maprin cadddr x;
prin2!* "~ ";
maprin caddr x
>>;
% alternative printing with |
%symbolic procedure pasf_fancy!-pricong(c);
% if null !*nat then
% 'failed
% else <<
% maprin cadddr c;
% if car c eq 'cong then
% fancy!-prin2 "|"
% else
% fancy!-prin2 "\not|";
% maprin cadr c;
% >>;
procedure pasf_fancy!-pricong(c);
if rl_texmacsp() then
pasf_fancy!-pricong!-texmacs c
else
pasf_fancy!-pricong!-fm c;
procedure pasf_fancy!-pricong!-texmacs(c);
if null !*nat then
'failed
else <<
maprin cadr c; % lhs
if car c eq 'cong then
fancy!-prin2 "\equiv"
else
fancy!-prin2 "\not\equiv";
fancy!-prin2!-underscore();
fancy!-prin2 "{";
maprin cadddr c; % modulus
fancy!-prin2 "}";
fancy!-prin2 " ";
maprin caddr c; % rhs
>>;
procedure pasf_fancy!-pricong!-fm(x);
if null !*nat then
'failed
else <<
maprin cadr x;
if car x eq 'cong then
fancy!-special!-symbol(186,2)
else <<
fancy!-prin2 "/";
fancy!-special!-symbol(186,2)
>>;
maprin caddr x;
fancy!-prin2 " (";
maprin cadddr x;
fancy!-prin2 ")"
>>;
algebraic operator ncong;
put('ncong,'prifn,'pasf_princong);
put('ncong,'pasf_simpfn,'pasf_simpat);
put('ncong,'number!-of!-args,3);
put('ncong,'rtypefn,'quotelog);
put('ncong,'fancy!-prifn,'pasf_fancy!-pricong);
procedure pasf_princong(x);
if null !*nat then
'failed
else <<
maprin cadr x;
prin2!* " #";
maprin cadddr x;
prin2!* "# ";
maprin caddr x
>>;
algebraic infix leq;
put('leq,'pasf_simpfn,'pasf_simpat);
put('leq,'number!-of!-args,2);
put('leq,'rtypefn,'quotelog);
algebraic infix geq;
put('geq,'pasf_simpfn,'pasf_simpat);
put('geq,'number!-of!-args,2);
put('geq,'rtypefn,'quotelog);
algebraic infix lessp;
put('lessp,'pasf_simpfn,'pasf_simpat);
put('lessp,'number!-of!-args,2);
put('lessp,'rtypefn,'quotelog);
algebraic infix greaterp;
put('greaterp,'pasf_simpfn,'pasf_simpat);
put('greaterp,'number!-of!-args,2);
put('greaterp,'rtypefn,'quotelog);
flag('(equal neq leq geq lessp greaterp),'spaced);
flag('(pasf_simpat),'full);
% Temporarily introduced algebraic mode interfaces
operator rlqeex;
procedure rlqeex(phi,k);
rl_mk!*fof pasf_qeex(rl_simp phi,k);
operator rlsimplb;
procedure rlsimplb(phi,k);
rl_mk!*fof rl_simplb(rl_simp phi,k);
%rl_mk!*fof rl_simp phi;
operator rlstrb;
procedure rlstrb(phi);
(if res then rl_mk!*fof res else '(list))
where res = cl_simpl!-bqua!-strb(rl_simp phi,'unknown);
operator rleq;
procedure rleq(phi);
(if res then rl_mk!*fof res else '(list))
where res = cl_simpl!-bqua!-eq(rl_simp phi);
operator rlsimplat;
procedure rlsimplat(phi);
rl_mk!*fof rl_simplat1(rl_simp phi,'dummy);
operator rlivl2qff;
procedure rlivl2qff(ivl,var);
rl_mk!*fof pasf_ivl2qff(for each iv in cdr ivl collect
cadr iv . caddr iv,var);
operator rlqff2ivl;
procedure rlqff2ivl(f);
'list . for each iv in pasf_qff2ivl1(rl_simp f) collect
{'list,car iv,cdr iv};
operator rlb2terml;
procedure rlb2terml(b, var);
'list . pasf_b2terml(rl_simp b, var);
operator rlb2atl;
procedure rlb2atl(b, var);
'list . for each at in rl_b2atl(rl_simp b, var) collect rl_mk!*fof at;
% End of temporary methods
procedure pasf_verbosep();
% Presburger arithmetic verbose verbose switch. Returns true if the
% main switch rlverbose is on and the secondary switch rlpasfvb is
% on.
!*rlverbose and !*rlpasfvb;
procedure pasf_simpterm(u);
% Presburger arithmetic simp term. [u] is Lisp Prefix. Returns
% the [u] as a PASF term.
numr simp u;
procedure pasf_prepat(f);
% Presburger arithmetic prep atomic formula. [f] is a PASF
% atomic formula. Returns [f] in Lisp prefix form.
if pasf_cong f then
{pasf_opn f,prepf pasf_arg2l f,prepf pasf_arg2r f,pasf_m f}
else
pasf_opn f . for each arg in pasf_argn f collect prepf arg;
procedure pasf_resimpat(f);
% Presburger arithmetic resimp atomic formula. [f] is an PASF
% atomic formula. Returns the atomic formula [f] with resimplified
% terms.
pasf_mkn(pasf_op f,for each arg in pasf_argn f collect
numr resimp !*f2q arg);
procedure pasf_lengthat(f);
% Presburger arithmetic length of atomic formula. [f] is an
% atomic formula. Returns a number, the length of [f].
length pasf_argn f;
procedure pasf_simpat(u);
% Presburger arithmetic simp atomic formula. [u] is Lisp prefix.
% Returns [u] as an atomic formula.
begin scalar op,lhs,rhs,m,term,atf;
op := car u;
lhs := simp cadr u;
if denr lhs neq 1 then
typerr(u,"atomic formula");
rhs := simp caddr u;
if denr rhs neq 1 then
typerr(u,"atomic formula");
term := numr subtrsq(lhs,rhs);
% Check for the correct term form. Method fails if
% the term is not correct.
tnf_expr2tnf term;
% Now the formula term is surely correct
if op memq '(cong ncong) then <<
m := cadddr u;
if not (numberp m) or eqn(m,0) then
typerr(m,"modulus");
return pasf_0mk2((op . numr simp m),term)
>>;
atf := pasf_0mk2(op,term);
return atf;
end;
procedure pasf_opn(atf);
% Presburger arithmetic operator name. [atf] is an atomic formula
% $R(t_1,t_2)$. Returns the name of $R$.
if pairp car atf then
caar atf
else
car atf;
procedure pasf_op(atf);
% Presburger arithmetic operator. [atf] is an atomic formula
% $R(t_1,t_2)$. Returns $R$.
car atf;
procedure pasf_mkop(op,m);
% Presburger arithmetic make operator. [op] is one of the operators
% [equal], [neq], [cong], [ncong], [leq], [geq], [lessp],
% [greaterp]; m is a modulus. Returns $op$ if operator is not
% [cong] or [ncong] and $(op . m)$ else.
if op memq '(cong ncong) then
(op . if null m then
rederr{"Modulo 0 congruence created"}
else
m)
else
op;
procedure pasf_atfp(f);
% Presburger arithmetic atomic formula predicate. [f] is a
% formula. Returns t is and only if [f] is an atomic formula.
(pasf_opn f) memq '(equal neq leq geq lessp greaterp
cong ncong);
procedure pasf_cong(atf);
% Presburger arithmetic congruence atomic formula. [atf] is an
% atomic formula. Returns $t$ if the operator is [cong] or [ncong].
pasf_opn(atf) memq '(cong ncong);
procedure pasf_m(atf);
% Presburger arithmetic modulus operator. [atf] is an atomic
% formula $t_1 = t_2 ~(n)$. Returns $n$.
cdar atf;
procedure pasf_hasm(atf);
% Presburger arithmetic has modulus operator. [atf] is an atomic
% formula $t_1 = t_2 ~(n)$. Returns $true$ if and only if [atf]
% is a congruence.
pairp car atf;
procedure pasf_arg2l(atf);
% Presburger arithmetic binary operator left hand side argument.
% [atf] is an atomic formula $R(t_1,t_2)$. Returns $t_1$.
cadr atf;
procedure pasf_arg2r(atf);
% Presburger arithmetic binary operator right hand side argument.
% [atf] is an atomic formula $R(t_1,t_2)$. Returns $t_2$.
caddr atf;
procedure pasf_argn(atf);
% Presburger arithmetic 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 pasf_mk2(op,lhs,rhs);
% Presburger arithmetic make atomic formula for binary operator.
% [op] is one of the operators [equal], [neq], [div], [sdiv],
% [assoc], and [nassoc]; [lhs] and [rhs] are terms. Returns the
% atomic formula $[op]([lhs],[rhs])$.
{op,lhs,rhs};
procedure pasf_0mk2(op,lhs);
% Presburger arithmetic make zero right hand atomic formula for
% binary operator. [op] is one of the operators [equal], [neq],
% [div], [sdiv], [assoc], and [nassoc]; [lhs] is a term. Returns
% the atomic formula $[op]([lhs],0)$.
{op,lhs,nil};
procedure pasf_mkn(op,argl);
% Presburger arithmetic make atomic formula for n-ary operator.
% [op] is one of the operators [equal], [neq], [div], [sdiv],
% [assoc], and [nassoc]; [argl] is a list $(t_1,t_2)$ of terms.
% Returns the atomic formula $[op](t_1,t_2)$.
op . argl;
procedure pasf_mkrng(bv,lr,ur);
% Presburger arithmetic make range operator. [bv] is the variable
% to bound; [lr] and [ur] are the bounds. Returns the range formula
% $[lr] \leq [bv] \leq [ur]$.
if domainp lr and domainp ur then
if lr=ur then
pasf_mk2('equal,numr simp bv,lr)
else rl_mkn('and,{
pasf_mk2('geq,numr simp bv,numr simp lr),
pasf_mk2('leq,numr simp bv,numr simp ur)})
else
rederr{"pasf_mkrng : Bounds should be domain valued elements"};
procedure pasf_mknrng(bv,lr,ur);
% Presburger arithmetic make negated range operator. [bv] is the
% variable to bound; [lr] and [ur] are the bounds. Returns the
% negated range formula $[lr] \leq [bv] \leq [ur]$.
if domainp lr and domainp ur then
rl_mkn('or,{
pasf_mk2('leq,numr simp bv,lr),
pasf_mk2('geq,numr simp bv,ur)})
else
rederr{"pasf_mkrng : Bounds should be domain valued elements"};
endmodule; % [pasf]
end; % of file