main
test-branch
|
Last change
on this file since 7d77e64 was ea777aa, checked in by Alex Wilton <awilton@…>, 3 years ago |
|
Moved examples, include, build_default.properties, common.xml, and README out from dev.civl.com into the root of the repo.
git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@5704 fb995dde-84ed-4084-dfe6-e5aef3e2452c
|
-
Property mode
set to
100644
|
|
File size:
2.0 KB
|
| Line | |
|---|
| 1 | #include <stdio.h>
|
|---|
| 2 | #ifdef _CIVL
|
|---|
| 3 | #include <civlc.cvh>
|
|---|
| 4 | #endif
|
|---|
| 5 |
|
|---|
| 6 | #ifdef _CIVL
|
|---|
| 7 | $input int ni,nj;
|
|---|
| 8 | $input int bi,bj; //TODO: bounds of block sizes ?
|
|---|
| 9 | $assume(ni > 1);
|
|---|
| 10 | $assume(nj > 1);
|
|---|
| 11 | $input double uin[ni][nj];
|
|---|
| 12 | #endif
|
|---|
| 13 | double u1[ni][nj];
|
|---|
| 14 | double u2[ni][nj];
|
|---|
| 15 |
|
|---|
| 16 | int main(int argc, char** argv) {
|
|---|
| 17 | int i,j,ir,jr,ib,jb;
|
|---|
| 18 |
|
|---|
| 19 | /*
|
|---|
| 20 | for(i=0;i<ni;i++) {
|
|---|
| 21 | for(j=0;j<nj;j++) {
|
|---|
| 22 | u1[i][j] = 0;
|
|---|
| 23 | u2[i][j] = 0;
|
|---|
| 24 | }
|
|---|
| 25 | }
|
|---|
| 26 |
|
|---|
| 27 | // straightforward loop nest
|
|---|
| 28 | for(i=1;i<ni-1;i++) {
|
|---|
| 29 | for(j=1;j<nj-1;j++) {
|
|---|
| 30 | u1[i][j] = uin[i][j]*uin[i][j];
|
|---|
| 31 | }
|
|---|
| 32 | }
|
|---|
| 33 | */
|
|---|
| 34 | $havoc(&u1);
|
|---|
| 35 | $havoc(&u2);
|
|---|
| 36 | $assume($forall (int i : 0 .. ni-1) u1[i][0] == 0 && u1[i][nj-1] == 0 && u2[i][0] == 0 && u2[i][nj-1] == 0);
|
|---|
| 37 | $assume($forall (int j : 0 .. nj-1) u1[0][j] == 0 && u1[ni-1][j] == 0 && u2[0][j] == 0 && u2[ni-1][j] == 0);
|
|---|
| 38 | $assume($forall (int i : 1 .. ni-2) ($forall (int j : 1 .. nj-2) u1[i][j] == uin[i][j] * uin[i][j]));
|
|---|
| 39 |
|
|---|
| 40 | if (ni > 2) {
|
|---|
| 41 | i = ni - 1;
|
|---|
| 42 | if (nj > 2)
|
|---|
| 43 | j = nj - 1;
|
|---|
| 44 | else
|
|---|
| 45 | j = 1;
|
|---|
| 46 | } else {
|
|---|
| 47 | i = 1;
|
|---|
| 48 | j = nj;
|
|---|
| 49 | }
|
|---|
| 50 |
|
|---|
| 51 | // blocked loop nest
|
|---|
| 52 | for(i=1;i<ni-bi;i=i+bi) {
|
|---|
| 53 | for(j=1;j<nj-bj;j=j+bj) {
|
|---|
| 54 | for(ib=0;ib<bi;ib++) {
|
|---|
| 55 | for(jb=0;jb<bj;jb++) {
|
|---|
| 56 | u2[i+ib][j+jb] = uin[i+ib][j+jb]*uin[i+ib][j+jb];
|
|---|
| 57 | }
|
|---|
| 58 | }
|
|---|
| 59 | }
|
|---|
| 60 | }
|
|---|
| 61 | // remainder i
|
|---|
| 62 | for(ir=i;ir<ni-1;ir=ir++) {
|
|---|
| 63 | for(jr=1;jr<nj-bj;jr=jr++) {
|
|---|
| 64 | for(jb=0;jb<bj;jb++) {
|
|---|
| 65 | u2[ir][jr+jb] = uin[ir][jr+jb]*uin[ir][jr+jb];
|
|---|
| 66 | }
|
|---|
| 67 | }
|
|---|
| 68 | }
|
|---|
| 69 | // remainder j
|
|---|
| 70 | for(jr=j;jr<nj-1;jr=jr++) {
|
|---|
| 71 | for(ir=1;ir<ni-bi;ir=ir++) {
|
|---|
| 72 | for(ib=0;ib<bi;ib++) {
|
|---|
| 73 | u2[ir+ib][jr] = uin[ir+ib][jr]*uin[ir+ib][jr];
|
|---|
| 74 | }
|
|---|
| 75 | }
|
|---|
| 76 | }
|
|---|
| 77 | // remainder ij
|
|---|
| 78 | for(ir=i;ir<ni-1;ir=ir++) {
|
|---|
| 79 | for(jr=j;jr<nj-1;jr=jr++) {
|
|---|
| 80 | u2[ir][jr] = uin[ir][jr]*uin[ir][jr];
|
|---|
| 81 | }
|
|---|
| 82 | }
|
|---|
| 83 |
|
|---|
| 84 |
|
|---|
| 85 | // assert equality of u1 and u2
|
|---|
| 86 | for(i=0;i<ni;i++) {
|
|---|
| 87 | for(j=0;j<nj;j++) {
|
|---|
| 88 | $assert(u1[i][j] == u2[i][j]);
|
|---|
| 89 | }
|
|---|
| 90 | }
|
|---|
| 91 | }
|
|---|
Note:
See
TracBrowser
for help on using the repository browser.
