Changes between Version 24 and Version 25 of Examples

Timestamp:

08/07/24 12:59:07 (21 months ago)

Author:

siegel

Comment:

--

Examples

@@ -63 +63 @@
 File `csr_driver.cvl`:
 {{{
-/* Filename : csr.cvl
+/* Filename : csr_driver.cvl
    Author   : Stephen F. Siegel
-   Created  : 2023-09-03
-   Modified : 2023-09-04
+   Created  : 2023-08-03
+   Modified : 2023-08-07
 
    Verification of matrix-vector multiplication routine using
@@ -82 +82 @@
 #include "csr.h"
 
+typedef struct $mat {
+  int n, m; // num rows, columns;
+  double data[][];
+} $mat;
+
+void $mat_vec_mul($mat mat, double * v, double *p) {
+  int n = mat.n, m = mat.m;
+  for (int i=0; i<n; i++) {
+    double s = 0.0;
+    for (int j=0; j<m; j++) s += mat.data[i][j]*v[j];
+    p[i] = s;
+  }
+}
+
+$mat $mat_csr(struct csr_matrix csr) {
+  int n = csr.rows, m = csr.cols;
+  $mat mat;
+  mat.n = n;
+  mat.m = m;
+  mat.data = (double[n][m])$lambda(int i,j) 0.0;
+  for (int i=0; i<n; i++) {
+    int r = csr.row_ptr[i], rnxt = csr.row_ptr[i+1];
+    for (int k=r; k<rnxt; k++)
+      mat.data[i][csr.col_ind[k]] = csr.val[k];
+  }
+  return mat;
+}
+
 // N,M=number of rows,columns.  N_B,M_B=upper bounds on N,M
 $input int N_B = 3, M_B = 3, N, M;
@@ -91 +119 @@
    of integers in [0,max].  Precondition: 0 <= len <= max+1 */
 void strict_inc(int * p, int len, int max) {
-  $assert(0<=len && len <= max+1);
+  //$assert(0<=len && len <= max+1);
   for (int i=0; i<len; i++) {
     int a = (i == 0 ? 0 : p[i-1]+1), b = max - len + i + 1;
@@ -146 +174 @@
 }
 
-/* Gets the (i,j)-th entry from the CSR matrix mat */
-double get_i_j(struct csr_matrix mat, int i, int j) {
-  int r = mat.row_ptr[i], rnxt = mat.row_ptr[i+1], col;
-  for (int k=r; k<rnxt; k++) {
-    col = mat.col_ind[k];
-    if (col == j) return mat.val[k];
-    if (col > j) break;
-  }
-  return 0.0;
-}
-
-/* Makes a dense matrix from the given CSR matrix */
-double ** make_dense(struct csr_matrix mat) {
-  int n = mat.rows, m = mat.cols;
-  double ** dense = malloc(n*sizeof(double*));
-  for (int i=0; i<n; i++) {
-    dense[i] = malloc(m*sizeof(double));
-    for (int j=0; j<m; j++)
-      dense[i][j] = get_i_j(mat, i, j);
-  }
-  return dense;
-}
-
-void destroy_dense(double ** dense, int nrow) {
-  for (int i=0; i<nrow; i++) free(dense[i]);
-  free(dense);
-}
-
-void dense_matrix_vector_multiply(int nrow, int ncol, double ** dense,
-                                  double * v, double *p) {
-  for (int i=0; i<nrow; i++) {
-    double s = 0.0;
-    for (int j=0; j<ncol; j++) s += dense[i][j]*v[j];
-    p[i] = s;
-  }
-}
-
 int main(void) {
   double v[M], actual[N], expected[N];
@@ -188 +179 @@
   struct csr_matrix mat = make_csr(N, M);
   csr_matrix_vector_multiply(&mat, v, actual);
-  double ** dense = make_dense(mat);
-  dense_matrix_vector_multiply(N, M, dense, v, expected);
+  $mat dense = $mat_csr(mat);
+  $mat_vec_mul(dense, v, expected);
 #ifdef VERBOSE
   printf("\n");
@@ -202 +193 @@
 #endif
   destroy_csr(mat);
-  destroy_dense(dense, N);
   $assert($equals(actual, expected));
 }
@@ -339 +329 @@
 }}}
 
-Times on a 2020 M1 !MacBook Pro: for matrices up to size 3x3: 10s. 
-Up to 3x4: 40s.  Up to 4x3: 43s.  Up to 4x4: 38 minutes.
+Times on a 2020 M1 !MacBook Pro: for matrices up to size 3x3: 6s. 
+Up to 3x4: 17s.  Up to 4x3: 17s.  Up to 4x4: 28 minutes.