test/db3/empset.c

   1 # include "empset.h"
   2
   3 static bool initDone = FALSE;
   4 static /*@only@*/ ereftab known;
   5
   6 static eref empset_get (employee e, erc s) /*@*/
   7 {
   8   erc_elements(s, er)
   9     {
  10       employee e1 = eref_get(er);
  11
  12       if (employee_equal(&e1, &e))
  13         {
  14           return er;
  15         }
  16     } end_erc_elements ;
  17
  18   return eref_undefined;
  19 }
  20
  21 bool empset_member (employee e, erc s)
  22 {
  23   return (eref_isDefined (empset_get (e, s)));
  24 }
  25
  26 void empset_clear (empset s)
  27 {
  28   erc_clear (s);
  29 }
  30
  31 bool /*@alt void@*/ empset_insert (empset s, employee e)
  32   /*@globals internalState@*/
  33   /*@modifies internalState@*/
  34 {
  35   if (eref_isDefined (empset_get (e, s)))
  36     {
  37       return FALSE;
  38     }
  39
  40   empset_insertUnique (s, e);
  41   return TRUE;
  42 }
  43
  44 void empset_insertUnique (empset s, employee e)
  45    /*@globals known@*/
  46    /*@modifies known@*/
  47 {
  48   eref er;
  49
  50   er = ereftab_lookup (e, known);
  51
  52   if (!eref_isDefined (er))
  53     {
  54       er = eref_alloc ( );
  55       eref_assign (er,e);
  56       ereftab_insert (known, e, er);
  57     }
  58
  59   erc_insert (s, er);
  60 }
  61
  62 bool /*@alt void@*/ empset_delete (empset s, employee e)
  63 {
  64   eref er;
  65
  66   er = empset_get (e, s);
  67
  68   if (!eref_isDefined (er))
  69     {
  70       return FALSE;
  71     }
  72
  73   return erc_delete (s, er);
  74 }
  75
  76 empset empset_disjointUnion (empset s1, empset s2)
  77    /*@globals known@*/
  78    /*@modifies known@*/
  79 {
  80   erc result;
  81   empset tmp;
  82
  83   result = erc_create ( );
  84
  85   if (erc_size (s1) > erc_size (s2))
  86     {
  87       tmp = s1;
  88       s1 = s2;
  89       s2 = tmp;
  90     }
  91
  92   erc_join (result, s1);
  93
  94   empset_elements(s2, emp)
  95     {
  96       empset_insertUnique(result, emp);
  97     } end_empset_elements ;
  98
  99   return result;
 100 }
 101
 102 empset empset_union (empset s1, empset s2)
 103 {
 104   erc result;
 105   empset tmp;
 106
 107   result = erc_create ();
 108
 109   if (erc_size (s1) > erc_size (s2))
 110     {
 111       tmp = s1;
 112       s1 = s2;
 113       s2 = tmp;
 114     }
 115   erc_join (result, s2);
 116
 117   empset_elements (s1, emp)
 118     {
 119       if (!empset_member(emp, s2))
 120         {
 121           empset_insert(result, emp);
 122         }
 123     } end_empset_elements ;
 124
 125   return result;
 126 }
 127
 128 void empset_intersect (empset s1, empset s2)
 129 {
 130   erc toDelete = erc_create();
 131
 132   empset_elements (s2, emp)
 133     {
 134       if (!empset_member(emp, s2))
 135         {
 136           empset_insert(toDelete, emp);
 137         }
 138     } end_empset_elements ;
 139
 140   empset_elements (toDelete, emp)
 141     {
 142       empset_delete(s1, emp);
 143     } end_empset_elements;
 144
 145   erc_final (toDelete);
 146 }
 147
 148 bool empset_subset (empset s1, empset s2)
 149 {
 150   empset_elements(s1, emp)
 151     {
 152       if (!empset_member(emp, s2))
 153         {
 154           return FALSE;
 155         }
 156     } end_empset_elements ;
 157
 158   return TRUE;
 159 }
 160
 161 void empset_initMod (void)
 162   /*@globals initDone, undef known@*/
 163   /*@modifies initDone, known@*/
 164 {
 165   if (initDone)
 166     {
 167       /*@-globstate@*/ return; /*@=globstate@*/
 168     }
 169
 170   bool_initMod ();
 171   employee_initMod ();
 172   eref_initMod ();
 173   erc_initMod ();
 174   ereftab_initMod ();
 175   known = ereftab_create ();
 176   initDone = TRUE;
 177 }