reduce-historical/r37/log/redlog.rlg

Sun Aug 18 18:57:13 2002 run on Windows
% ----------------------------------------------------------------------
% $Id: redlog.tst,v 1.5 1999/04/13 21:53:26 sturm Exp $
% ----------------------------------------------------------------------
% Copyright (c) 1995-1997
% Andreas Dolzmann and Thomas Sturm, Universitaet Passau
% ----------------------------------------------------------------------
% $Log: redlog.tst,v $
% 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();


{ofsf}


% Chains
-3/5<x>y>z<=a<>b>c<5/3;


 - 5*x - 3 < 0 and x - y > 0 and y - z > 0 and  - a + z <= 0 and a - b <> 0

 and b - c > 0 and 3*c - 5 < 0


% For loop actions.
g := for i:=1:6 mkor
   for j := 1:6 mkand
      mkid(a,i) <= mkid(a,j);


g := false or (true and 0 <= 0 and a1 - a2 <= 0 and a1 - a3 <= 0

 and a1 - a4 <= 0 and a1 - a5 <= 0 and a1 - a6 <= 0) or (true

 and  - a1 + a2 <= 0 and 0 <= 0 and a2 - a3 <= 0 and a2 - a4 <= 0

 and a2 - a5 <= 0 and a2 - a6 <= 0) or (true and  - a1 + a3 <= 0

 and  - a2 + a3 <= 0 and 0 <= 0 and a3 - a4 <= 0 and a3 - a5 <= 0

 and a3 - a6 <= 0) or (true and  - a1 + a4 <= 0 and  - a2 + a4 <= 0

 and  - a3 + a4 <= 0 and 0 <= 0 and a4 - a5 <= 0 and a4 - a6 <= 0) or (true

 and  - a1 + a5 <= 0 and  - a2 + a5 <= 0 and  - a3 + a5 <= 0 and  - a4 + a5 <= 0

 and 0 <= 0 and a5 - a6 <= 0) or (true and  - a1 + a6 <= 0 and  - a2 + a6 <= 0

 and  - a3 + a6 <= 0 and  - a4 + a6 <= 0 and  - a5 + a6 <= 0 and 0 <= 0)


% Quantifier elimination and variants
h := rlsimpl rlall g;


h := all a1 all a2 all a3 all a4 all a5 all a6 ((a1 - a2 <= 0 and a1 - a3 <= 0

 and a1 - a4 <= 0 and a1 - a5 <= 0 and a1 - a6 <= 0) or (a1 - a2 >= 0

 and a2 - a3 <= 0 and a2 - a4 <= 0 and a2 - a5 <= 0 and a2 - a6 <= 0) or (

a1 - a3 >= 0 and a2 - a3 >= 0 and a3 - a4 <= 0 and a3 - a5 <= 0 and a3 - a6 <= 0

) or (a1 - a4 >= 0 and a2 - a4 >= 0 and a3 - a4 >= 0 and a4 - a5 <= 0

 and a4 - a6 <= 0) or (a1 - a5 >= 0 and a2 - a5 >= 0 and a3 - a5 >= 0

 and a4 - a5 >= 0 and a5 - a6 <= 0) or (a1 - a6 >= 0 and a2 - a6 >= 0

 and a3 - a6 >= 0 and a4 - a6 >= 0 and a5 - a6 >= 0))

rlmatrix h;


(a1 - a2 <= 0 and a1 - a3 <= 0 and a1 - a4 <= 0 and a1 - a5 <= 0

 and a1 - a6 <= 0) or (a1 - a2 >= 0 and a2 - a3 <= 0 and a2 - a4 <= 0

 and a2 - a5 <= 0 and a2 - a6 <= 0) or (a1 - a3 >= 0 and a2 - a3 >= 0

 and a3 - a4 <= 0 and a3 - a5 <= 0 and a3 - a6 <= 0) or (a1 - a4 >= 0

 and a2 - a4 >= 0 and a3 - a4 >= 0 and a4 - a5 <= 0 and a4 - a6 <= 0) or (

a1 - a5 >= 0 and a2 - a5 >= 0 and a3 - a5 >= 0 and a4 - a5 >= 0 and a5 - a6 <= 0

) or (a1 - a6 >= 0 and a2 - a6 >= 0 and a3 - a6 >= 0 and a4 - a6 >= 0

 and a5 - a6 >= 0)

on rlrealtime;


rlqe h;

---- (all a1 a2 a3 a4 a5 a6) [DFS: depth 6, watching 5]
[0e] [1e] [2e] [3e] [3e] [3e] [3e] [2e] [3e] [3e] [3e] [2e] [3e] [3e] [3e] [2e] 
[3e] [3e] [3e] [2e] [3e] [3e] [3e] [3e] [1e] [2e] [3e] [3e] [3e] [2e] [3e] [3e] 
[3e] [2e] [3e] [3e] [3e] [2e] [3e] [3e] [3e] [3e] [1e] [2e] [3e] [3e] [3e] [2e] 
[3e] [3e] [3e] [2e] [3e] [3e] [3e] [2e] [3e] [3e] [3e] [1e] [2e] [3e] [3e] [3e] 
[2e] [3e] [3e] [3e] [2e] [3e] [3e] [3e] [2e] [3e] [3e] [3e] [1e] [2e] [3e] [3e] 
[3e] [2e] [3e] [3e] [3e] [2e] [3e] [3e] [3e] [2e] [3e] [3e] [3e] [1e] [2e] [3e] 
[3e] [3e] [3e] [2e] [3e] [3e] [3e] [2e] [3e] [3e] [3e] [2e] [3e] [3e] [3e] [2e] 
[3e] [3e] [3e] [3e] [DEL:25/116]
Realtime: 20 s

true

off rlrealtime;



h := rlsimpl rlall(g,{a2});


h := all a1 all a3 all a4 all a5 all a6 ((a1 - a2 <= 0 and a1 - a3 <= 0

 and a1 - a4 <= 0 and a1 - a5 <= 0 and a1 - a6 <= 0) or (a1 - a2 >= 0

 and a2 - a3 <= 0 and a2 - a4 <= 0 and a2 - a5 <= 0 and a2 - a6 <= 0) or (

a1 - a3 >= 0 and a2 - a3 >= 0 and a3 - a4 <= 0 and a3 - a5 <= 0 and a3 - a6 <= 0

) or (a1 - a4 >= 0 and a2 - a4 >= 0 and a3 - a4 >= 0 and a4 - a5 <= 0

 and a4 - a6 <= 0) or (a1 - a5 >= 0 and a2 - a5 >= 0 and a3 - a5 >= 0

 and a4 - a5 >= 0 and a5 - a6 <= 0) or (a1 - a6 >= 0 and a2 - a6 >= 0

 and a3 - a6 >= 0 and a4 - a6 >= 0 and a5 - a6 >= 0))

rlqe h;

---- (all a1 a3 a4 a5 a6) [BFS: depth 5]
-- left: 5
[1e] 
-- left: 4
[6e] [5e] [4e] [3e] [2e] [1e] 
-- left: 3
[17e] [16e] [15e] [14e] [13e] [12e] [11e] [10e] [9e] [8e] [7e] [6e] [5e] [4e] [3
e] [2e] [1e] 
-- left: 2
[16e] [15e] [14e] [13e] [12e] [11e] [10e] [9e] [8e] [7e] [6e] [5e] [4e] [3e] [2e
] [1e] [DEL:65/40]
true


off rlqeheu,rlqedfs;


rlqe ex(x,a*x**2+b*x+c>0);

---- (ex x) [BFS: depth 1]
-- left: 1
[1e] [DEL:0/1]
                     3
a > 0 or (2*a*b*c - b  > 0 and a = 0 and b <> 0)

                                                          2
 or (a = 0 and (b > 0 or (b = 0 and c > 0))) or (4*a*c - b  < 0 and a < 0)

on rlqedfs;


rlqe ex(x,a*x**2+b*x+c>0);

---- (ex x) [DFS: depth 1, watching 1]
[0e] [DEL:0/1]
                     3
a > 0 or (2*a*b*c - b  > 0 and a = 0 and b <> 0)

                                                          2
 or (a = 0 and (b > 0 or (b = 0 and c > 0))) or (4*a*c - b  < 0 and a < 0)

on rlqeheu;



rlqe(ex(x,a*x**2+b*x+c>0),{a<0});

---- (ex x) [BFS: depth 1]
-- left: 1
[1e] [DEL:0/1]
         2
4*a*c - b  < 0


rlgqe ex(x,a*x**2+b*x+c>0);

---- (ex x) [BFS: depth 1]
-- left: 1
[1e!] [DEL:0/1]
{{a <> 0},

          2
 4*a*c - b  < 0 or a >= 0}

rlthsimpl ({a*b*c=0,b<>0});


{a*c = 0,b <> 0}



rlqe ex({x,y},(for i:=1:5 product mkid(a,i)*x**10-mkid(b,i)*y**2)<=0);

---- (ex x y) [BFS: depth 2]
-- left: 2
[1(y^2)(x^10)(SVF).e] 
-- left: 1
[6e] [5e] [4e] [3e] [2e] [1e] [DEL:0/7]
true


sol := rlqe ex(x,a*x**2+b*x+c>0);

---- (ex x) [BFS: depth 1]
-- left: 1
[1e] [DEL:0/1]
                            3
sol := a > 0 or (2*a*b*c - b  > 0 and a = 0 and b <> 0)

                                                          2
 or (a = 0 and (b > 0 or (b = 0 and c > 0))) or (4*a*c - b  < 0 and a < 0)

rlatnum sol;


10


rlatl sol;


            3
{2*a*b*c - b  > 0,

          2
 4*a*c - b  < 0,

 a = 0,

 a < 0,

 a > 0,

 b = 0,

 b <> 0,

 b > 0,

 c > 0}

rlatml sol;


             3
{{2*a*b*c - b  > 0,1},

           2
 {4*a*c - b  < 0,1},

 {a = 0,2},

 {a < 0,1},

 {a > 0,1},

 {b = 0,1},

 {b <> 0,1},

 {b > 0,1},

 {c > 0,1}}

rlterml sol;


             2
{b*(2*a*c - b ),

          2
 4*a*c - b ,

 a,

 b,

 c}

rltermml sol;


              2
{{b*(2*a*c - b ),1},

           2
 {4*a*c - b ,1},

 {a,4},

 {b,3},

 {c,1}}

rlifacl sol;


          2
{4*a*c - b ,

          2
 2*a*c - b ,

 a,

 b,

 c}

rlifacml sol;


           2
{{4*a*c - b ,1},

           2
 {2*a*c - b ,1},

 {a,4},

 {b,4},

 {c,1}}


rlstruct(sol,v);


{v3 > 0 or (v1 > 0 and v3 = 0 and v4 <> 0)

  or (v3 = 0 and (v4 > 0 or (v4 = 0 and v5 > 0))) or (v2 < 0 and v3 < 0),

                  3
 {v1 = 2*a*b*c - b ,

                2
  v2 = 4*a*c - b ,

  v3 = a,

  v4 = b,

  v5 = c}}

rlifstruct(sol,v);


{v3 > 0 or (v2*v4 > 0 and v3 = 0 and v4 <> 0)

  or (v3 = 0 and (v4 > 0 or (v4 = 0 and v5 > 0))) or (v1 < 0 and v3 < 0),

                2
 {v1 = 4*a*c - b ,

                2
  v2 = 2*a*c - b ,

  v3 = a,

  v4 = b,

  v5 = c}}


rlitab sol;

10 = 100%
[9: 18] [8: 15] [7: 15] [6: 15] [5: 9] [4: 9] [3: 9] [2: 16] [1: 20] 
Success: 10 -> 9
0 = 100%
No success, returning the original formula
5 = 100%
[5: 7] [4: 5] [3: 5] [2: 5] [1: 9] 
No success, returning the original formula
1 = 100%
[1: 1] 
No success, returning the original formula

a > 0

                                                          3
 or (a = 0 and (b > 0 or (b = 0 and c > 0) or (2*a*b*c - b  > 0 and b < 0)))

              2
 or (4*a*c - b  < 0 and a < 0)

rlatnum ws;


9

rlgsn sol;

[DNF] 
global: 1; impl: 1; no neq: 3; glob-prod-al: 0.
[GP] [1] 
[3] [2] [1] 

                                                    3
a > 0 or (a = 0 and b = 0 and c > 0) or (2*a*b*c - b  > 0 and a = 0 and b <> 0)

                                   2
 or (a = 0 and b > 0) or (4*a*c - b  < 0 and a < 0)

rlatnum ws;


11


off rlverbose;



rlqea ex(x,m*x+b=0);


{{b = 0 and m = 0,{x = infinity1}},

                - b
 {m <> 0,{x = ------}}}
                m


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


dong := {x229 + 3*x259 + 4*x261 + 3*x262 + 2*x263 + x269 + 2*x270 + 3*x271

          + 4*x272 + 5*x273 = 2,

         x229 + 7*x259 + 11*x261 + 8*x262 + 5*x263 + 3*x269 + 6*x270 + 9*x271

          + 12*x272 + 15*x273 = 4,

         2*x259 + 5*x261 + 4*x262 + 3*x263 + 3*x268 + 4*x269 + 5*x270 + 6*x271

          + 7*x272 + 8*x273 = 1,

         2*x229 + x262 + 2*x263 + 5*x268 + 4*x269 + 3*x270 + 2*x271 + x272 = 1,

         3*x229 + x259 + x262 + 2*x263 + 4*x268 + 3*x269 + 2*x270 + x271 - x273

          = 2,

         x229 + x259 + 2*x261 + 2*x262 + 2*x263 + 3*x268 + 3*x269 + 3*x270

          + 3*x271 + 3*x272 + 3*x273 = 1,

         x229 + x259 + x261 + x262 + x263 + x268 + x269 + x270 + x271 + x272

          + x273 = 1}

sol := rlopt(dong,0);


sol := {0,

        {{x229

               - x262 - 2*x263 - 5*x268 - 4*x269 - 3*x270 - 2*x271 - x272 + 1
           = -----------------------------------------------------------------,
                                             2

          x259 = (x262 + 2*x263 + 7*x268 + 6*x269 + 5*x270 + 4*x271 + 3*x272

              + 2*x273 + 1)/2,

          x261 =  - x262 - x263 - 2*x268 - 2*x269 - 2*x270 - 2*x271 - 2*x272

           - 2*x273}}}


% Substitution
sub(first second sol,for each atf in dong mkand atf);


true and 0 = 0 and 0 = 0 and 0 = 0 and 0 = 0 and 0 = 0 and 0 = 0 and 0 = 0

rlsimpl ws;


true

sub(x=a,x=0 and a=0 and ex(x,x=y) and ex(a,x>a));


a = 0 and a = 0 and ex x (x - y = 0) and ex a0 (a - a0 > 0)


f1 := x=0 and b>=0;


f1 := x = 0 and b >= 0

f2 := a=0;


f2 := a = 0

f := f1 or f2;


f := (x = 0 and b >= 0) or a = 0


% Boolean normal forms.
rlcnf f;


(a = 0 or b >= 0) and (a = 0 or x = 0)


rldnf ws;


a = 0 or (b >= 0 and x = 0)


rlcnf f;


(a = 0 or b >= 0) and (a = 0 or x = 0)


% Negation normal form and prenex normal form
hugo := a=0 and b=0 and y<0 equiv ex(y,y>=a) or a>0;


hugo := (a = 0 and b = 0 and y < 0) equiv (ex y ( - a + y >= 0) or a > 0)

rlnnf hugo;


((a = 0 and b = 0 and y < 0) and (ex y ( - a + y >= 0) or a > 0))

 or ((a <> 0 or b <> 0 or y >= 0) and (all y ( - a + y < 0) and a <= 0))

rlpnf hugo;


all y1 ex y0 (((a = 0 and b = 0 and y < 0) and ( - a + y0 >= 0 or a > 0))

 or ((a <> 0 or b <> 0 or y >= 0) and ( - a + y1 < 0 and a <= 0)))


% Length and Part
part(hugo,0);


equiv

part(hugo,2,1,2);


 - a + y >= 0

length ws;


2

length hugo;


2

length part(hugo,1);


3


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


mats := all t ex l ex u ((t >= 0 and t - 1 <= 0) impl (l > 0 and u - 1 <= 0

 and  - l*x1 + 2*t*u*x1 - t*x1 + t*x2 + u = 0 and  - l*x2 + t*u*x2 - 2*t*x2 = 0)

)

sol := rlgsn rlqe mats;


sol := 3*x1 + 2 <> 0 and 2*x1 + 1 <> 0 and x1 + 1 <> 0 and x2 = 0

          2                               2
 and (2*x1  + x1 < 0 or x1 >= 0) and (3*x1  + 5*x1 + 2 < 0

        2                        2               2
 or 2*x1  + 3*x1 + 1 >= 0 or 2*x1  + x1 < 0 or x1  + x1 > 0)

          2                       2               2
 and (3*x1  + 5*x1 + 2 < 0 or 2*x1  + x1 < 0 or x1  + x1 > 0 or x1 = 0)

          2                        2               2
 and (2*x1  + 3*x1 + 1 >= 0 or 2*x1  + x1 < 0 or x1  + x1 > 0)

          2                        2               2
 and (2*x1  + 3*x1 + 1 >= 0 or 2*x1  + x1 < 0 or x1  + x1 > 0 or x1 = 0)

        2                               2
 and (x1  + x1 < 0 or x1 >= 0) and (3*x1  + 2*x1 < 0 or x1 >= 0)

rltab(sol,{x1>0,x1<0,x1=0});


                             2                       2
(x1 = 0 and (x2 = 0 and (3*x1  + 5*x1 + 2 < 0 or 2*x1  + 3*x1 + 1 >= 0

        2               2
 or 2*x1  + x1 < 0 or x1  + x1 > 0)

          2                        2               2
 and (2*x1  + 3*x1 + 1 >= 0 or 2*x1  + x1 < 0 or x1  + x1 > 0))) or (x1 < 0 and 

     2                    2                2
(3*x1  + 2*x1 < 0 and 2*x1  + x1 < 0 and x1  + x1 < 0 and 3*x1 + 2 <> 0

 and 2*x1 + 1 <> 0 and x1 + 1 <> 0 and x2 = 0)) or (x1 > 0 and (x2 = 0 and (

    2                       2                        2               2
3*x1  + 5*x1 + 2 < 0 or 2*x1  + 3*x1 + 1 >= 0 or 2*x1  + x1 < 0 or x1  + x1 > 0)

          2                       2               2
 and (3*x1  + 5*x1 + 2 < 0 or 2*x1  + x1 < 0 or x1  + x1 > 0)

          2                        2               2
 and (2*x1  + 3*x1 + 1 >= 0 or 2*x1  + x1 < 0 or x1  + x1 > 0)))


% Part on psopfn / cleanupfn
part(rlqe ex(x,m*x+b=0),1);


b = 0

walter := (x>0 and y>0);


walter := x > 0 and y > 0

rlsimpl(true,rlatl walter);


true

part(rlatl walter,1,1);


x


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


{-70,

 {{vcol00001 = 30,

   vcol00002 = 28,

   vcol00003 = 42,

   vcol00004 = 70,

   vcol00005 = 70,

   vcol00006 = 30,

   vcol00007 = 28,

   vcol00008 = 42,

   vcol00009 = 30,

   vcol00010 = 28,

   vcol00011 = 42,

   vcol00012 = 33,

                154
   vcol00013 = -----,
                 5

                231
   vcol00014 = -----,
                 5

   vcol00015 = 77,

   vcol00016 = 147,

   vcol00017 = 63,

                294
   vcol00018 = -----,
                 5

                441
   vcol00019 = -----,
                 5

   vcol00020 = 63,

                294
   vcol00021 = -----,
                 5

                441
   vcol00022 = -----,
                 5

                363
   vcol00023 = -----,
                10

                847
   vcol00024 = -----,
                25

                2541
   vcol00025 = ------,
                 50

                847
   vcol00026 = -----,
                10

                2317
   vcol00027 = ------,
                 10

                993
   vcol00028 = -----,
                10

                2317
   vcol00029 = ------,
                 25

                6951
   vcol00030 = ------,
                 50

                993
   vcol00031 = -----,
                10

                2317
   vcol00032 = ------,
                 25

                6951
   vcol00033 = ------,
                 50

                3993
   vcol00034 = ------,
                100

                9317
   vcol00035 = ------,
                250

                27951
   vcol00036 = -------,
                 500

                9317
   vcol00037 = ------,
                100

                32487
   vcol00038 = -------,
                 100

                13923
   vcol00039 = -------,
                 100

                32487
   vcol00040 = -------,
                 250

                97461
   vcol00041 = -------,
                 500

                13923
   vcol00042 = -------,
                 100

                32487
   vcol00043 = -------,
                 250

                97461
   vcol00044 = -------,
                 500

                43923
   vcol00045 = -------,
                1000

                102487
   vcol00046 = --------,
                 2500

                307461
   vcol00047 = --------,
                 5000

                102487
   vcol00048 = --------}}}
                 1000


% Algebraically closed fields standard form:
sub(x=a,x=0 and a=0 and ex(x,x=y) and ex(a,x<>a));


a = 0 and a = 0 and ex x (x - y = 0) and ex a0 (a - a0 <> 0)


rlset acfsf;


{ofsf}


rlsimpl(x^2+y^2+1<>0);


 2    2
x  + y  + 1 <> 0


rlqe ex(x,x^2=y);


true


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


           2                    2      2                      2    3      2
h := (a*b*c  - 2*a*b*c*f + a*b*f  - a*c *e + 2*a*c*e*f - a*e*f  + b *f - b *c*e

      2              2      2      3      2        3        2    3
 - 2*b *e*f + 2*b*c*e  + b*e *f - c  + 3*c *f - c*e  - 3*c*f  + f  = 0 or (

                                 3      2        2    2            2
a*b*c - a*b*f - a*c*e + a*e*f - b  + 2*b *e - b*e  - c  + 2*c*f - f  <> 0

 and a - d <> 0) or (a*b - a*e - c + f <> 0 and a - d <> 0 and b - e <> 0)

 or (a - d <> 0 and b - e <> 0)) and (a - d <> 0 or b - e <> 0 or c - f = 0) and

   2                                  2      2                        2
 (a *e - a*b*d - a*c - a*d*e + a*f + b  + b*d  - 2*b*e + c*d - d*f + e  <> 0

     2                                    2                        3  2
 or a *f - a*c*d - a*d*f + b*c - b*f + c*d  - c*e + e*f = 0) and (a *f

    2            2          2    2    2    2      2
 - a *b*e*f - 2*a *c*d*f + a *c*e  - a *d*f  + a*b *d*f - a*b*c*d*e + 3*a*b*c*f

                      2      2  2        2            2            2
 + a*b*d*e*f - 3*a*b*f  + a*c *d  - 2*a*c *e + 2*a*c*d *f - a*c*d*e  + a*c*e*f

        2    3      2        2  2        2          2          2
 + a*e*f  - b *f + b *c*e - b *d *f + 2*b *e*f - b*c *d + b*c*d *e - b*c*d*f

          2          2      2      3    2  3      2          2
 - 2*b*c*e  + 2*b*d*f  - b*e *f + c  - c *d  + 3*c *d*e - 3*c *f - 3*c*d*e*f

      3        2    3
 + c*e  + 3*c*f  - f  = 0 or a - d = 0)

rlstruct h;


{(v4 = 0 or (v5 <> 0 and v7 <> 0) or (v6 <> 0 and v7 <> 0 and v8 <> 0)

  or (v7 <> 0 and v8 <> 0)) and (v7 <> 0 or v8 <> 0 or v9 = 0)

  and (v2 <> 0 or v3 = 0) and (v1 = 0 or v7 = 0),

        3  2    2            2          2    2    2    2      2
 {v1 = a *f  - a *b*e*f - 2*a *c*d*f + a *c*e  - a *d*f  + a*b *d*f - a*b*c*d*e

                                    2      2  2        2            2
   + 3*a*b*c*f + a*b*d*e*f - 3*a*b*f  + a*c *d  - 2*a*c *e + 2*a*c*d *f

            2                  2    3      2        2  2        2          2
   - a*c*d*e  + a*c*e*f + a*e*f  - b *f + b *c*e - b *d *f + 2*b *e*f - b*c *d

          2                      2          2      2      3    2  3      2
   + b*c*d *e - b*c*d*f - 2*b*c*e  + 2*b*d*f  - b*e *f + c  - c *d  + 3*c *d*e

        2                    3        2    3
   - 3*c *f - 3*c*d*e*f + c*e  + 3*c*f  - f ,

        2                                  2      2                        2
  v2 = a *e - a*b*d - a*c - a*d*e + a*f + b  + b*d  - 2*b*e + c*d - d*f + e ,

        2                                    2
  v3 = a *f - a*c*d - a*d*f + b*c - b*f + c*d  - c*e + e*f,

            2                    2      2                      2    3      2
  v4 = a*b*c  - 2*a*b*c*f + a*b*f  - a*c *e + 2*a*c*e*f - a*e*f  + b *f - b *c*e

        2              2      2      3      2        3        2    3
   - 2*b *e*f + 2*b*c*e  + b*e *f - c  + 3*c *f - c*e  - 3*c*f  + f ,

                                        3      2        2    2            2
  v5 = a*b*c - a*b*f - a*c*e + a*e*f - b  + 2*b *e - b*e  - c  + 2*c*f - f ,

  v6 = a*b - a*e - c + f,

  v7 = a - d,

  v8 = b - e,

  v9 = c - f}}

rlqe rlall (h equiv resultant(x^3+a*x^2+b*x+c,x^3+d*x^2+e*x+f,x)=0);


true

clear h;



% Discretely valued fields standard form:
rlset dvfsf;


*** p is being cleared 

*** turned off switch rlqeheu 

*** turned off switch rlqedfs 

*** turned on switch rlsusi 

{acfsf}

sub(x=a,x=0 and a=0 and ex(x,x=y) and ex(a,x~a));


a = 0 and a = 0 and ex x (x - y = 0) and ex a0 (a ~ a0)



% P-adic Balls, taken from Andreas Dolzmann, Thomas Sturm. P-adic
% Constraint Solving, Proceedings of the ISSAC '99.
rlset dvfsf;


*** turned on switch rlqeheu 

*** turned on switch rlqedfs 

*** turned off switch rlsusi 

*** p is being cleared 

*** turned off switch rlqeheu 

*** turned off switch rlqedfs 

*** turned on switch rlsusi 

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


  2                               2
(p  - 4*p + 3 | 2 or 2 ~ 1) and (p  + p - 2 | 3 or 3 ~ 1)

 and (p + 2 | 2*p or p - 2 || p + 2)

rlmkcanonic ws;


true

rlset(dvfsf,100003);


*** turned on switch rlqeheu 

*** turned on switch rlqedfs 

*** turned off switch rlsusi 

*** p is set to 100003 

*** turned off switch rlqeheu 

*** turned off switch rlqedfs 

*** turned on switch rlsusi 

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


true


% Size of the Residue Field, taken from Andreas Dolzmann, Thomas
% Sturm. P-adic Constraint Solving. Proceedings of the ISSAC '99.
rlset(dvfsf);


*** turned on switch rlqeheu 

*** turned on switch rlqedfs 

*** turned off switch rlsusi 

*** p is being cleared 

*** turned off switch rlqeheu 

*** turned off switch rlqedfs 

*** turned on switch rlsusi 

{dvfsf,100003}

rlqe ex(x,x~1 and x-1~1 and x-2~1 and x-3~1 and 2~1 and 3~1);


(3 ~ 1 and 2 ~ 1) or (7 ~ 1 and 6 ~ 1 and 5 ~ 1 and 3 ~ 1 and 2 ~ 1)

 or (5 ~ 1 and 3 ~ 1 and 2 ~ 1)

 or (11 ~ 1 and 10 ~ 1 and 6 ~ 1 and 3 ~ 1 and 2 ~ 1)

 or (7 ~ 1 and 6 ~ 1 and 3 ~ 1 and 2 ~ 1)

 or (6 ~ 1 and 5 ~ 1 and 3 ~ 1 and 2 ~ 1)

rlexplats ws;


(3 ~ 1 and 2 ~ 1) or (7 ~ 1 and 5 ~ 1 and 3 ~ 1 and 2 ~ 1)

 or (11 ~ 1 and 5 ~ 1 and 3 ~ 1 and 2 ~ 1) or (7 ~ 1 and 3 ~ 1 and 2 ~ 1)

 or (5 ~ 1 and 3 ~ 1 and 2 ~ 1)

rldnf ws;


3 ~ 1 and 2 ~ 1


% Selecting contexts:

rlset ofsf;


*** turned on switch rlqeheu 

*** turned on switch rlqedfs 

*** turned off switch rlsusi 

{dvfsf}

f:= ex(x,m*x+b=0);


f := ex x (b + m*x = 0)

rlqe f;


b = 0 or m <> 0

rlset dvfsf;


*** p is being cleared 

*** turned off switch rlqeheu 

*** turned off switch rlqedfs 

*** turned on switch rlsusi 

{ofsf}

rlqe f;


b + m = 0 or m <> 0

rlset acfsf;


*** turned on switch rlqeheu 

*** turned on switch rlqedfs 

*** turned off switch rlsusi 

{dvfsf}

rlqe f;


b = 0 or m <> 0


end;


Time for test: 135709 ms, plus GC time: 5137 ms