wip hostside resolver continues; still startup.c not checked in here; before remove...

diff --git a/hostside/common.h b/hostside/common.h
index c27ba145982900f02f2241c43974e625cf229739..ef4d3e7089b9f7afefe50481a277c521b1284158 100644 (file)
--- a/hostside/common.h
+++ b/hostside/common.h
@@ -128,4 +128,8 @@ void nmra_addchecksum(Nmra *packet);
 void nmra_encodeforpic(const Nmra *packet, PicInsn *pi_out);
 
 
+#define ARRAY_SIZE(a) (sizeof((a))/sizeof(*(a)))
+#define ARRAY_END(a) ((a) + ARRAY_SIZE((a)))
+
+
 #endif /*COMMON_H*/

diff --git a/hostside/resolve.c b/hostside/resolve.c
index e471163fc2dc2de3826fe3352ba842339f1a1856..4c27aaa85d9d02f0b04dc65e7b6438834df23bef 100644 (file)
--- a/hostside/resolve.c
+++ b/hostside/resolve.c
@@ -178,24 +178,37 @@ void resolve_begin(void) {
   TrainNum t##n= (tra) - trains;               \
   TrainResolution *t##r= rx + t##n;
 
-#define APPENDING(array, variable, isreal)                             \
-  typeof(*array) variable;                                             \
-  for ((variable)=(array);                                             \
-       ;                                                               \
-       (variable)++) {                                                 \
-    assert((variable) < (array)+sizeof((array))/sizeof(*(array)));     \
-    if (!(isreal)) break;                                              \
-  }
+#define BLANKREASONS(array, sentinelmember)    \
+    ((*(SegmentNum*)(array))= NOTA(Segment))
+
+#define ADDREASON(array, newvalue) do{                 \
+    typeof(*(array)) addreason_i;                      \
+    for (addreason_i=(array);                          \
+         ;                                             \
+         addreason_i++) {                              \
+      assert(addreason_i < ARRAY_END(array));          \
+      if (!SOMEP(*(SegmentNum*)(addreason_i))) {       \
+       *addreason_i++= newvalue;                       \
+        *(SegmentNum*)addreason_i= NOTA(Segment);      \
+        assert(addreason_i < ARRAY_END(array));                \
+       break;                                          \
+      }                                                        \
+      if (*addreason_i == newvalue)                    \
+       break;                                          \
+    }                                                  \
+  }while(0)
+
+#define FOR_TRAIN_R(t)  FOR_TRAIN(t, t##r=rx, t##r++)
 
 int resolve_complete(void) {
   int problems;
   SEG_IV;
 
   rx= mmalloc(sizeof(*rx) * n_trains);
-  FOR_TRA {
-    rx[tran].r= RR_N;
-    rx[tran].why_eh.d= NOTA(Segment);
-    rx[tran].whynot_e.d1= NOTA(Segment);
+  FOR_TRAIN_R(t) {
+    tr->r= RR_N;
+    BLANKREASONS(tr->why_eh);
+    BLANKREASONS(tr->whynot_e);
   }
 
   while 1 {
@@ -212,18 +225,30 @@ int resolve_complete(void) {
        continue;
       /* 3. we have a violation of D \subset U, namely d */
 
+      ProofElement why_h;
+      why_h.d= d;
+      why_h.t= NOTA(Train);
+      
       if (d->owner) { /* 3a perhaps */
        TRAIN(t, d->owner);  /* t st d \elem E(t) */
-       if (tr->r == RR_H || SOMEP(tr->whynot_e[0]))
+       why_h.t= tn;
+       if (tr->r == RR_H)
          goto not_3a;
 
+       if (tr->r == RR_E)
+         /* we added it in this sweep and have found another d */
+         goto already_3a;
+       assert(tr->r == RR_N);
+
        /* check E(t) \disjoint U */
-       Clash clash;
-       FOR_SEGMENT(clash.d1, NOOP, NOOP) {
-         if (clash.d1->owner == t && clash.d1->tr_updated) {
-           FOR_TRAIN(clash.t2, NOOP, NOOP) {
-             if (clash.t2r->r == HH_H && clash.d1->owner == clash.t2) {
-               ADDREASON(tr->whynot_e, clash, SOMEP(clash->clash.d1));
+       FOR_SEGMENT(d1, NOOP, NOOP) {
+         if (d1->owner == t && d1->tr_updated) {
+           FOR_TRAIN(t2, NOOP, NOOP) {
+             if (t2r->r == HH_H && d1->owner == t2) {
+               Clash clash;
+               clash.d1= d1;
+               clash.t2= t2;
+               ADDREASON(tr->whynot_e, clash);
              }
            }
          }
@@ -232,8 +257,48 @@ int resolve_complete(void) {
          goto not_3a;
 
        /* Yay! 3a. */
+       tr->r= RR_E;
+      already_3a:
+       ProofElement why_e;
+       why_e.d= d;
+       why_e.t= NOTA(Train);
+       ADDREASON(tr->why_eh, why_e);
+       continue;
+      }
+
+    not_3a:
+      if (d->home) { /* 3b then */
+       TRAIN(t1, d->home); /* t' st d \elem H(t') */
        
+       if (tr->r == RR_H)
+         /* added in this sweep, have found another d */
+         goto already_3b;
+
+       FOR_SEGMENT(dplus, NOOP, NOOP) {
+         if (!dplus->owner) continue;
+         TRAIN(tplus, dplus->owner);
+         if (tplusr->r != HH_E) continue;
+         dplus->tr_updated= 0;
+       }
+       FOR_TRAIN_R(tplus) {
+         BLANKREASONS(tplusr->whynot_e);
+         if (tplusr->r == HH_E) {
+           tplusr->r= HH_N;
+           BLANKREASONS(tplusr->why_eh);
+         }
+       }
+
+       tr->r= RR_H;
+       BLANKREASONS(tr->why_eh);
 
+      already_3b:
+       ADDREASON(tr->why_eh, why_h);
+       fixme /* need to make us scan for case 3a first, so that
+                when we report a problem we report as reasons
+                for some H only those ds which would not have
+                been satisfied by E.  perhaps scan for Es
+                and then only for Hs, each time ? */
+       
          /* tr->whynot_e is already filled in */
          goto not_3a;
        assert(tr->r == RR_N);