Last change
on this file since 1 was 1, checked in by Marek Rychlik, 15 years ago |
First import of a version circa 1997.
|
File size:
568 bytes
|
Line | |
---|
1 | if get('geometry2, 'version)=false then load(geometry2);
|
---|
2 | X:[x1,y1]; Y:[x2,y2]; O1:[-p,0]; O2:[p,0];
|
---|
3 | /* Semi-axes are 1 and sqrt(1-p^2) */
|
---|
4 | f(W) := (1-p^2)*w[1]^2+w[2]^2-(1-p^2); /* W is on the ellipse */
|
---|
5 | vars: []; params: [p,u,x1,y1,x2,y2,r1,r2,s1,s2];
|
---|
6 | cover: [
|
---|
7 | [
|
---|
8 | f(X), f(Y),
|
---|
9 | distance(X,O1,r1),
|
---|
10 | distance(Y,O1,s1),
|
---|
11 | collinear(X,Y,O1),
|
---|
12 | u*(1-p^2)-2
|
---|
13 | ],
|
---|
14 | [
|
---|
15 | p,
|
---|
16 | (x1-x2)*(y1-y2)
|
---|
17 | ]
|
---|
18 | ];
|
---|
19 | concl: (r1+s1-u*r1*s1)*(r1+s1+u*r1*s1)*(r1-s1-u*r1*s1)*(r1-s1+u*r1*s1);
|
---|
20 |
|
---|
21 |
|
---|
22 |
|
---|
23 | eqns:[concl];
|
---|
24 |
|
---|
25 | eqns:expand(eqns);
|
---|
26 | cover:expand(cover);
|
---|
27 | stringout("klee2.out",eqns,vars,params,cover);
|
---|
Note:
See
TracBrowser
for help on using the repository browser.