Artifact 5857840bf197b90689fa9bb0d36890bd05848bdf8cc9bf59d1c1b00c39b11d56:
- Executable file
r38/packages/redlog/redlog.tst
— 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: 8005) [annotate] [blame] [check-ins using] [more...]
% ---------------------------------------------------------------------- % $Id: redlog.tst,v 1.7 2002/08/20 14:44:50 seidl Exp $ % ---------------------------------------------------------------------- % Copyright (c) 1995-1997 % Andreas Dolzmann and Thomas Sturm, Universitaet Passau % ---------------------------------------------------------------------- % $Log: redlog.tst,v $ % Revision 1.7 2002/08/20 14:44:50 seidl % Moved CAD example to a better place. % % Revision 1.6 2002/08/20 14:32:36 seidl % rlcad cox6 added. % % Revision 1.5 1999/04/13 21:53:26 sturm % Removed "on echo". % % Revision 1.4 1999/04/05 12:25:29 dolzmann % Fixed a bug. % % Revision 1.3 1999/04/05 12:15:43 dolzmann % Added code for testing the contexts acfsf and dvfsf. % % Revision 1.2 1997/08/20 16:22:07 sturm % Do not use "on time". % % Revision 1.1 1997/08/18 15:59:01 sturm % Renamed "rl.red" to "redlog.red", and thus "rl.tst" to this file % "redlog.tst." % % ---------------------------------------------------------------------- % Revision 1.3 1996/10/14 16:18:39 sturm % Added sc50b for testing the optimizer. % % Revision 1.2 1996/10/03 16:09:39 sturm % Added new QE example for testing rlatl, ..., rlifacml, rlstruct, % rlifstruct. % % Revision 1.1 1996/09/30 17:07:52 sturm % Initial check-in. % % ---------------------------------------------------------------------- on rlverbose; % Ordered fields standard form: rlset ofsf; rlset(); % Chains -3/5<x>y>z<=a<>b>c<5/3; % For loop actions. g := for i:=1:6 mkor for j := 1:6 mkand mkid(a,i) <= mkid(a,j); % Quantifier elimination and variants h := rlsimpl rlall g; rlmatrix h; on rlrealtime; rlqe h; off rlrealtime; h := rlsimpl rlall(g,{a2}); rlqe h; off rlqeheu,rlqedfs; rlqe ex(x,a*x**2+b*x+c>0); on rlqedfs; rlqe ex(x,a*x**2+b*x+c>0); on rlqeheu; rlqe(ex(x,a*x**2+b*x+c>0),{a<0}); rlgqe ex(x,a*x**2+b*x+c>0); rlthsimpl ({a*b*c=0,b<>0}); rlqe ex({x,y},(for i:=1:5 product mkid(a,i)*x**10-mkid(b,i)*y**2)<=0); sol := rlqe ex(x,a*x**2+b*x+c>0); rlatnum sol; rlatl sol; rlatml sol; rlterml sol; rltermml sol; rlifacl sol; rlifacml sol; rlstruct(sol,v); rlifstruct(sol,v); rlitab sol; rlatnum ws; rlgsn sol; rlatnum ws; off rlverbose; rlqea ex(x,m*x+b=0); % from Marc van Dongen. Finding the first feasible solution for the % solution of systems of linear diophantine inequalities. dong := { 3*X259+4*X261+3*X262+2*X263+X269+2*X270+3*X271+4*X272+5*X273+X229=2, 7*X259+11*X261+8*X262+5*X263+3*X269+6*X270+9*X271+12*X272+15*X273+X229=4, 2*X259+5*X261+4*X262+3*X263+3*X268+4*X269+5*X270+6*X271+7*X272+8*X273=1, X262+2*X263+5*X268+4*X269+3*X270+2*X271+X272+2*X229=1, X259+X262+2*X263+4*X268+3*X269+2*X270+X271-X273+3*X229=2, X259+2*X261+2*X262+2*X263+3*X268+3*X269+3*X270+3*X271+3*X272+3*X273+X229=1, X259+X261+X262+X263+X268+X269+X270+X271+X272+X273+X229=1}; sol := rlopt(dong,0); % Substitution sub(first second sol,for each atf in dong mkand atf); rlsimpl ws; sub(x=a,x=0 and a=0 and ex(x,x=y) and ex(a,x>a)); f1 := x=0 and b>=0; f2 := a=0; f := f1 or f2; % Boolean normal forms. rlcnf f; rldnf ws; rlcnf f; % Negation normal form and prenex normal form hugo := a=0 and b=0 and y<0 equiv ex(y,y>=a) or a>0; rlnnf hugo; rlpnf hugo; % Length and Part part(hugo,0); part(hugo,2,1,2); length ws; length hugo; length part(hugo,1); % Tableau mats := all(t,ex({l,u},( (t>=0 and t<=1) impl (l>0 and u<=1 and -t*x1+t*x2+2*t*x1*u+u=l*x1 and -2*t*x2+t*x2*u=l*x2)))); sol := rlgsn rlqe mats; rltab(sol,{x1>0,x1<0,x1=0}); % Part on psopfn / cleanupfn part(rlqe ex(x,m*x+b=0),1); walter := (x>0 and y>0); rlsimpl(true,rlatl walter); part(rlatl walter,1,1); % Optimizer sc50b!-t := -1*vCOL00004$ sc50b!-c := { vCOL00001 >= 0,vCOL00002 >= 0,vCOL00003 >= 0,vCOL00004 >= 0,vCOL00005 >= 0, vCOL00006 >= 0,vCOL00007 >= 0,vCOL00008 >= 0,vCOL00009 >= 0,vCOL00010 >= 0, vCOL00011 >= 0,vCOL00012 >= 0,vCOL00013 >= 0,vCOL00014 >= 0,vCOL00015 >= 0, vCOL00016 >= 0,vCOL00017 >= 0,vCOL00018 >= 0,vCOL00019 >= 0,vCOL00020 >= 0, vCOL00021 >= 0,vCOL00022 >= 0,vCOL00023 >= 0,vCOL00024 >= 0,vCOL00025 >= 0, vCOL00026 >= 0,vCOL00027 >= 0,vCOL00028 >= 0,vCOL00029 >= 0,vCOL00030 >= 0, vCOL00031 >= 0,vCOL00032 >= 0,vCOL00033 >= 0,vCOL00034 >= 0,vCOL00035 >= 0, vCOL00036 >= 0,vCOL00037 >= 0,vCOL00038 >= 0,vCOL00039 >= 0,vCOL00040 >= 0, vCOL00041 >= 0,vCOL00042 >= 0,vCOL00043 >= 0,vCOL00044 >= 0,vCOL00045 >= 0, vCOL00046 >= 0,vCOL00047 >= 0,vCOL00048 >= 0, 3*vCOL00001+(3*vCOL00002)+(3*vCOL00003) <= 300, 1*vCOL00004+(-1*vCOL00005) = 0, -1*vCOL00001+(1*vCOL00006) = 0, -1*vCOL00002+(1*vCOL00007) = 0, -1*vCOL00003+(1*vCOL00008) = 0, -1*vCOL00006+(1*vCOL00009) <= 0, -1*vCOL00007+(1*vCOL00010) <= 0, -1*vCOL00008+(1*vCOL00011) <= 0, -1*vCOL00009+(3*vCOL00012)+(3*vCOL00013)+(3*vCOL00014) <= 300, 0.400000*vCOL00005+(-1*vCOL00010) <= 0, 0.600000*vCOL00005+(-1*vCOL00011) <= 0, 1.100000*vCOL00004+(-1*vCOL00015) = 0, 1*vCOL00005+(1*vCOL00015)+(-1*vCOL00016) = 0, -1*vCOL00006+(-1*vCOL00012)+(1*vCOL00017) = 0, -1*vCOL00007+(-1*vCOL00013)+(1*vCOL00018) = 0, -1*vCOL00008+(-1*vCOL00014)+(1*vCOL00019) = 0, -1*vCOL00017+(1*vCOL00020) <= 0, -1*vCOL00018+(1*vCOL00021) <= 0, -1*vCOL00019+(1*vCOL00022) <= 0, -1*vCOL00020+(3*vCOL00023)+(3*vCOL00024)+(3*vCOL00025) <= 300, 0.400000*vCOL00016+(-1*vCOL00021) <= 0, 0.600000*vCOL00016+(-1*vCOL00022) <= 0, 1.100000*vCOL00015+(-1*vCOL00026) = 0, 1*vCOL00016+(1*vCOL00026)+(-1*vCOL00027) = 0, -1*vCOL00017+(-1*vCOL00023)+(1*vCOL00028) = 0, -1*vCOL00018+(-1*vCOL00024)+(1*vCOL00029) = 0, -1*vCOL00019+(-1*vCOL00025)+(1*vCOL00030) = 0, -1*vCOL00028+(1*vCOL00031) <= 0, -1*vCOL00029+(1*vCOL00032) <= 0, -1*vCOL00030+(1*vCOL00033) <= 0, -1*vCOL00031+(3*vCOL00034)+(3*vCOL00035)+(3*vCOL00036) <= 300, 0.400000*vCOL00027+(-1*vCOL00032) <= 0, 0.600000*vCOL00027+(-1*vCOL00033) <= 0, 1.100000*vCOL00026+(-1*vCOL00037) = 0, 1*vCOL00027+(1*vCOL00037)+(-1*vCOL00038) = 0, -1*vCOL00028+(-1*vCOL00034)+(1*vCOL00039) = 0, -1*vCOL00029+(-1*vCOL00035)+(1*vCOL00040) = 0, -1*vCOL00030+(-1*vCOL00036)+(1*vCOL00041) = 0, -1*vCOL00039+(1*vCOL00042) <= 0, -1*vCOL00040+(1*vCOL00043) <= 0, -1*vCOL00041+(1*vCOL00044) <= 0, -1*vCOL00042+(3*vCOL00045)+(3*vCOL00046)+(3*vCOL00047) <= 300, 0.400000*vCOL00038+(-1*vCOL00043) <= 0, 0.600000*vCOL00038+(-1*vCOL00044) <= 0, 1.100000*vCOL00037+(-1*vCOL00048) = 0, -0.700000*vCOL00045+(0.300000*vCOL00046)+(0.300000*vCOL00047) <= 0, -1*vCOL00046+(0.400000*vCOL00048) <= 0, -1*vCOL00047+(0.600000*vCOL00048) <= 0}$ rlopt(sc50b!-c,sc50b!-t); % QE by partial CAD: cox6 := ex({u,v},x=u*v and y=u**2 and z=v**2)$ rlcad cox6; % Algebraically closed fields standard form: sub(x=a,x=0 and a=0 and ex(x,x=y) and ex(a,x<>a)); rlset acfsf; rlsimpl(x^2+y^2+1<>0); rlqe ex(x,x^2=y); clear f; h := rlqe ex(x,x^3+a*x^2+b*x+c=0 and x^3+d*x^2+e*x+f=0); rlstruct h; rlqe rlall (h equiv resultant(x^3+a*x^2+b*x+c,x^3+d*x^2+e*x+f,x)=0); clear h; % Discretely valued fields standard form: rlset dvfsf; sub(x=a,x=0 and a=0 and ex(x,x=y) and ex(a,x~a)); % P-adic Balls, taken from Andreas Dolzmann, Thomas Sturm. P-adic % Constraint Solving, Proceedings of the ISSAC '99. rlset dvfsf; rlqe all(r_1,all(r_2,all(a,all(b, ex(x,r_1||x-a and r_2||x-b and r_1|r_2) impl all(y,r_2||y-b impl r_1||y-a))))); rlmkcanonic ws; rlset(dvfsf,100003); rlqe all(r_1,all(r_2,all(a,all(b, ex(x,r_1||x-a and r_2||x-b and r_1|r_2) impl all(y,r_2||y-b impl r_1||y-a))))); % Size of the Residue Field, taken from Andreas Dolzmann, Thomas % Sturm. P-adic Constraint Solving. Proceedings of the ISSAC '99. rlset(dvfsf); rlqe ex(x,x~1 and x-1~1 and x-2~1 and x-3~1 and 2~1 and 3~1); rlexplats ws; rldnf ws; % Selecting contexts: rlset ofsf; f:= ex(x,m*x+b=0); rlqe f; rlset dvfsf; rlqe f; rlset acfsf; rlqe f; end; % of file