source: git/Tst/New/sat_cleardenom.tst @ 56c0fe

spielwiese
Last change on this file since 56c0fe was 6d5e3ce, checked in by Janko Boehm <boehm@…>, 11 years ago
Added test for sat
  • Property mode set to 100644
File size: 2.3 KB
Line 
1LIB "tst.lib"; tst_init();
2LIB "elim.lib";
3ring R=(0,a),x(1..3),dp;
4minpoly = a2+1;
5
6int n = 3;
7int m = 2;
8  list rl = ringlist(R);
9   int k;
10   for(k = 1; k <= n; k++)
11     {
12        rl[2][k] = "x("+string(k)+")";
13     }
14   for(k = 1; k <= m; k++)
15     {
16        rl[2][k+n] = "y("+string(k)+")";
17     }
18   rl[3]= list(list("dp",1:(n+m)),list("C",0));
19   /*Use Hilbert driven Buchberger*/
20   def Rbig0 = ring(rl);
21   setring Rbig0;
22
23
24matrix HM[2][2]=y(1),
25(85487396464080*a-672629646755040)*x(1)^4+(1486235684289200*a-221204675596320)*x(1)^3*x(2)+(392179468524480*a+140976390779120)*x(1)^2*x(2)^2+(1486235684289200*a-221204675596320)*x(1)*x(2)^3+(306692072060400*a+813606037534160)*x(2)^4+(417625502236920*a-62157512916432)*x(1)^3*x(3)+(270683195894300*a-40287276890280)*x(1)^2*x(2)*x(3)+(-989927116413440*a+147336326913024)*x(1)*x(2)^2*x(3)+(-232014167909400*a+34531951620240)*x(2)^3*x(3)+(-5037031828686240*a+1904524949647680)*x(1)^2*x(3)^2+(-1643951241259920*a+3502964647809600)*x(1)*x(2)*x(3)^2+(920076216181200*a+2440818112602480)*x(2)^2*x(3)^2+(-1392085007456400*a+207191709721440)*x(1)*x(3)^3+(-696042503728200*a+103595854860720)*x(2)*x(3)^3,
26y(2),
27-655628472*x(1)^3*x(3)-424944380*x(1)^2*x(2)*x(3)+1554082304*x(1)*x(2)^2*x(3)+364238040*x(2)^3*x(3)+2185428240*x(1)*x(3)^3+1092714120*x(2)*x(3)^3;
28
29ideal I =x(1)^6+3*x(1)^4*x(2)^2+3*x(1)^2*x(2)^4+x(2)^6-4*x(1)^4*x(3)^2-34*x(1)^3*x(2)*x(3)^2-7*x(1)^2*x(2)^2*x(3)^2+12*x(1)*x(2)^3*x(3)^2+6*x(2)^4*x(3)^2+36*x(1)^2*x(3)^4+36*x(1)*x(2)*x(3)^4+9*x(2)^2*x(3)^4;
30
31ideal phi=(85487396464080*a-672629646755040)*x(1)^4+(1486235684289200*a-221204675596320)*x(1)^3*x(2)+(392179468524480*a+140976390779120)*x(1)^2*x(2)^2+(1486235684289200*a-221204675596320)*x(1)*x(2)^3+(306692072060400*a+813606037534160)*x(2)^4+(417625502236920*a-62157512916432)*x(1)^3*x(3)+(270683195894300*a-40287276890280)*x(1)^2*x(2)*x(3)+(-989927116413440*a+147336326913024)*x(1)*x(2)^2*x(3)+(-232014167909400*a+34531951620240)*x(2)^3*x(3)+(-5037031828686240*a+1904524949647680)*x(1)^2*x(3)^2+(-1643951241259920*a+3502964647809600)*x(1)*x(2)*x(3)^2+(920076216181200*a+2440818112602480)*x(2)^2*x(3)^2+(-1392085007456400*a+207191709721440)*x(1)*x(3)^3+(-696042503728200*a+103595854860720)*x(2)*x(3)^3,
32-655628472*x(1)^3*x(3)-424944380*x(1)^2*x(2)*x(3)+1554082304*x(1)*x(2)^2*x(3)+364238040*x(2)^3*x(3)+2185428240*x(1)*x(3)^3+1092714120*x(2)*x(3)^3;
33sat(I+minor(HM,2),phi);
34tst_status(1);$
35
Note: See TracBrowser for help on using the repository browser.